Natural Number Game - Weird proof in Advanced Addition World

Stream: general

[Sukera]

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]

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

[Sukera]

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

[Henrik Böving]

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]

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]

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]

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

[Sukera]

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

[Sukera]

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

[Kevin Buzzard]

What's the actual statement of the theorem?

[Sukera]

Just level 2 of the Advanced Addition World

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]

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

[Kevin Buzzard]

@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.