Natural numbers game - Advanced addition

Stream: new members

[Damiano Testa]

I managed to solve the Advanced Addition World Level 1 and 2 (http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/?world=8&level=1) using the commands below, but, honestly, I do not understand why it worked. Can someone explain the reason why this is a valid proof? Thank you!

Level 1:
cases hs with g h,
refl,

Level21:
cases h with g h,
refl,

[Johan Commelin]

Ha, there's a bit of trickery going on there...

[Johan Commelin]

I think this is not the "intended solution" (@Kevin Buzzard correct me if I'm wrong)

[Johan Commelin]

@Damiano Testa I think Kevin wanted to have you start with apply succ_inj, or something like that.

[Johan Commelin]

@Damiano Testa If you have h : x = complicated thing, and you run cases h, then Lean figures out that it should just substitute all occurences of x with complicated thing (I actually don't know the details of why).
In this case it seems to figure out that the only way that succ a and succ b can be equal is if a = b, so it replaces all occurences of b with a.

[Johan Commelin]

@Floris van Doorn or @Jeremy Avigad could you maybe give the "official" explanation?

[Jeremy Avigad]

It has to do with the fact that equality is defined internally as an indexed inductive type with a single constructor, reflexivity; the elimination principle is essentially just substitution.

Probably the best way to think of it is this: when you ask Lean to do cases on an equality "x = y", it knows that x and y are supposed to be the same, and so it replaces x by y.

[Jeremy Avigad]

Another way to say it: the canonical way to "use" an equation is just to substitute. cases on something is supposed to give us the canonical way of using it.

[Johan Commelin]

But how can it "see through" the succ on both sides...

[Johan Commelin]

Why does it change a = b in the goal to a = a

[Floris van Doorn]

cases has special support to deal with equalities between constructors of inductive types. Under the hood I'm quite sure it calls no_confusion.
no_confusion is the way in Lean to simultaneously do show things:

• Two different constructors of an inductive type are never equal;
• Every constructor is injective: they are only equal if all their inputs are equal.

[Johan Commelin]

Yup, it calls no_confusion

[Floris van Doorn]

Johan is correct that in this case it does not just apply the induction principle of equality, so it's more than just induction hs (which should fail)

[Johan Commelin]

Yup, that indeed fails.

[Jeremy Avigad]

Sorry, yes, I read too quickly. Leo did a lot of work on the cases tactic so that it would do the right thing when pattern matching in function definitions. So there are heuristics being applied under the hood, including no_confusion.

[Kevin Buzzard]

rofl so @Damiano Testa it's all about no_confusion, so I hope you're no longer confused :-)

[Kevin Buzzard]

but I rather suspect you are now more confused :-/

[Kevin Buzzard]

These are great proofs by the way!

[Damiano Testa]

Dear All,

Thank you very much for your answers! I do not fully understand them and as @Kevin Buzzard suggests, I will need to apply no_confusion a few more times! Anyway, it is fun to learn Lean!

[Kevin Buzzard]

https://xenaproject.wordpress.com/2018/03/24/no-confusion-over-no_confusion/ @Damiano Testa