Induction proofs

Stream: new members

[Victor Tsynkov]

My first question. Beware. What is the best way to do an induction proof if the base case is not 0? For example, prove that sum_{i=1}^n (2i-1) = n^2 by induction on n starting with n=1. In this case one can shift and do sum_{j=0} (2j+1) instead. But I'm interested to see how to deal with the original form if possible. Can one still somehow easily use the induction n tactic like in the natural game? Thank you!

[Jalex Stark]

i think reparameterizing so that the induction variable starts at 0 is a good approach.

[Jalex Stark]

do you have example code? (where you managed to make the induction work but you want advice on how to make it cleaner?)

[Kevin Buzzard]

I think the base case for that sum question is n=0 anyway ;-) The empty sum is 0. But in general when I'm in this situation, assuming the base case isn't any larger than 2, I do cases n with n' and then I have to deal with the case n=0 separately, and now we're left with the case n=n'+1, and if my base case is 1 I do induction on n' but if it's bigger than 1 I do cases n' again. There might be some induction theorem in the library which saves you having to do this.

[Kevin Buzzard]

@Victor Tsynkov one thing I find particularly sexy about Lean is that it's possible to rigorously ask your question as a Lean sorry which you want filled in. For example, if you were interested in how to do induction starting from the case n=d you could ask how to fill in the following sorry:

example (P : ℕ → Prop) -- thing you want to prove
  (d : ℕ) -- base
  (hbase : P d)
  (hstep : ∀ m : ℕ, d ≤ m → P m → P (m + 1)) :
  ∀ n : ℕ, d ≤ n → P n :=
begin
  sorry
end

[Kevin Buzzard]

and another thing which is particularly sexy (especially now, given that it just worked) is that you can search the library and see what you need is in there already. And lo:

import tactic

example (P : ℕ → Prop)
  (d : ℕ) -- base
  (hbase : P d)
  (hstep : ∀ m : ℕ, d ≤ m → P m → P (m + 1)) :
  ∀ n : ℕ, d ≤ n → P n :=
begin
  intros n hn,
  library_search,
end

takes a while to run, but comes up with exact nat.le_induction hbase hstep n hn,

[Kevin Buzzard]

So the answer to your question is that you can apply nat.le_induction and what is even cooler is that you learnt that if instead of asking an informal question you can ask a formalised question, then you might be able to use Lean's tactics to find out your own answer :D

nat.le_induction : ∀ {P : ℕ → Prop} {m : ℕ}, P m → (∀ (n : ℕ), m ≤ n → P n → P (n + 1)) → ∀ (n : ℕ), m ≤ n → P n

[Victor Tsynkov]

@Kevin Buzzard @Jalex Stark Thank you both a lot! I didn't know how to actually write the sum in Lean to post working code, let alone how to search for a general induction framework, but this will help me get going.

[Kevin Buzzard]

I didn't write any sum, I just said "let P n be any true/false statement at all".

[Kevin Buzzard]

Working in the biggest generality is somehow the right thing to do here

[Victor Tsynkov]

Finally! I think I got to prove this, thanks to the information in this thread:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computing.20finset.20(range).20sums

Posting this here in case someone else will be interested. The proof starting at one seems quite a bit longer than the other one though!

import algebra.big_operators
import tactic

open_locale big_operators

-- shift terms for a series
def g1 (i : ℕ) : ℕ := 2 * i - 1 -- for i = 1, 2, ...
-- change to
def g2 (j : ℕ) : ℕ := 2 * j + 1  -- now j = 0, 1, 2, ...

--!!! the best way to do it ???
lemma ind_start_one (n : ℕ) : 1 ≤ n → ∑ i in finset.range (n+1), g1 i = n * n :=
begin
    apply nat.le_induction,
    {   -- base case
        rw finset.sum_range_succ g1 1,
        unfold g1,
        have h1 : ∑ i in finset.range 1, g1 i = 0,
            rw finset.sum_range_succ g1 0,
            --simp,
            simp only [add_zero, finset.sum_empty, finset.range_zero],
            unfold g1, norm_num,
        unfold g1 at h1,
        rw h1, norm_num,
    },
    {   -- inductive step
        intros n hn hind,
        rw finset.sum_range_succ g1 (n+1),
        rw hind,
        unfold g1,
        have h : 2 * (n+1) = 2 * n + 2, ring, -- can't do it without this step!
        rw h,
        norm_num, ring,
    },
    done
end

example (n : ℕ) : ∑ i in finset.range n, g2 i = n * n :=
begin
    induction n with d hd,
    {  -- base case n = 0; nothing to sum
        refl,
    },
    { -- inductive case
        have h1 := finset.sum_range_succ g2 d,
        have h2 : d.succ = d + 1, exact nat.succ_eq_add_one d,
        rw h2, rw h1, rw hd,
        unfold g2, ring,
    }
end

[Victor Tsynkov]

But I do have another question.

[Victor Tsynkov]

When trying to use exact instead of apply, these two below seem to be the same. Never mind the sorry, why would exact fail in the second case? It's fed the same terms as far as I can tell.

import algebra.big_operators
import tactic

open_locale big_operators

def g1 (i : ℕ) : ℕ := 2 * i - 1 -- for i = 1, 2, ...

-- go forward
def prd (n : ℕ) : Prop := ∑ i in finset.range (n+1), g1 i = n * n
lemma ind_start_one_forw_1 (n : ℕ) : 1 ≤ n → prd n :=
begin
    -- first show this is true for n = 1
    have hbase : prd 1,
    { sorry, },
    -- then show that ∀ n : ℕ, 1 ≤ n && true for n → true for (n+1)
    have hstep : ∀ m : ℕ, 1 ≤ m → prd m → prd (m+1),
    {
        sorry,
    },
    exact nat.le_induction hbase hstep n, -- this is fine
