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

docs#finset.Ico

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

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 (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],
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