Zulip Chat Archive

Stream: new members

Topic: beginner proof by induction question


view this post on Zulip Bryan Gin-ge Chen (Aug 30 2018 at 03:52):

I'm trying to prove that k=0n1Fk=F2k1 \sum_{k=0}^{n-1}F_k = F_{2k-1} , where FkF_{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,
add_comm, nat.succ_eq_add_one, mul_add],
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.

view this post on Zulip Kenny Lau (Aug 30 2018 at 05:19):

what you wrote at the beginning of this message is false

view this post on Zulip Kenny Lau (Aug 30 2018 at 05:29):

also what you stated in your lean code is false

view this post on Zulip 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

view this post on Zulip 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,
  rw [nat.add_sub_assoc],
  change _ = fibonacci (2 * n + 1) - 1,
  unfold fib_even_sum,
  rw [finset.sum_range_succ],
  induction n with n ih, {refl},
  rw [finset.sum_range_succ, ih, add_comm],
  change fibonacci (2*n+1) - 1 + fibonacci (2*n+2) = fibonacci (2*n+3) - 1,
  rw [ nat.sub_add_comm], refl,
  { clear ih,
    induction n with n ih, {refl},
    change 1  fibonacci (2*n+3),
    unfold fibonacci,
    transitivity, {exact ih},
    apply nat.le_add_right },
  from dec_trivial
end

view this post on Zulip 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.

view this post on Zulip 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,
rw [finset.sum_range_succ, f1, sum_odd_fib_eq_fib_double, add_comm],
refl
end

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

view this post on Zulip Patrick Massot (Aug 30 2018 at 12:33):

We will soon have tools to avoid such kind of mistakes

view this post on Zulip Kevin Buzzard (Aug 30 2018 at 12:37):

You mean Kenny?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 30 2018 at 13:09):

is there any documentation explaining how to use it?

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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,
rw [finset.sum_range_succ, f1, add_assoc, add_comm, f2, add_comm, nat.succ_eq_add_one, mul_add, add_comm],
change fibonacci (2 * n + 1) + fibonacci (2 * n + 2) = fibonacci (2 * n + 3),
refl
end

view this post on Zulip Bryan Gin-ge Chen (Aug 30 2018 at 16:17):

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

view this post on Zulip 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, Fn+12FnFn+2=(1)nF_{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
  rw [add_comm, sub_eq_add_neg, neg_add,
  add_assoc, add_comm, mul_comm,
  add_assoc, add_assoc, neg_add_self, zero_add],
  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),
  rw [mul_add, mul_add, int.coe_nat_add],
  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.

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:06):

abcde is by ring

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:07):

don't forget import tactic.ring at top

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2018 at 20:11):

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

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:11):

works here

view this post on Zulip Chris Hughes (Sep 04 2018 at 20:11):

Did you import tactic.ring?

view this post on Zulip Patrick Massot (Sep 04 2018 at 20:12):

Chris, can you also golf my limit computation?

view this post on Zulip Chris Hughes (Sep 04 2018 at 20:13):

Probably not. I know nothing about analysis in lean.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 04 2018 at 20:25):

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Sep 04 2018 at 20:27):

Thanks, that's very helpful!


Last updated: May 15 2021 at 23:13 UTC