end

-- some strange behaviour here, not sure what's going on yet
-- isn't this the same as variant _f1 above?
lemma ind_start_one_forw_2 (n : ℕ) : 1 ≤ n → ∑ i in finset.range (n+1), g1 i = n * n :=
begin
    -- first show this is true for n = 1
    have hbase : ∑ i in finset.range (1+1), g1 i = 1 * 1,
    { sorry, },
    -- then show that ∀ m : ℕ, 1 ≤ m && true for m → true for (m+1)
    have hstep : ∀ m : ℕ, 1 ≤ m → ∑ i in finset.range (m+1), g1 i = m * m →
        ∑ i in finset.range (m+2), g1 i = (m+1) * (m+1),
    { sorry, },
    exact nat.le_induction hbase hstep n, -- why would this fail ???
end

[Patrick Massot]

Did you read the error message?

[Victor Tsynkov]

I can't make sense of it.

[Jalex Stark]

Your base case proof did a lot of unnecessary work

lemma ind_start_one (n : ℕ) : 1 ≤ n → ∑ i in finset.range (n+1), g1 i = n * n :=
begin
    apply nat.le_induction,
    {   -- base case
        rw finset.sum_range_succ g1 1, refl,
    },
    {   -- inductive step
        sorry
    },
    done
end

[Kevin Buzzard]

subtraction is poorly behaved on nat so you can expect trouble if you use it, e.g. in the g1 case. The base case is true by definition though:

lemma ind_start_one (n : ℕ) : 1 ≤ n → ∑ i in finset.range (n+1), g1 i = n * n :=
begin
    apply nat.le_induction,
    {   -- base case
        refl
    },
    {   -- inductive step
        intros n hn hind,
        rw finset.sum_range_succ g1 (n+1),
        rw hind,
        unfold g1,
        have h : 2 * (n+1) = 2 * n + 2, ring, -- can't do it without this step!
        rw h,
        norm_num, ring,
    },
    done
end

[Jalex Stark]

what's the error message that you don't understand?

[Jalex Stark]

error messages are one of the key ways that Lean teaches you how to use it

[Kevin Buzzard]

If you read the error message you'll see that you have not fed the correct variables into the function in order to prove the result.

[Patrick Massot]

Also, you can start that proof by apply nat.le_induction.

[Patrick Massot]

(and then refl)

[Victor Tsynkov]

Kevin Buzzard said:

If you read the error message you'll see that you have not fed the correct variables into the function in order to prove the result.

I thought I fed the same variables in both cases. One worked, the other didn't. I'm still confused. It's just getting really late so no more coffee-:(

[Kevin Buzzard]

The error is this:

type mismatch at application
  nat.le_induction hbase hstep
term
  hstep
has type
  ∀ (m : ℕ),
    1 ≤ m →
    ∑ (i : ℕ) in finset.range (m + 1), g1 i = m * m →
    ∑ (i : ℕ) in finset.range (m + 2), g1 i = (m + 1) * (m + 1)
but is expected to have type
  ∀ (n : ℕ),
    1 * 1 ≤ n →
    ∑ (i : ℕ) in finset.range (1 + 1), g1 i = n → ∑ (i : ℕ) in finset.range (1 + 1), g1 i = n + 1

so (replacing n by m in the second one) you have a sum being m*m and it expected it to be m, and you have another sum being (m+1)*(m+1) and Lean expected it to be m+1. This means that either you've made some big error somewhere else, or you've just not fed the right variables in, in the right order.

[Kevin Buzzard]

OK so in fact something a bit more subtle is going on.

[Kevin Buzzard]

nat.le_induction is a function and some of the inputs are explicit, but others are implicit, like P. Lean has to guess P and unfortunately what's happening is that you don't give Lean enough clues, and it's guessing it wrong; it sees hbase and figures that m must be 1 and then incorrectly guesses that all the 1's in hbase are going to be ns in the general case. Can you see that you haven't given Lean enough information to figure out P? There are lots of functions of n such that if you set n=1 they become ∑ i in finset.range (1+1), g1 i = 1 * 1. You want three of those 1s to be ns, but not the fourth one; but Lean has no way of guessing this.

[Kevin Buzzard]

apply nat.le_induction _ hstep works. hstep has got a lot more clues in, and Lean can solve the jigsaw puzzle for P from hstep.

[Kevin Buzzard]

refine nat.le_induction _ hstep n, also works. Basically hbase is poisoned; it misleads the elaborator.

[Kevin Buzzard]

exact @nat.le_induction (λ n, ∑ (i : ℕ) in finset.range (n + 1), g1 i = n * n) _ hbase hstep _, also works. Here we use @ to tell Lean that we're going to input P directly; that way hbase can't confuse the elaborator.

[Victor Tsynkov]

Kevin Buzzard said:

OK so in fact something a bit more subtle is going on.

This makes sense. I had started to think something like this was going on, but I couldn't figure it all out. Thank you for such detailed explanation @Kevin Buzzard

[Kevin Buzzard]

Yes, you were right to be confused, I had just assumed you'd fed the variables in in the wrong order but on closer inspection it was unification failing

[Kevin Buzzard]

This sort of problem is super-hard; Lean has some algorithm which fails in some cases because failure is inevitable in this situation, you can't always guess P. Lean looks at the base case first and makes the wrong guess. If it looked at the step case first it would be OK, but then you'll find examples where looking at the step case gave you the wrong answer