## Stream: new members

### Topic: beginner proof by induction question

#### Bryan Gin-ge Chen (Aug 30 2018 at 03:52):

I'm trying to prove that $\sum_{k=0}^{n-1}F_k = F_{2k-1}$, where $F_{k}$ is the kth Fibonacci number. Here's my attempt so far:

import algebra.big_operators

def fibonacci : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fibonacci n + fibonacci (n+1)

def fib_even_sum : ℕ → ℕ := λ n, (finset.range n).sum (λ m, fibonacci (2*m))

theorem sum_even_fib_eq_fib_double_sub_one: ∀ (n : ℕ),
fib_even_sum n = fibonacci (2*n - 1)
| 0 := rfl
| (nat.succ n) :=
have f1 : (finset.range n).sum (λ m, fibonacci (2*m)) = fib_even_sum n, by refl,
begin
unfold fib_even_sum,
rw [finset.sum_range_succ, f1, sum_even_fib_eq_fib_double_sub_one,
sorry
end


As you can see, my goal looks like this:

⊢ fibonacci (2 * n - 1) + fibonacci (2 * n) = fibonacci (2 * n + 2 * 1 - 1)


But I can't figure out how to simplify 2*n + 2*1 -1 inside fibonacci to 2*n - 1. If I could do that then I would happily finish with refl.

Other style or efficiency suggestions would also be appreciated. Is there a smart way to apply simp? I haven't managed that either.

#### Kenny Lau (Aug 30 2018 at 05:19):

what you wrote at the beginning of this message is false

#### Kenny Lau (Aug 30 2018 at 05:29):

also what you stated in your lean code is false

#### Kenny Lau (Aug 30 2018 at 05:30):

import algebra.big_operators

def fibonacci : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fibonacci n + fibonacci (n+1)

def fib_even_sum : ℕ → ℕ := λ n, (finset.range n).sum (λ m, fibonacci (2*m))

theorem not_sum_even_fib_eq_fib_double_sub_one: ¬∀ (n : ℕ),
fib_even_sum n = fibonacci (2*n - 1) :=
λ H, absurd (H 1) dec_trivial


#### Kenny Lau (Aug 30 2018 at 06:10):

import algebra.big_operators

def fibonacci : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fibonacci n + fibonacci (n+1)

def fib_even_sum : ℕ → ℕ := λ n, (finset.range n).sum (λ m, fibonacci (2*m))

theorem sum_even_fib_eq_fib_double_sub_three (n : ℕ) :
fib_even_sum n = fibonacci (2*n - 1) - 1 :=
begin
cases n with n, {refl},
change _ = fibonacci (2 * n + 2 - 1) - 1,
change _ = fibonacci (2 * n + 1) - 1,
unfold fib_even_sum,
rw [finset.sum_range_succ],
induction n with n ih, {refl},
change fibonacci (2*n+1) - 1 + fibonacci (2*n+2) = fibonacci (2*n+3) - 1,
{ clear ih,
induction n with n ih, {refl},
change 1 ≤ fibonacci (2*n+3),
unfold fibonacci,
transitivity, {exact ih},
from dec_trivial
end


#### Kevin Buzzard (Aug 30 2018 at 11:30):

Note that your goal about fibonacci (2 * n - 1) + fibonacci (2 * n) = fibonacci (2 * n + 2* 1 - 1) is false if n = 0, because 0 - 1 = 0.

#### Bryan Gin-ge Chen (Aug 30 2018 at 12:21):

Ah, thanks! That was really silly of me... I got lazy because I had previously proved this:

def odd : ℕ → ℕ := λ n, 2*n+1

def fib_odd_sum : ℕ → ℕ := λ n, (finset.range n).sum (λ m, fibonacci (odd m))

theorem sum_odd_fib_eq_fib_double : ∀ (n : ℕ),
fib_odd_sum n = fibonacci (2*n)
| 0 := rfl
| (nat.succ n) :=
have f1 : (finset.range n).sum (λ m, fibonacci (odd m)) = fib_odd_sum n, by refl,
begin
unfold fib_odd_sum,
refl
end


and I just wanted to copy and paste stuff. Granted, I should still have checked what I was trying to prove...

#### Patrick Massot (Aug 30 2018 at 12:33):

We will soon have tools to avoid such kind of mistakes

You mean Kenny?

#### Patrick Massot (Aug 30 2018 at 12:41):

I mean the tactic sanity_check that Rob showed in Orsay, Simon's SlimCheck, and Nunchaku in Lean

#### Johannes Hölzl (Aug 30 2018 at 13:05):

You find Pablo's Nunchaku-Lean prototype in https://gitlab.binets.fr/pablo.le-henaff/nunchaku-lean

#### Johannes Hölzl (Aug 30 2018 at 13:06):

it doesn't yet implement the dependent type as proposed by the arxiv paper, but hopefully in the future it does

#### Patrick Massot (Aug 30 2018 at 13:09):

is there any documentation explaining how to use it?

#### Johannes Hölzl (Aug 30 2018 at 13:23):

Not yet. It is only a prototype. Currently, it doesn't even have a leanpkg.toml.
What should work is:

import nunchaku

example (n : nat) : n > 1  := by nunchaku


and it should report n = 0 as counterexample.

#### Patrick Massot (Aug 30 2018 at 14:44):

Thanks. I guess I'll need to see more documentation (including how to install all the dependencies)

#### Bryan Gin-ge Chen (Aug 30 2018 at 16:16):

Returning to my original problem, here's my fixed up proof:

import algebra.big_operators

def fibonacci : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := fibonacci n + fibonacci (n+1)

def fib_even_sum : ℕ → ℕ := λ n, (finset.range n).sum (λ m, fibonacci (2*m))

lemma succ_gt_zero (n : ℕ): nat.succ n > 0 := dec_trivial

theorem sum_even_fib_eq_fib_double_sub_one: ∀ (n : ℕ),
n>0 → fib_even_sum n + 1 = fibonacci (2*n - 1)
| 0 := begin
intro h,
exact false.elim ((gt_irrefl 0) h)
end
| 1 := begin
intro h,
refl
end
| (nat.succ (n+1)) :=
have f1 : (finset.range (n+1)).sum (λ m, fibonacci (2*m)) = fib_even_sum (n+1), by refl,
have f2 : fib_even_sum (n+1) + 1 = fibonacci (2*(n+1) - 1), by exact sum_even_fib_eq_fib_double_sub_one (n+1) (succ_gt_zero n),
begin
intro h,
unfold fib_even_sum,
change fibonacci (2 * n + 1) + fibonacci (2 * n + 2) = fibonacci (2 * n + 3),
refl
end


#### Bryan Gin-ge Chen (Aug 30 2018 at 16:17):

Thanks to Kenny for his proof as well, which was very instructive.

#### Bryan Gin-ge Chen (Sep 04 2018 at 20:04):

If anyone has a strong stomach, I'd appreciate feedback on this ugly proof of yet another silly Fibonacci fact (this time, $F_{n+1}^2-F_nF_{n+2}=(-1)^n$):

import algebra.big_operators algebra.group_power

def F : ℕ → ℕ
| 0 := 0
| 1 := 1
| (n+2) := F n + F (n+1)

variables (a b c d e:ℤ)
lemma abcde : a*b + c*d - (e + d*c) = (-1)*(e - b*a) :=
begin
simp [mul_comm]
end

open nat

variable n : ℕ
local notation [parsing_only] F_n := ↑(F n)
local notation [parsing_only] F_n1 := ↑(F (succ n))
local notation [parsing_only] F_n2 := ↑(F (succ n+1))

theorem ex10 : ((F (n+1) ^ 2):ℤ) - (F n) * (F (n+2)) = (-1) ^ n :=
begin
induction n with n ih, {refl},
unfold pow monoid.pow,
unfold pow monoid.pow at ih,
rw [←ih, mul_one, mul_one],
change ↑((F (succ n + 1)) * (F n + F (succ n)))
- (F_n1 * (F_n1 + F_n2))
= (-1:ℤ) * (F_n1 * F_n1 - F_n * F_n2),
change F_n2 * F_n + F_n2 * F_n1
-(F_n1 * F_n1 + F_n1 * F_n2)
= (-1:ℤ) * (F_n1 * F_n1 - F_n * F_n2),
rw [abcde]
end


Is there a better tactic to use for proving abcde (or better, getting around it entirely)? Constructing these long sequences of rws is very tiresome but I don't have a good idea of when I can throw in simp.

#### Patrick Massot (Sep 04 2018 at 20:06):

abcde is by ring

#### Patrick Massot (Sep 04 2018 at 20:07):

don't forget import tactic.ring at top

#### Chris Hughes (Sep 04 2018 at 20:08):

theorem ex10 : ((F (n+1) ^ 2):ℤ) - (F n) * (F (n+2)) = (-1) ^ n :=
begin
induction n with n ih,
{ refl },
{ simp [F, _root_.pow_succ, ih.symm],
ring },
end


#### Bryan Gin-ge Chen (Sep 04 2018 at 20:09):

Ah, right. I could have sworn I tried that..

Indeed, I can just delete abcde entirely and finish with ring.

#### Bryan Gin-ge Chen (Sep 04 2018 at 20:11):

@Chris Hughes that's not working for me, unfortunately...

works here

#### Chris Hughes (Sep 04 2018 at 20:11):

Did you import tactic.ring?

#### Patrick Massot (Sep 04 2018 at 20:12):

Chris, can you also golf my limit computation?

#### Chris Hughes (Sep 04 2018 at 20:13):

Probably not. I know nothing about analysis in lean.

#### Bryan Gin-ge Chen (Sep 04 2018 at 20:14):

OK, it works now. I had some other notation in my main file that was interfering somehow.

#### Bryan Gin-ge Chen (Sep 04 2018 at 20:24):

@Chris Hughes If you don't mind, could you explain your thought process when you came up with that? For instance, did you peek at my ugly proof first, or did those lemmas immediately jump into your head.

Is the take-away that simp, then ringshould be my go-to for this sort of thing?

#### Mario Carneiro (Sep 04 2018 at 20:25):

ring does equalities between ring expressions, i.e. addition, subtraction, multiplication and powers by constants

#### Chris Hughes (Sep 04 2018 at 20:26):

I used your proof a little bit, to see that I needed induction. Other than that, it's just unfold everything, find some way of substituting in the induction hypothesis, and then hope ring works.