search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 47 forks source link

Is it okay to use `succ_add` to prove `succ_add` or is this a typo? #33

Closed williamdemeo closed 7 years ago

williamdemeo commented 7 years ago

I would make this a pull request, but I'm not sure it's a real typo (and I have pull-request-rejection anxiety :)

Here is an example from Section 7.4:

    theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
    nat.rec_on n rfl (λ n ih, by simp only [succ_add, ih])

Is the use of succ_add in the simp tactic okay? Maybe it's only used to establish the induction hypothesis...? Or was the proof supposed to use add_succ? That is,

    theorem succ_add (m n : nat) : succ m + n = succ (m + n) :=
    nat.rec_on n rfl (λ n ih, by simp only [add_succ, ih])
williamdemeo commented 7 years ago

Never mind... it seems okay.