# Zulip Chat Archive

## Stream: new members

### Topic: Hints on double Induction with le_induction

#### Newell Jensen (Sep 20 2022 at 02:06):

Looking through `mathlib`

, I haven't been able to find double induction. Any suggestions on double induction using `le_induction`

(starting from 1 for both indices as seen in the hypotheses)? Doesn't seem like there is a double index variant of `le_induction`

. The code below is what I am trying to prove. I don't need anyone to actually prove this for me as I would like to do it myself and just looking for some hints to help me along.

```
import tactic
open_locale big_operators
example (m n : ℕ) (h₁ : 1 ≤ m) (h₂ : 1 ≤ n) :
(∑ i in finset.range (m + 1), ∑ j in finset.range (n + 1), (i + j)) =
(m * n * (m + n + 2)) / 2 :=
begin
apply nat.le_induction, -- this is for one index
{ sorry },
{ sorry },
{ sorry },
{ sorry },
end
```

#### Mario Carneiro (Sep 20 2022 at 02:08):

double induction is usually just an induction inside another one

#### Newell Jensen (Sep 20 2022 at 02:09):

Mario Carneiro said:

double induction is usually just an induction inside another one

Maybe I am just being blind but do you know of any examples in the code base where this is happening so I can use it as an example?

#### Newell Jensen (Sep 20 2022 at 03:12):

Will try nested induction for now (not sure on the `le_induction`

part though)

#### Kevin Buzzard (Sep 20 2022 at 06:48):

I would formalise the statement like this:

```
example (m n : ℕ) (h₁ : 1 ≤ m) (h₂ : 1 ≤ n) :
(∑ i in finset.range (m + 1), ∑ j in finset.range (n + 1), (i + j : ℚ)) =
(m * n * (m + n + 2)) / 2 :=
```

because then you are doing the mathematically correct division, not "division with remainder", which is worse to work with.

#### Kevin Buzzard (Sep 20 2022 at 06:50):

```
import tactic
import tactic.slim_check
open_locale big_operators
example (m n : ℕ) (h₁ : 1 ≤ m) (h₂ : 1 ≤ n) :
(∑ i in finset.range (m + 1), ∑ j in finset.range (n + 1), (i + j)) =
(m * n * (m + n + 2)) / 2 :=
begin
slim_check,
/-
===================
Found problems!
m := 1
n := 1
guard: 1 ≤ 1
guard: 1 ≤ 1
issue: 4 = 2 does not hold
(0 shrinks)
-------------------
-/
end
```

Your statement as it stands appears to be wrong (with or without the coercion to rationals). Just to be clear: `finset.range n`

is 0<=j<n.

#### Kevin Buzzard (Sep 20 2022 at 07:09):

```
example (m n : ℕ) : (∑ i in finset.range (m + 1), ∑ j in finset.range (n + 1), (i + j : ℚ)) =
(m + 1) * (n + 1) * (m + n) / 2 :=
```

