How to prove that inductive type is false?

Stream: general

[Mario Weitzer]

How can I prove the following?

inductive mytype : ℕ → Prop
| mytype_one : mytype 1
| mytype_succ : ∀ n, mytype n → mytype n.succ

example : ¬(mytype 0) := sorry

[Adam Topaz]

inductive mytype : ℕ → Prop
| mytype_one : mytype 1
| mytype_succ : ∀ n, mytype n → mytype n.succ

example : ¬(mytype 0) .

[Mario Weitzer]

Hmm, that doesn‘t work for me. I should probably mention that I am using Lean 3.

[Adam Topaz]

it should work. Here's the code in the lean3 web editor: https://leanprover-community.github.io/lean-web-editor/#code=inductive%20mytype%20%3A%20%E2%84%95%20%E2%86%92%20Prop%0A%7C%20mytype_one%20%3A%20mytype%201%0A%7C%20mytype_succ%20%3A%20%E2%88%80%20n%2C%20mytype%20n%20%E2%86%92%20mytype%20n.succ%0A%0Aexample%20%3A%20%C2%AC(mytype%200)%20.%0A

[Mario Weitzer]

Oh wait, sorry. It works, but I had to remove the :=
But what does this even mean?

[Adam Topaz]

This is an unreachable case of an inductive type, and so lean knows it's impossible all by itself.

[Adam Topaz]

if you want a more verbose variant, you could do something like this:

example : ¬(mytype 0) := λ h, by cases h

[Mario Weitzer]

I see. The solution being “.” makes this not only the shortest but also the lowest proof, I guess. I made it a theorem and “#print”ed it and as I suspected the solution involves no_confusion but I just couldn’t figure it out myself. Also, library_search couldn’t solve it. Thank you very much!

[Kevin Buzzard]

library_search looks for theorems in the library which will solve the goal, and given that you just defined mytype and didn't prove any theorems about it, it's unsurprising that library_search doesn't work.