Stream: general

Sukera (Dec 25 2022 at 18:34):

Hi there, I hope this is the correct stream! I think I found a weird proof for Level 2 of the Advanced Addition World in the Natural Number Game. I'm using this solution:

cases h with ha hb,
refl,


which I'm not sure why or how it works in the first place, especially since it doesn't use any of the additional peano axioms that are thought to be required.

Sukera (Dec 25 2022 at 18:35):

Can someone help me to understand why this works? Should it work..?

Sukera (Dec 25 2022 at 18:35):

For what it's worth, this same proof also works for level 1 of Advanced Addition..

Henrik Böving (Dec 25 2022 at 20:20):

In general the vast majority of things in Lean should work the way they are yes^^

The reason it works is that cases implicitly made use of the injectivity properties here on its own which is in general a thing it can do, for example you can also use it to prove that 1 \neq 2

Kevin Buzzard (Dec 25 2022 at 20:45):

I don't explain definitional equality in the game but things like x + 0 = x can be proved with refl because they're true by definition. See this section of my course for more details.

Sukera (Dec 25 2022 at 20:55):

The equality part with refl makes sense to me, but the task state after cases doesn't

a : mynat,
h : succ (succ a) = succ (succ a)
⊢ a = a


I'm mostly confused why cases doesn't replace h with ha and hb, as the documentation implies :thinking: I guess it makes sense that it sees that ha and hb can be combined with injectivity, resulting in just h again?

Sukera (Dec 25 2022 at 20:56):

well, less the documentation, more the explanation in the Game :)

Sukera (Dec 25 2022 at 20:57):

I guess I'm just missing ha and hb, that cases (as far as I understood so far) should have introduced here

Sukera (Dec 25 2022 at 21:09):

anyway, it's a fun game and good to learn Lean - thanks for creating it! :)

Kevin Buzzard (Dec 25 2022 at 21:40):

What's the actual statement of the theorem?

Sukera (Dec 26 2022 at 10:22):

For all naturals $a$ and $b$, if we assume $succ(succ(a))=succ(succ(b))$, then we can deduce $a=b$.

theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b :=


Sukera (Dec 26 2022 at 10:25):

it kind of feels like cases just does the deduction by itself

Kevin Buzzard (Dec 28 2022 at 01:45):

@Sukera sorry for the delay, was doing family stuff. Yeah cases does do the deduction by itself. You're doing cases on an equality here, which is not at all documented or explained in the game. Equality is an inductive type with one constructor and Lean's equation compiler is very powerful. Basically instead of using succ_inj you are reproving it. You can break out of the game like this:

cases h,
refl,
end
#print succ_inj


and the output of the #print statement is a bit incomprehensible, it's

  eq.dcases_on h
(λ (H_1 : succ n = succ m),
mynat.no_confusion H_1
(λ (n_eq : n = m),
eq.rec (λ (h : succ m = succ m) (H_2 : h == eq.refl (succ m)), eq.refl m) (eq.symm n_eq) h))
(eq.refl (succ n))
(heq.refl h)


and you can see that it's using eq.dcases_on h right at the start, which is doing cases on a hypothesis of the form succ(a)=succ(b). To understand better what's going on you'll have to learn a bit about induction on equality, which I talk about here.

Last updated: Dec 20 2023 at 11:08 UTC