Skip to content

Instantly share code, notes, and snippets.

@takoeight0821 takoeight0821/Fib.v
Last active Jun 13, 2018

Embed
What would you like to do?
ひろしま学生IT勉強会で発表した資料です
(* 普通の再帰で書いたfibと、末尾再帰のfibが等しいことをCoqで証明
http://www.madsbuch.com/blog/100-days-of-fibonacci-day-7-coq/
を参考にした。
*)
From mathcomp Require Import ssreflect.all_ssreflect.
Fixpoint fib1 (n : nat) : nat :=
match n with
| 0 => 0
| 1 => 1
| S n' => fib1 n' + fib1 (n' - 1)
end.
Eval simpl in fib1 7.
Fixpoint fib2 (a b n : nat) : nat :=
match n with
| 0 => a
| S n => fib2 b (a + b) n
end.
Eval simpl in fib2 0 1 7.
Definition spec_of_fib (f : nat -> nat) :=
f 0 = 0 /\ f 1 = 1 /\
forall n : nat,
f (S (S n)) = f (S n) + f n.
Lemma fib1_is_fib : spec_of_fib fib1.
Proof.
rewrite /spec_of_fib.
split; try by rewrite /=.
split; try by rewrite /=.
move=> n.
rewrite /=.
have: n.+1 - 1 = n.
rewrite -minusE /=.
by rewrite minusE subn0.
move => subn_Sn1.
by rewrite subn_Sn1.
Qed.
Lemma fib2_shift : forall f : nat -> nat,
spec_of_fib f ->
forall k i : nat,
fib2 (f i) (f (S i)) k = f (k + i).
Proof.
move=> f.
rewrite /spec_of_fib.
case=> f0.
case=> f1.
move=> rec.
elim.
- by [].
- move=> n IHk i.
by rewrite addSnnS -(IHk (i.+1)) (rec i) /= addnC.
Qed.
Lemma fib2_is_fib : spec_of_fib (fib2 0 1).
Proof.
rewrite /spec_of_fib.
split.
by [].
split.
by [].
elim.
- by rewrite /=.
- move=> n.
rewrite (fib2_shift fib1 fib1_is_fib n.+2 0)
(fib2_shift fib1 fib1_is_fib n.+1 0)
(fib2_shift fib1 fib1_is_fib n.+3 0).
by rewrite /=.
Qed.
Lemma fib_eq : forall (f1 f2 : nat -> nat),
spec_of_fib f1 -> spec_of_fib f2 ->
forall (n : nat), f1 n = f2 n.
Proof.
rewrite /spec_of_fib.
move=> f1 f2 [eq0f1 [eq1f1 specf1]] [eq0f2 [eq1f2 specf2]].
have: forall m : nat, f1 m = f2 m /\ f1 m.+1 = f2 m.+1.
elim.
- by rewrite eq0f1 eq0f2 eq1f1 eq1f2.
- move=> m [IHm0 IHm1].
by rewrite (specf1 m) (specf2 m) IHm0 IHm1.
move=> H n.
destruct (H n).
by rewrite H0.
Qed.
Theorem fib1_eq_fib2 : forall (n : nat),
fib1 n = fib2 0 1 n.
Proof.
move=> n.
by rewrite (fib_eq fib1 (fib2 0 1) fib1_is_fib fib2_is_fib).
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.