induction

Stream: general

[Johan Commelin]

Occasionally I find myself having the goal \forall n, P n that I want to prove by induction. But (as a mathematician) I always allow myself to use P m for all m < n in the induction step. So I would like to rewrite my initial goal into \forall n m, m < n \to P m. Is a statement like that already in mathlib?

[Kenny Lau]

Occasionally I find myself having the goal \forall n, P n that I want to prove by induction. But (as a mathematician) I always allow myself to use P m for all m < n in the induction step. So I would like to rewrite my initial goal into \forall n m, m < n \to P m. Is a statement like that already in mathlib?

strong induction?

[Johan Commelin]

I don't know anything about strong induction. Is that the name for the thing I am talking about?

[Kenny Lau]

it's called strong induction.

#check @nat.strong_induction_on
-- nat.strong_induction_on :
--  ∀ {p : ℕ → Prop} (n : ℕ), (∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) → p n

[Chris Hughes]

Read the section in TPIL on the equation compiler and the docs in mathlib on the equation compiler.