Induction on sum of parameters

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

Hi,

very basic question but, if I want to prove theorem F (m n : Nat): P m n by induction on m+n, is there a tactic or trick that allows this without changing the theorem statement or creating an auxiliary lemma? I can imagine how reformulating to theorem F (m n N: Nat) (h: m+n = N): P m n and then doing induction on N would work. But can this be avoided?

[Eric Wieser]

induction h : m + n?

[Bernardo Anibal Subercaseaux Roa]

I tried

lemma euclid_algo_symmetric (m n : Nat) : euclid_algo m n = euclid_algo n m := by
  induction h : m + n

but get unknown identifier 'h' and also

tactic 'induction' failed, major premise type is not an inductive type
  ?m.57616
mn: ℕ
x✝: ?m.57616
⊢ euclid_algo m n = euclid_algo n m

Am I doing something wrong?

[Eric Wieser]

Maybe this only works with induction'

[Bernardo Anibal Subercaseaux Roa]

that did work! Thanks! is there a simple explanation of the difference between induction and induction'? or some resource I should check?

[Kevin Buzzard]

induction' is on the way out, is the main difference. Although maybe it just got a reprieve :-)

[Mario Carneiro]

you can do generalize e : m + n = mn; induction mn generalizing m n

[Trevor Hyde]

(deleted)