Efficient_Fibonacci.v

Require Import Omega.

Fixpoint fib (n : nat) :=
  match n with
  | 0 => 1
  | S n' => match n' with
            | 0 => 1
            | S n'' => fib n' + fib n''
            end
  end.

Fixpoint fib_tail' (n a b : nat) : nat :=
  match n with
  | 0 => b
  | S n' => fib_tail' n' (a + b) a
  end.

Definition fib_tail (n : nat) :=
  fib_tail' n 1 1.

Lemma fib_tail'_correct:
  forall n k,
    k <= n -> fib_tail' k (fib (S n - k)) (fib (n - k)) = fib n.
Proof.
  induction k; intros.
  - simpl. f_equal. omega.
  - simpl. rewrite <- IHk; try omega.
    f_equal. replace (S n - k) with (S (n - k)) by omega.
    simpl. assert (n - k >= 1) by omega.
    case_eq (n - k); intros; try omega.
    replace (n - S k) with n0 by omega.
    reflexivity.
Qed.

Theorem fib_tail_correct :
  forall n,
    fib_tail n = fib n.
Proof.
  intros. unfold fib_tail.
  replace 1 with (fib (S n - n)) at 1.
  replace 1 with (fib (n - n)).
  eapply fib_tail'_correct; omega.
  replace (n - n) with 0 by omega; reflexivity.
  replace (S n - n) with (S 0) by omega; reflexivity.
Qed.