Zulip Chat Archive

Stream: new members

Topic: add_right_cancel natural number game

Thomas Laraia (Jul 04 2021 at 08:36):

Hi, I am working on add_right_cancel in Advanced Addition World and am not understanding why I cannot apply succ_inj to the h hypothesis. I can see the steps that need to be taken but maybe I need to take a more roundabout way?

intro h,
induction t with d hd,
rw add_zero at h,
rw add_zero at h,
rw h,
repeat {rw add_succ at h},
apply succ_inj at h,

Thomas Laraia (Jul 04 2021 at 08:42):

And at the same time, if I just apply succ_inj, the goal changes from a = b to succ a = succ b, which feels like the opposite of what succ_inj is supposed to do.

Ruben Van de Velde (Jul 04 2021 at 08:58):

You've fallen victim to a common misunderstanding about apply. apply means "I've got a lemma whose conclusion matches the goal, so to prove my goal, it suffices to prove the hypothesis of this lemma"

Ruben Van de Velde (Jul 04 2021 at 09:01):

In this case, you want to use succ_inj {a b : mynat} : succ(a) = succ(b) → a = b with the hypothesis h : succ (a + d) = succ (b + d) to conclude a + d = b + d; you do that by treating → as a function application: have h2 := succ_inj h,

Ruben Van de Velde (Jul 04 2021 at 09:03):

Alternatively, you can go backwards from the goal and claim it suffices to prove a + d = b + d by apply hd,

Thomas Laraia (Jul 04 2021 at 09:08):

Perfect, thank you for the explanation!

Last updated: Dec 20 2023 at 11:08 UTC