ひろしま学生IT勉強会で発表した資料です

Fib.v

(* 普通の再帰で書いた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.