0
$\begingroup$

So, as mentioned in my previous two questions, I have been using The Natural Number Game to help me teach myself how to use the mathematical proof assistant Lean4.

I am currently trying to complete the Advanced Addition world so I can get access to the "≤ World"1 so I can more easily prove the clunky version of Fermat's Last Theorem2, and for some reason I am currently stuck on proving the add_right_theorem (Level 1 of Advanced Addition World), which states that$$a+n=b+n\implies a=b$$which I don't exactly know how I would state the proof or write it out in Lean4

Here's what I have done so far:

  1. The first part (the proof by induction) is pretty easy. All I need to do is this:
induction n with d hd
repeat rw [add_zero]
intro h
exact h

however the second part$$a+\operatorname{succ}(d)=b+\operatorname{succ}(d)\implies a=b$$is where I am struggling. All I can do is add the successions together to rewrite it as$$\operatorname{succ}(a+d)=\operatorname{succ}(b+d)\implies a=b$$before being forced to introduce the hypothesis h to rewrite it as this:

hd: a + d = b + d → a = b
h: succ (a + d) = succ (b + d)
Goal: a = b

Now, when I apply succ_inj at h, it leaves me with

hd: a + d = b + d → a = b
h: a + d = b + d
Goal: a = b

and now I'm stuck, because I can't use decide since that returns the exact same thing, and triv doesn't work since the case "True" doesn't exist. (I got a bit desperate, sorry.)

Here is my proof so far:

induction n with d hd
repeat rw [add_zero]
intro h
exact h
repeat rw [add_succ]
intro h
apply succ_inj at h

So my question is: Where am I messing up the proof of the add_right_cancel theorem, and how should I actually go about proving it?


1I'll replace this with \le if it would look neater, the unicode for the "less than or equal to" symbol is u+00264 for anyone who wants to know.

2The more clunky version of Fermat's Last Theorem (that is, the first case of it) comes up in Power World level 10/10, and states that for no $a,b,c,n\in\mathbb N$,$$(a+1)^{n+3}+(b+1)^{n+3}=(c+1)^{n+3}$$which is where the Inequality World would come in handy, because it would greatly shorten the proof. The first case has been proven in Lean.

$\endgroup$

1 Answer 1

1
$\begingroup$

From

hd: a + d = b + d → a = b
h: a + d = b + d
Goal: a = b

you can use the apply tactic.

$\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.