Strong induction in lean

Stream: new members

[Calle Sönne]

I want to prove strong induction in lean but Im having a hard time writing it out. Is it possible to do and-statements of variable length in lean? Something like this is what I want to do in lean:

theorem strong_induction (P : ℕ → Prop) (H0 : P 0) (Hn : ∀
    (n : ℕ), P 1 ∧ P 2 ∧ ... ∧ P n → P (n+1)) : ∀ m : ℕ, P m := sorry

or maybe like this if that's possible:

theorem strong_induction' (P : ℕ → Prop) (H0 : P 0) (Hn : ∀
    (n : ℕ), P s → P (n+1), ∀ (s:ℕ) (Hs : s ≤ n) : ∀ m : ℕ, P m := sorry

[Rob Lewis]

You might want to look at nat.strong_induction_on and nat.case_strong_induction_on, which follow the pattern of your second example.

[Kevin Buzzard]

theorem strong_induction (P : ℕ → Prop) (H : ∀ n : ℕ, (∀ m : ℕ, m < n → P m) → P n) (n : ℕ) : P n := sorry would be the way I'd formalise it.

[Kevin Buzzard]

Note that the devious case H 0 says that if something is true for all elements of the empty set, then P 0 follows, which is a trick I mentioned in lectures. There is something called "well-founded induction" which works on any set with a well-founded ordering -- for example the naturals, but also many other ordered sets.

[Calle Sönne]

Ah forgot about that trick, thank you!