Skip to content

Instantly share code, notes, and snippets.

@anton-trunov
Created November 15, 2016 15:00
Show Gist options
  • Save anton-trunov/84b63d4ca28c2698ed87b5c680974506 to your computer and use it in GitHub Desktop.
Save anton-trunov/84b63d4ca28c2698ed87b5c680974506 to your computer and use it in GitHub Desktop.
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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment