Hints on double Induction with le_induction

Stream: new members

[Newell Jensen]

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]

double induction is usually just an induction inside another one

[Newell Jensen]

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]

Will try nested induction for now (not sure on the le_induction part though)

[Kevin Buzzard]

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]

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]

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]

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]

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)

import tactic

open_locale big_operators

open finset

lemma helper_lemma (c : ℚ) :
  ∀ m, ∑ i in range (m + 1), (c + i) = (2 * c + m) * (m + 1) / 2 :=
begin
  ...
end

example (m n : ℕ) : (∑ i in range (m + 1), ∑ j in range (n + 1), (i + j : ℚ)) =
(m + 1) * (n + 1) * (m + n) / 2 :=
begin
  simp_rw helper_lemma,
  ...
end

The proofs

import tactic

open_locale big_operators

open finset

lemma helper_lemma (c : ℚ) :
  ∀ m, ∑ i in range (m + 1), (c + i) = (2 * c + m) * (m + 1) / 2 :=
begin
  intro m,
  induction m with d hd,
  { simp, ring, },
  { rw [sum_range_succ, hd],
    simp, ring, },
end


example (m n : ℕ) : (∑ i in range (m + 1), ∑ j in range (n + 1), (i + j : ℚ)) =
(m + 1) * (n + 1) * (m + n) / 2 :=
begin
  simp_rw helper_lemma,
  induction m with d hd,
  { simp, ring, },
  { rw [sum_range_succ, hd],
    simp, ring, },
end

[Chris Birkbeck]

maybe docs#nat.sub_induction might also be useful

[Chris Birkbeck]

and also docs#nat.strong_sub_recursion

[Vincent Beffara]

Or perhaps something like docs#well_founded.induction on NxN

[Newell Jensen]

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]

Yes, so range n is {0, 1, ..., n - 1}, not {1, ..., n}

[Mauricio Collares]

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]

yes, was just noticing this actually

[Newell Jensen]

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

[Yaël Dillies]

docs#finset.Ico

[Newell Jensen]

Kevin Buzzard said:

(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)

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]

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]

Might as well add it to mathlib now ;)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Newell Jensen]

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