Fibonacci

Stream: maths

[adem bizid]

I have been struggling to prove that two fibonacci functions defined differently are equal. I used these two different ways of defining fibonacci:

def fib (n:Nat): Nat :=
  match n with
  | 0=> 0
  | 1=>1
  | n+2 => fib (n) + fib (n+1)

def fib1 (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 =>
    let rec loop : Nat → Nat → Nat → Nat
      | 0, _, b => b
      | m + 1, a, b => loop m b (a + b)
    loop n 1 1

I tried using the help of AI but there is always errors. Is it possible to prove such statement?
Thanks in advance for the help.

[Kyle Miller]

I got it with some helper lemmas:

def fib (n:Nat): Nat :=
  match n with
  | 0=> 0
  | 1=>1
  | n+2 => fib (n) + fib (n+1)

def fib1 (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | 1 => 1
  | n + 2 =>
    let rec loop : Nat → Nat → Nat → Nat
      | 0, _, b => b
      | m + 1, a, b => loop m b (a + b)
    loop n 1 1

theorem fib1_loop_add (n a b c d : Nat) :
    fib1.loop n a b + fib1.loop n c d = fib1.loop n (a + c) (b + d) := by
  induction n generalizing a b c d with
  | zero => rfl
  | succ n ih =>
    simp only [fib1.loop, ih]
    congr 1
    omega

theorem fib1_rule (n : Nat) : fib1 (n + 2) = fib1 n + fib1 (n + 1) := by
  obtain _ | _ | n := n
  · rfl
  · rfl
  · simp only [fib1, fib1.loop, Nat.reduceAdd, fib1_loop_add]

theorem fib_eq_fib1 (n : Nat) : fib n = fib1 n := by
  induction n using Nat.strongRecOn with
  | _ n ih =>
    obtain _ | _ | n := n
    · rfl
    · rfl
    · rw [fib, ih n (by omega), ih (n + 1) (by omega)]
      rw [← fib1_rule]

[Andrew Yang]

This is also a useful one

theorem fib1.loop_invariant : fib1.loop i (fib j) (fib (j + 1)) = fib (i + j + 1)