## 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],
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],