Zulip Chat Archive

Stream: new members

Topic: Strong induction in lean


view this post on Zulip 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

view this post on Zulip Rob Lewis (Nov 19 2018 at 16:19):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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