fibonacci using well_founded.fix

gistfile1.txt

definition dcases_on {C : nat → Type} (n : nat) (c₁ : n = 0 → C 0) (c₂ : Πm, n = succ m → C (succ m)) : C n :=
nat.cases_on n
  (λ (H : n = 0), c₁ H)
  (λ (m : nat) (H : n = succ m), c₂ m H) (eq.refl n)

definition fib.F (n : nat) (r : Π (m : nat), m < n → nat) : nat :=
dcases_on n
  (λ (H : n = 0), succ zero)
  (λ (n₁ : nat) (H₁ : n = succ n₁), dcases_on n₁
    (λ (H : n₁ = 0), succ zero)
    (λ (n₂ : nat) (H₂ : n₁ = succ n₂),
      have l₁ : n₁ < n, from H₁⁻¹ ▸ self_lt_succ n₁,
      have l₂ : n₂ < n, from lt_trans (H₂⁻¹ ▸ self_lt_succ n₂) l₁,
      r n₁ l₁ + r n₂ l₂))

definition fib (n : nat) :=
well_founded.fix fib.F n

theorem fib.zero_eq : fib 0 = 1 :=
well_founded.fix_eq fib.F 0

theorem fib.one_eq  : fib 1 = 1 :=
well_founded.fix_eq fib.F 1

theorem fib.succ_succ_eq (n : nat) : fib (succ (succ n)) = fib (succ n) + fib n :=
well_founded.fix_eq fib.F (succ (succ n))