applying theorem to hypothesis

Stream: new members

[Mujtaba Alam]

(world 8 level 10) I have the hypothesis (I think that's the term?) H : succ (a + d) = 0 and the goal ⊢ false. I'd like to apply the theorem succ_ne_zero := (a : mynat) : succ a ≠ 0 to H in order to have H : false. How do I do that?

[Riccardo Brasca]

Does

exact (succ_ne_zero (a + d) H)

work?

[Kevin Buzzard]

I don't teach definitional equality in the game, but succ a ≠ 0 is by definition succ a = 0 -> false, which means that if you feed succ_ne_zero x a proof that succ x = 0 then it will return a proof of false, so my guess is that Riccardo's suggestion will work.

[Ryan Duan]

Is there a way for me to reorder things? Like how can I reoder a +c +b + d into b + c + a + d? I expiremented using a series of add_comms and add_assocs and they didn't really reorder differently. Do I just need to try more or is there an easier way?

[Yaël Dillies]

If this is your goal, abel or ring will do it.

[Ryan Duan]

gotcha. I don't thinkn ring worked in the context i had, but abel did. Thanks!

[Kyle Miller]

@Ryan Duan You can pass arguments to add_assoc and add_comm help specify which terms they should apply to:

example (a b c d : ℕ) : a + c + b + d = b + c + a + d :=
begin
  rw [add_assoc a, add_comm a, add_comm c],
end

[Kevin Buzzard]

Whether tactics like abel or ring will work may somehow depend on how far through the game you are :-)

[Mujtaba Alam]

Kevin Buzzard said:

I don't teach definitional equality in the game, but succ a ≠ 0 is by definition succ a = 0 -> false

I'm certain that was mentioned at least once, and confident it was mentioned twice. I'm just thick/couldn't figure out the syntax

[Mujtaba Alam]

Riccardo Brasca said:

Does

exact (succ_ne_zero (a + d) H)

work?

Yes it does!
I see that once it gets it's first argument it becomes succ (a + b) = 0 -> false, and since H is the first proposition it give false. Very functional.
Thank you!

[Mujtaba Alam]

One possible bug: in world 8 level 12, a single refl, proves the theorem. Is this the intended solution?

[Kyle Miller]

One way to think about it is that refl will automatically rewrite using all the lemmas that are true by definition -- the lemmas add_zero and add_succ define addition, and one_eq_succ_zero defines 1.

[Kyle Miller]

This is more-or-less what "definitional equality" is -- Lean has a collection of defining lemmas it will automatically apply when it checks whether two things are the same.

[Kyle Miller]

The natural number game doesn't reveal which lemmas are true by definition. They come from the underlying theory. (And I'm not being particularly precise here. More precisely there's a system for unfolding definitions while it checks whether two things are the same.)

[Kyle Miller]

By the way, this is roughly what a refl for world 8 level 12 is doing:

rw one_eq_succ_zero,
rw add_succ,
rw add_zero,
refl,

[Kyle Miller]

If you want a less smart refl, then you can use tactic.reflexivity reducible. For example, that fails, but the following works:

rw one_eq_succ_zero,
rw add_succ,
rw add_zero,
tactic.reflexivity reducible,