2
$\begingroup$

So I have been using The Natural Number Game (as I have mentioned in my previous post) to learn Lean1. 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$?

$\endgroup$
5
  • 1
    $\begingroup$ Does this answer your question? In Lean, why is it possible to prove $\text{succ}\; x \neq 0$ without adding it as an axiom? $\endgroup$
    – Jason Rute
    Jan 21 at 3:26
  • $\begingroup$ @JasonRute No, as I’m forced to type the proof line by line, and don’t have access to defining custom functions. I also don’t have access to a lot of the functions used in the question and answers you linked. $\endgroup$
    – CrSb0001
    Jan 21 at 14:01
  • $\begingroup$ Can you link to the NNG world you are stuck in so we can see which rules you are allowed to use? $\endgroup$
    – Jason Rute
    Jan 21 at 15:20
  • $\begingroup$ Ok. Found it. adam.math.hhu.de/#/g/leanprover-community/nng4/world/Algorithm/… The solution is by induction. It’s the same technique given in Andre’s answer to the linked question. Use the is_zero function you have available. $\endgroup$
    – Jason Rute
    Jan 21 at 15:23
  • $\begingroup$ Ok, maybe I’m leading you astray here. Looking at your proof, your first two steps are correct. Now, as you said you want to use trivial but right now what you are proving is false. Can you use your hypotheses to turn it into something true where trivial works. (Hint, rewrite succ a to be 0.) $\endgroup$
    – Jason Rute
    Jan 21 at 15:51

2 Answers 2

6
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.