## Stream: new members

### Topic: Induction proofs

#### Victor Tsynkov (Jun 16 2020 at 15:41):

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 (Jun 16 2020 at 15:44):

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

#### Jalex Stark (Jun 16 2020 at 15:44):

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 (Jun 16 2020 at 15:52):

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 (Jun 16 2020 at 15:55):

@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 (Jun 16 2020 at 15:57):

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 (Jun 16 2020 at 15:59):

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 (Jun 16 2020 at 16:08):

@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 (Jun 16 2020 at 16:12):

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

#### Kevin Buzzard (Jun 16 2020 at 16:13):

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

#### Victor Tsynkov (Jun 16 2020 at 19:59):

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,
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 (Jun 16 2020 at 19:59):

But I do have another question.

#### Victor Tsynkov (Jun 16 2020 at 20:04):

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 (Jun 16 2020 at 20:05):

Did you read the error message?

#### Victor Tsynkov (Jun 16 2020 at 20:06):

I can't make sense of it.

#### Jalex Stark (Jun 16 2020 at 20:09):

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 (Jun 16 2020 at 20:09):

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 (Jun 16 2020 at 20:10):

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

#### Jalex Stark (Jun 16 2020 at 20:11):

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

#### Kevin Buzzard (Jun 16 2020 at 20:12):

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 (Jun 16 2020 at 20:14):

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

#### Patrick Massot (Jun 16 2020 at 20:14):

(and then refl)

#### Victor Tsynkov (Jun 16 2020 at 21:07):

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 (Jun 16 2020 at 21:50):

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 (Jun 16 2020 at 21:52):

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

#### Kevin Buzzard (Jun 16 2020 at 21:56):

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 (Jun 16 2020 at 21:56):

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 (Jun 16 2020 at 22:00):

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

#### Kevin Buzzard (Jun 16 2020 at 22:02):

 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 (Jun 17 2020 at 10:37):

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 (Jun 17 2020 at 10:38):

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 (Jun 17 2020 at 10:40):

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

Last updated: May 11 2021 at 00:31 UTC