I think this is the correct statement (and I've dropped the hypotheses that m,n>=1 as I don't think they're necessary)

#### Kevin Buzzard (Sep 20 2022 at 07:15):

My instinct for the proof would not be to just launch into Mario's strategy (a single induction) until you're absolutely clear on precisely which statement in one variable you want to prove by induction (the statement you want to prove has two variables). I am not sure that there's just one "double induction" -- can you say precisely which inductive principle you want to use? The following would be an interesting experiment:

(1) state *in Lean* what you mean by "double induction" (hopefully in a form strong enough to prove your example mathematically)

(2) Assume your induction principle and `apply`

it to prove your example

(3) prove your double induction principle (it will be easier to prove a more abstract statement than to prove the special case we have here)

#### Kevin Buzzard (Sep 20 2022 at 07:38):

OK so I have a relatively straightforward proof using only single induction, using a "helper lemma". I'll post a hint and a solution as spoilers.

Hint (helper lemma statement)

The proofs

#### Chris Birkbeck (Sep 20 2022 at 08:25):

maybe docs#nat.sub_induction might also be useful

#### Chris Birkbeck (Sep 20 2022 at 08:28):

and also docs#nat.strong_sub_recursion

#### Vincent Beffara (Sep 20 2022 at 08:46):

Or perhaps something like docs#well_founded.induction on NxN

#### Newell Jensen (Sep 20 2022 at 19:20):

Kevin Buzzard said:

Your statement as it stands appears to be wrong (with or without the coercion to rationals). Just to be clear:

`finset.range n`

is 0<=j<n.

From *Handbook of Mathematical Induction - Theory and Applications*, Theorem 3.5.1 on page 44 states:

**Theorem 3.5.1.** *Let positive integers m and n be given.*

$\sum_{i=1}^m \sum_{j=1}^n (i + j) = \dfrac{mn(m + n + 2)}{2}.$

The textbook then proceeds to give a proof of this using double induction. Yes, that is why the range was bumped up to `m + 1`

and `n + 1`

, so that it would actually be summing up to `m`

and `n`

.

#### Yaël Dillies (Sep 20 2022 at 19:22):

Yes, so `range n`

is `{0, 1, ..., n - 1}`

, not `{1, ..., n}`

#### Mauricio Collares (Sep 20 2022 at 19:32):

Bumping to `m+1`

and `n+1`

sums from 0 to m and from 0 to n, and the terms where either i = 0 or j = 0 matter.

#### Newell Jensen (Sep 20 2022 at 19:33):

yes, was just noticing this actually

#### Newell Jensen (Sep 20 2022 at 19:33):

Seems I need to find a range that can start from 1

#### Yaël Dillies (Sep 20 2022 at 19:38):

#### Newell Jensen (Sep 20 2022 at 19:40):

Kevin Buzzard said:

(1) state

in Leanwhat you mean by "double induction" (hopefully in a form strong enough to prove your example mathematically)

(2) Assume your induction principle and`apply`

it to prove your example

(3) prove your double induction principle (it will be easier to prove a more abstract statement than to prove the special case we have here)

Well last night late before bed I was playing around with (3) even before I read your comment and came up with this. I just got to my computer so haven't tried proving it yet.

```
@[elab_as_eliminator] lemma le_double_induction {P : nat → nat → Prop} {l}
(h0 : P l l) (h1 : ∀m, P m l → P (m + 1) l) (h2 : ∀m n, P m n → P m (n + 1)) :
∀m n, l ≤ m → l ≤ n → P m n :=
begin
sorry,
end
```

This is the method of double induction that I was going for at least (as there are several different ways of doing it). So yes, if I was able to have a proof of this, then I could apply it (your (2) above) and then go from there solving the pieces.

#### Mario Carneiro (Sep 20 2022 at 19:47):

```
import data.nat.basic
@[elab_as_eliminator] lemma le_double_induction {P : nat → nat → Prop} {l}
(h0 : P l l) (h1 : ∀m, P m l → P (m + 1) l) (h2 : ∀m n, P m n → P m (n + 1)) :
∀m n, l ≤ m → l ≤ n → P m n :=
λ m n hm hn, begin
refine nat.le_induction _ (λ m h, h2 _ _) _ hn,
exact nat.le_induction h0 (λ n h, h1 _) _ hm
end
```

#### Newell Jensen (Sep 20 2022 at 19:49):

Might as well add it to mathlib now ;)

#### Mario Carneiro (Sep 20 2022 at 19:57):

well you can see what I meant by "use `le_induction`

twice"

#### Mario Carneiro (Sep 20 2022 at 19:58):

every subproof comes up exactly once so I don't see a big reason to have the lemma

#### Newell Jensen (Sep 21 2022 at 05:27):

Almost there but having a hard time on the last part. Suggestions?

```
import tactic
import algebra.big_operators.intervals
open_locale big_operators
@[elab_as_eliminator] lemma le_double_induction {P : nat → nat → Prop} {l}
(h0 : P l l) (h1 : ∀m, P m l → P (m + 1) l) (h2 : ∀m n, P m n → P m (n + 1)) :
∀m n, l ≤ m → l ≤ n → P m n :=
λ m n hm hn, begin
refine nat.le_induction _ (λ m h, h2 _ _) _ hn,
exact nat.le_induction h0 (λ n h, h1 _) _ hm
end
example (m n : ℕ) : 1 ≤ m → 1 ≤ n → (∑ i in finset.Ico 1 (m + 1),
∑ j in finset.Ico 1 (n + 1), (i + j)) = (m * n * (m + n + 2)) / 2 :=
begin
apply le_double_induction,
{ refl },
{ intros m h1,
simp at *,
have h2 : ∑ (x : ℕ) in finset.Ico 1 (m + 1 + 1), (x + 1) =
(∑ (x : ℕ) in finset.Ico 1 (m + 1), (x + 1)) + (m + 2),
{ rw finset.sum_Ico_succ_top, linarith },
rw [h2, h1, mul_add (m + 1) (m + 1 + 1) 2, nat.add_div_of_dvd_left,
nat.mul_div_cancel, mul_add (m + 1) m 2, nat.add_div_of_dvd_left,
nat.mul_div_cancel, mul_add m (m + 1) 2, nat.add_div_of_dvd_left,
nat.mul_div_cancel],
ring_nf,
repeat { simp }
},
{
intros m n h3,
have h4 : ∑ (i : ℕ) in finset.Ico 1 (m + 1),
∑ (j : ℕ) in finset.Ico 1 (n + 1 + 1), (i + j) =
∑ (i : ℕ) in finset.Ico 1 (m + 1), ∑ (j : ℕ) in finset.Ico 1 (n + 1),
(i + j) + m * (n + 1) + m * (m + 1) / 2,
{ -- want to do `rw finset.sum_Ico_succ_top` like above but
-- it gets applied to `1 (m + 1)` and not the `1 (n + 1 + 1)`
-- like I would like, any suggestions?
sorry },
sorry,
}
end
```

Last updated: Dec 20 2023 at 11:08 UTC