auxiliary lemma for induction

Stream: general

[Kevin Buzzard]

structure foo :=
(size : ℕ)

definition auxiliary_thing (p : foo → Sort*) (m : ℕ)
(H0 : ∀ x : foo, x.size = 0 → p x)
(Hsucc : ∀ n : ℕ,
  (∀ x : foo, x.size = n → p x) → (∀ x : foo, x.size = n+1 → p x)) :
∀ x : foo, x.size = m → p x :=
begin
  induction m with n Hn,
    exact H0,
  exact Hsucc n Hn,
end

/- What I actually want -/
definition foo.recurse_on_size (p : foo → Sort*)
(H0 : ∀ x : foo, x.size = 0 → p x)
(Hsucc : ∀ n : ℕ,
  (∀ x : foo, x.size = n → p x) → (∀ x : foo, x.size = n+1 → p x)) :
∀ x : foo, p x :=
begin
  intro x,
  apply auxiliary_thing p (x.size) H0 Hsucc,
  refl,
end

Is this introduction of an auxiliary lemma a sensible way to go about things, or am I better off trying to prove what I want directly using some fancy equation compiler trickery?

[Simon Hudon]

Are you using the auxiliary lemma in order to have m to do your induction on? Have you tried generalize h : x.size = m, induction m with n Hn?

[Kevin Buzzard]

Aah that's the trick. Thanks Simon!

[Simon Hudon]

Any time :)

[Simon Hudon]

I wonder if it would be worth combining the two tactics so that induction e (with e an arbitrary expression) would produce the equality assumption.