Zulip Chat Archive

Stream: new members

Topic: Proof review: Sum of first n Fibonacci terms


Huỳnh Trần Khanh (Jan 14 2021 at 08:49):

The Lean community is awesome! Thanks to your help, now I'm able to complete this proof. Suggestions welcome.

import data.nat.basic
import data.real.basic

def placeholder := 998244353

def fibonacci :   
  | 0 := placeholder
  | 1 := 1
  | 2 := 1
  | (n + 1) := have n - 1 < n + 1 := nat.sub_lt_succ n 1, fibonacci n + fibonacci (n - 1)

def fibonacci_sum :   
  | 0 := placeholder
  | 1 := fibonacci 1
  | (n + 1) := fibonacci_sum n + fibonacci (n + 1)

lemma closed_form { n :  } : 0 < n  fibonacci (n + 2) - 1 = fibonacci_sum n := begin
  intro bound,

  cases n,
  {
    exact absurd bound (lt_irrefl 0),
  },
  {
    induction n with n induction_hypothesis,
    {
      norm_num [fibonacci, fibonacci_sum],
    },
    {
      norm_num [fibonacci_sum],
      rw (induction_hypothesis (nat.succ_pos n)).symm,

      rw fibonacci,
      norm_num,
      ring,
    }
  }
end

Kenny Lau (Jan 14 2021 at 08:51):

What is the placeholder for

Kenny Lau (Jan 14 2021 at 08:52):

obviously f(0) = 0

Huỳnh Trần Khanh (Jan 14 2021 at 08:52):

I want to count from 1

Kevin Buzzard (Jan 14 2021 at 08:52):

That's fine but if you choose the correct value for zero then your proofs will be easier

Damiano Testa (Jan 14 2021 at 08:52):

In line with Kenny's comment, why do you not define fibonacci as

def fibonacci :   
  | 0 := 0
  | 1 := 1
  | (n + 1) := have n - 1 < n + 1 := nat.sub_lt_succ n 1, fibonacci n + fibonacci (n - 1)

?

Kenny Lau (Jan 14 2021 at 08:53):

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

Kyle Miller (Jan 14 2021 at 22:13):

Here's a slow proof with omega, using fibonacci defined with values in the naturals:

import data.nat.basic
import tactic

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

def fibonacci_sum :   
| 0 := 0
| (n + 1) := fibonacci_sum n + fibonacci (n + 1)

lemma fibonacci_succ_pos (n : ) : 0 < fibonacci n.succ :=
begin
  induction n with n induction_hypothesis,
  { exact nat.one_pos, },
  { dsimp [fibonacci],
    apply nat.lt_add_left,
    exact induction_hypothesis, },
end

lemma closed_form {n : } : fibonacci_sum n = fibonacci (n + 2) - 1 :=
begin
  induction n with n induction_hypothesis,
  { refl, },
  { dsimp [fibonacci_sum],
    rw induction_hypothesis,
    dsimp [fibonacci],
    have h := fibonacci_succ_pos n,
    omega, },
end

Bryan Gin-ge Chen (Jan 14 2021 at 22:21):

I have a proof of a variant statement here too (originally written for an Observable notebook on Lean).

Kyle Miller (Jan 14 2021 at 22:30):

Subtraction for naturals is hard to deal with, so if you can make it be in terms of addition you can sometimes find simpler proofs:

import data.nat.basic

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

def fibonacci_sum :   
| 0 := 0
| (n + 1) := fibonacci (n + 1) + fibonacci_sum n

lemma closed_form {n : } : fibonacci_sum n + 1 = fibonacci (n + 2) :=
begin
  induction n with n induction_hypothesis,
  { refl, },
  { dsimp [fibonacci_sum],
    rw [add_assoc, induction_hypothesis],
    refl, },
end

Last updated: Dec 20 2023 at 11:08 UTC