fib_manual.v

Require Import Arith.

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

Fixpoint visit_fib_v2 (n a1 a2 : nat) : nat :=
  match n with
  | 0 => a1
  | S n' => (visit_fib_v2 n' a2 (a1 + a2))
  end.

Lemma visit_fib_v2_SS : forall n a0 a1,
    visit_fib_v2 (S (S n)) a0 a1 =
    visit_fib_v2 (S n) a1 (a0 + a1).
Proof. reflexivity. Qed.

Lemma fib_v1_SS : forall n,
    fib_v1 (S (S n)) = fib_v1 (S n) + fib_v1 n.
Proof. reflexivity. Qed.

Lemma fib_v1_eq_fib2_generalized : forall n a0 a1,
  visit_fib_v2 (S n) a0 a1 = a0 * fib_v1 n + a1 * fib_v1 (S n).
Proof.
  intro n. induction n.
(* The `-` symbols can be deleted they indicate a new subgoal *)
  - intros a0 a1.
(* `simpl` can be replaced by several helper lemmas, all of which can be proved by `reflexivity`. *)
    simpl.  
(* the `Search` commands show how to search for lemmas in Coq; we can get rid of them *)
    Search (_ * 0 = 0).
    rewrite Nat.mul_0_r.
    Search (0 + ?x = ?x).
    rewrite Nat.add_0_l.
    Search (?x * 1 = ?x).
    rewrite Nat.mul_1_r.
    reflexivity.
  - intros a0 a1.
    rewrite visit_fib_v2_SS, IHn, fib_v1_SS.
    Search (?x + ?y = ?y + ?x).
    rewrite Nat.add_comm.
    Search (?a * (?x + ?y) = ?a*?x + ?a*?y).
    rewrite Nat.mul_add_distr_l.
    Search (?x + (?y + ?z) = (?x + ?y) + ?z).
    rewrite Nat.add_assoc.
    rewrite Nat.mul_add_distr_r.
    reflexivity.
Qed.