# Zulip Chat Archive

## 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.strong_induction_on`

and `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