Proof review: Sum of first n Fibonacci terms

Stream: new members

[Huỳnh Trần Khanh]

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]

What is the placeholder for

[Kenny Lau]

obviously f(0) = 0

[Huỳnh Trần Khanh]

I want to count from 1

[Kevin Buzzard]

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

[Damiano Testa]

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]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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