How do I prove $\operatorname{succ}(a)$ cannot be equal to $0$ in Lean4?

Question

So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean¹. However, I am currently stuck on level 6/9 in the Algorithm world, where I am supposed to prove the theorem succ_ne_zero $\operatorname{succ}(a)\ne0$ (Peano's Last Axiom).

---

Define a function as follows:

is_zero 0 := True
is_zero (succ n) := False

We have to prove that in the natural numbers, there is no number such that $\operatorname{succ}(a)=0$ and are introduced to two new lemmas, is_zero_zero and is_zero_succ n. We are also introduced to the triv tactic, which the in-game documentation of it just says that triv will solve the goal True.

Here is my attempt at trying to solve this:

Code                           Explanation
____________________________________________________________________________________________________________________
intro h                        Start proof
rw [← is_zero_succ a]          Changes the goal "False" to "is_zero (succ a)"
symm at h                      Changes the assumption "h: succ a = 0" to "h: 0 = succ a" so I can use "zero_ne_succ"
apply zero_ne_succ at h        Changes the assumption "h: 0 = succ a" to "h: False"

And here is where I'm stuck. I seriously do not know what do from here, since I can't use triv since that can only solve a case if that case is True and using apply zero_ne_succ normally just gives me the goal 0 = succ ?a, which I can't do anything to.

So my question is: How do I prove in Lean4 that $\operatorname{succ}(a)\ne0$?

Answer 1

The exercise gives starting instructions:

intro h
rw [<- is_zero_suc a]

These give the following proof state:

Objects:
a: ℕ

Assumptions:
h: succ a = 0

Goal:
is_zero (succ a)

The thing to spot here is that one of the sides of equation h appears in the goal – succ a. This means that rewriting by h might let us make some progress.

rw [h]

Objects:
a: ℕ

Assumptions:
h: succ a = 0

Goal:
is_zero 0

Then, our goal is_zero 0 is by definition True, so we can use triv to finish. You could also use rw [is_zero_zero] then triv to see the definition being unfolded.

Answer 2

Another possibility here is using cases h as fifth step to your original demo attempt. This is the way to use a False hypothesis. As there is no element for this type/proof, there is nothing more to be done to prove the goal.