## Stream: general

### Topic: auxiliary lemma for induction

#### Kevin Buzzard (Aug 23 2018 at 12:07):

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 (Aug 23 2018 at 13:32):

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 (Aug 23 2018 at 13:46):

Aah that's the trick. Thanks Simon!

Any time :)

#### Simon Hudon (Aug 23 2018 at 14:02):

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.

Last updated: Aug 03 2023 at 10:10 UTC