1
$\begingroup$

So I have been trying to learn Lean and have managed to find this resource called the "Natural Number Game" which is supposed to help me learn Lean.

I am learning Lean to help me understand the art of proof writing, which has never really been a strong suit of mine, as well as to learn how to use a proof assistant.

Now, it has been going pretty well so far (except for proving $2+2=4$, which took me around a half hour) except now I'm stuck trying to prove $0+n=n$ by induction.

I have been able to prove the two intermediate steps (for $0+n=n$ and $0+\operatorname{succ}(d)=\operatorname{succ}(d)$), but I don't know how to prove it for $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$. Here is what I have tried so far:

rw [succ_eq_add_one]
rw [one_eq_succ_zero]
rw [add_succ]
rw [add_zero]

although I must have done something wrong, since I ended up with $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$, which is what I want to prove. My question is: What am I doing wrong here that made me end up with the original statement that I wanted to prove, and how do I prove that $\operatorname{succ}(0+\operatorname{succ}(d))=\operatorname{succ}(\operatorname{succ}(d))$?

Here is the code from proving the intermediate steps:

First intermediate step ($0+n=n$)

induction n with d hd
rw [add_zero]
rfl

Second intermediate step ($0+\operatorname{succ}(d)=\operatorname{succ}(d)$)

rw [add_succ]
induction d with d hd
rw [add_zero]
rfl
$\endgroup$
3
  • 1
    $\begingroup$ Can you explain better the problem? If you want to prove 0+d=d by induction (that is a very good idea), the two cases should be 0+0=0 and 0 + succ d = succ d knowing that 0 + d = d. $\endgroup$
    – Ricky
    Jan 19 at 15:54
  • 1
    $\begingroup$ Ah, I see, you are trying to prove even the induction step by induction. Well, this is not a very good idea. But notice that you now have a new assumption! $\endgroup$
    – Ricky
    Jan 19 at 16:01
  • $\begingroup$ Just use induction once :-) $\endgroup$ Jan 19 at 16:23

1 Answer 1

1
$\begingroup$

I managed to figure it out.

Going back to proving $0+\operatorname{succ}(d)=\operatorname{succ}(d)$, it turns out all I needed to do was rw [add_succ] to turn it into $\operatorname{succ}(0+d)=\operatorname{succ}(d)$ and then use rw [hd] to turn it into $\operatorname{succ}(d)=\operatorname{succ}(d)$ (because I forgot to rewrite what I had as the hypothesis because I could have done that in the first place) and then I could use rfl to finally complete my proof by induction.

Full proof (plus original step proving $0+n=n$):

induction n with d hd
rw [add_zero]
rfl
rw [add_succ]
rw [hd]
rfl

Where I probably went wrong in my original attempt:

succ_eq_add_one doesn't help because then I am going to be stuck proving that $0+d+1$ is identical to $d+1$, which in turn looped me back to where I had started.

$\endgroup$
1
  • $\begingroup$ Remember to mark your answer as accepted if it solves all your problems. $\endgroup$
    – James Wood
    Jan 22 at 9:56

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.