Fib.lean

import Std.Data.Nat.Lemmas
import Std.Tactic.Omega
import Std.Tactic.Simpa

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

def fastfib (n : Nat) := loop n 1 0
where loop n a b :=
  match n with
  | 0 => b
  | n' + 1 => loop n' (a + b) a

@[csimp]
theorem fib_eq_fastfib : @fib = @fastfib := by
  funext n
  unfold fastfib
  have inv (i : Nat) (h : i ≤ n) : fib n = fastfib.loop i (fib (n - i + 1)) (fib (n - i)) := by
    induction i with
    | zero => simp [fastfib.loop]
    | succ i' ih =>
      have n_sub_i' : n - i' = n - Nat.succ i' + 1 := by omega
      have n_sub_i'_add_1 : n - i' + 1 = Nat.succ (Nat.succ (n - Nat.succ i')) := by omega
      simp only [←n_sub_i', fastfib.loop]
      specialize ih (Nat.le_of_succ_le h)
      suffices fib (n - i') + fib (n - Nat.succ i') = fib (n - i' + 1) by simpa [this]
      simp only [←n_sub_i', n_sub_i'_add_1, fib]
  specialize inv n (Nat.le_refl n)
  simp [fib] at inv
  assumption