Applying `succ_inj` to a sum, natural numbers game

Stream: new members

[Berber]

I am currently playing the natural numbers game, "advanced addition world", level 1 https://adam.math.hhu.de/#/g/leanprover-community/nng4/world/AdvAddition/level/1

To show is that a + n = b + n implies a = b for natural numbers a b n. I started the induction, and I arrive at a point where I have assumptions succ (a + d) = succ (b + d) and a + d = b + d, and I want to show a = b, which I did via the following:

intro h
induction n with d hd
rw [← add_zero a, ← add_zero b]
exact h
repeat rw [add_succ] at h

I would just like to apply succ_inj at h, but it doesn't work. Normally I would think "Well, a and n are natural numbers, so a + n is a natural number, similarly a + b is a natural number, so I can just apply succ_inj, but I see that doesn't work as-is, since succ_inj doesn't know this.

How can I solve this problem?

Give me any suggestios, style guides, how to approach things etc. that you can! Thanks!

[Johannes Tantow]

You cannot apply succ_inj to h, because it is hypothesis. succ_inj looks like this: MyNat.succ_inj (a b : ℕ) (h : MyNat.succ a = MyNat.succ b) : a = b, i.e. it is an implication with the consequent a=b. You can apply it something that matches the consequent and have then the antecdent as the remaining goal. As this looks like h you know that you could close this goal with the right values for a and b. Can you transform the goal to that ? There is another hypothesis in the context.

[Kevin Buzzard]

apply succ_inj at h works fine for me after the code block above:

succinj.png

Can you clarify "but it doesn't work"?

[Berber]

Johannes Tantow said:

You cannot apply succ_inj to h, because it is hypothesis.

I do not understand what you mean here, care to explain? If h were the hypothesis succ x = succ y, then I would be able to apply succ_inj at h. Right?

In any case, now the hypothesis looks a bit different, namely succ (a + d) = succ (b + d), so I do not know what I can do here.

As this looks like h you know that you could close this goal with the right values for a and b. Can you transform the goal to that ? There is another hypothesis in the context.

I also don't understand this. I mean, if you are fine with it, you could provide a solution that you could present here?

[Berber]

Kevin Buzzard said:

apply succ_inj at h works fine for me after the code block above

Can you clarify "but it doesn't work"?

Fantastic (sarcasm), now it works for me as well. It seems like I tried it correctly. I don't know what is different now. Sometimes, the lean engine in the web interface behaves weirdly, so maybe it was that. Thanks for trying it out for me!

[Johannes Tantow]

Ok, I realize that I was talking rubbish. I didn't know that apply can be used this way to, but let me clarify my idea. Succ_inj looks fundamentally like : q -> p, where q is like the hypothesis h. You want to apply it forward and change h from q to p. I proposed to apply it backwards. Bring the goal into the state p and then apply succ_inj and close it with h.

My proof looks like this:

intro h
induction n with d ih
--base
rw [add_zero, add_zero] at h
exact h

--step
apply ih
apply succ_inj
exact h

[Kevin Buzzard]

yeah, apply can be used to argue forwards or backwards. Is that your question?