Stream: new members
Topic: Strong induction in lean
Calle Sönne (Nov 19 2018 at 16:14):
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 (Nov 19 2018 at 16:19):
You might want to look at
nat.case_strong_induction_on, which follow the pattern of your second example.
Kevin Buzzard (Nov 19 2018 at 17:20):
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 (Nov 19 2018 at 17:21):
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 (Nov 19 2018 at 18:45):
Ah forgot about that trick, thank you!
Last updated: May 13 2021 at 21:12 UTC