読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

Coqで”無限オブ無限”(証明部分)

ヒビルテで、さかいさんが興味深いCoqのコードを紹介していた。
λ. Coqで“無限オブ無限”
どうやら元ネタはここ(derive your dreams)らしい。

おもしろそうなので、さかいさんのコードを証明してみた。

証明した定理は以下。

Theorem main : forall m n:nat, m >= 1 -> n >= 1 ->
  Str_in (m,n) (iflatten ss).

但し、

ss =
 [[(1,1); (1,2); ...];
  [(2,1); (2,2); ...];
   :
   : ]

とする。


(*=====まず、ちょっと準備=====*)
Lemma p_split : forall (X Y:Set)(x1 x2:X)(y1 y2:Y),
  x1 = x2 -> y1 = y2 -> (x1, y1) = (x2, y2).
Proof.
intros X Y x1 x2 y1 y2 eqx eqy.
rewrite eqx. rewrite eqy. reflexivity.
Qed.

Definition comp (X Y Z:Set)(f:X->Y)(g:Y->Z)(x:X) := g (f x).
Implicit Arguments comp [X Y Z].

Fixpoint times (S:Set)(f:S->S) (n:nat)(x:S) : S :=
  match n with
  | O => x
  | S p => times S f p (f x)
  end.
Implicit Arguments times [S].

Lemma times_plus : forall (S:Set)(f:S->S)(i j:nat)(x:S),
  times f (i+j) x = comp (times f i) (times f j) x.
Proof.
intros S f i; induction i; intros j x.
(* sub1 *)
simpl. unfold comp. reflexivity.
(* sub2 *)
simpl. unfold comp. rewrite IHi. unfold comp. reflexivity.
Qed.

Definition f1 (X A B:Set)(f:X->A*B)(x:X) : A :=
  match f x with | (a,_) => a end.

Definition f2 (X A B:Set)(f:X->A*B)(x:X) : B :=
  match f x with | (_,b) => b end.
Implicit Arguments f1 [X A B].
Implicit Arguments f2 [X A B].

Axiom Extensionality_of_functions: forall (A B:Set) (f g:A -> B), (forall x, f(x)=g(x)) -> f=g.
(*=====準備終わり=====*)
(*=====ここからさかいさんのソースコード======*)
(* IFlatten.v *)
Section IFlatten.

Require Import List.
Require Import Streams.

(* anamorphisms (co-iteration) *)
CoFixpoint unfold (A X : Set) (phi : X -> A*X) (x : X) : Stream A := match phi x with
     | (a, x) => Cons a (unfold A X phi x)
   end.
Implicit Arguments unfold [A X].

Inductive CV (A X : Set) : Set :=
  | CVLast : X -> CV A X
  | CVCons : A * CV A X -> CV A X.
Implicit Arguments CVLast [A X].
Implicit Arguments CVCons [A X].

(* futumorphisms (cource-of-value co-iteration) *)
Definition futu (A X : Set) (phi : X -> A * CV A X) (x : X) : Stream A := let psi cv :=
         match cv with
           | CVLast x => phi x
           | CVCons p => p
         end
   in unfold psi (CVLast x) .
Implicit Arguments futu [A X].

Definition add_prefix (A : Set) (xs : list A) (X : Set) (cv : CV A X) : CV A X
:= fold_right (fun a cv => CVCons (a, cv)) cv xs.
Implicit Arguments add_prefix [A X].

Definition iflatten (A : Set) (ss : Stream (Stream A)) : Stream A := let phi x :=
          match x with
          | (ss, ls) =>
             let s := hd ss in
             let ss2 := tl ss in
             let ls2 := tl s :: List.map (fun x => tl x) ls in
               ( hd s
               , add_prefix
                 (List.map (fun x => hd x) ls)
                 (CVLast (ss2, ls2))
               )
          end
   in futu phi (ss, nil).
Implicit Arguments iflatten [A].

(*End IFlatten.*)
(*=======さかいさんのコード ここまで=========*)
(*========ここから証明===========*)

(* まずは定義 *)
(* 自然数のくみを要素に持つ無限無限リストStream (Stream M)を考える *)
Definition M := (nat * nat)%type.
CoFixpoint from (i j:nat) := Cons (i,j) (from i (1+j)).
CoFixpoint fromfrom i j := Cons (from i j) (fromfrom (1+i) j).

Fixpoint ls i j {struct i} := match i with
  | O => nil
  | S i' => from i j :: (ls i' (1+j))
  end.

Definition ss := fromfrom 1 1.
Definition CVm := CV M (Stream (Stream M) * list (Stream M)).

Definition phi' (x:Stream(Stream M) * list(Stream M)) :=
          match x with
          | (ss, ls) =>
             let s := hd ss in
             let ss2 := tl ss in
             let ls2 := tl s :: List.map (fun x => tl x) ls in
               ( hd s
               , add_prefix
                 (List.map (fun x => hd x) ls)
                 (CVLast (ss2, ls2))
               )
          end.

Definition phi (cv : CVm) := match cv with
  | CVLast (ss, ls) => phi' (ss, ls)
  | CVCons (m, cvtl) => (m, cvtl)
  end.

Definition futu_phi x := unfold phi (CVLast x).

(** 証明のために独自に定義したもうひとつのiflatten。 
 *  のちにさかいさんのiflattenと等しいことを証明する. 
 *)
Definition iflatten' (ss : Stream (Stream M)) : Stream M := futu_phi (ss, nil).
(* 定義した項目に関する簡単な補題たち *)
Lemma unfold_fromfrom : forall i j:nat,
  fromfrom i j = Cons (Cons (i,j) (from i (1+j))) (fromfrom (1+i) j).
Proof.
intros. rewrite (unfold_Stream (fromfrom i j)).
unfold fromfrom at 1.
rewrite (unfold_Stream (from i j)).
unfold from at 1. reflexivity.
Qed.

Lemma unfold_from : forall i j:nat,
  ls (1+i) j = from (1+i) j :: List.map (fun s => tl s) (ls i j).
intro i; induction i; intro j.
(* sub 1 *)simpl; reflexivity.
(* sub 2 *)simpl; simpl in IHi.
rewrite <- (IHi (S j)).
reflexivity.
Qed.

Lemma unfold_unfold : forall(X A:Set)(f:X->A*X)(x:X),
  unfold f x = Cons (f1 f x) (unfold f (f2 f x)).
intros X A f x; rewrite (unfold_Stream (unfold f x)).
unfold f1; unfold f2.
unfold unfold.
induction (f x).
fold unfold.
reflexivity.
Qed.

Lemma nth_unfold : forall (X A:Set)(f:X->A*X)(n:nat)(x:X),
  Str_nth n (unfold f x) = f1 f (times (f2 f) n x).
Proof.
intros X A f.
intro n; induction n.
intro x.
rewrite unfold_unfold.
simpl.
unfold Str_nth.
simpl.
reflexivity.
(* subgoal2 *)intro x.
unfold times.
fold times.
rewrite <- (IHn (f2 f x)).
rewrite unfold_unfold.
unfold Str_nth.
unfold Str_nth_tl at 1.
reflexivity.
Qed.
(* 独自に定義したiflatten'とさかいさんのiflattenの等価性 *)
Lemma eq_iflatten : iflatten ss = iflatten' ss.
Proof.
unfold iflatten'. unfold iflatten.
unfold futu_phi. unfold futu.
Check f_equal2.
Check unfold.
apply (f_equal2 (fun (f:CVm->M*CVm) (x:CVm) => unfold f x)).
(* sub1 *)
apply Extensionality_of_functions.
intro x. case x.
(* sub11 *)
simpl. reflexivity.
(* sub12 *)
simpl. intro p; case p. reflexivity.
(* sub2 *)
reflexivity.
Qed.
(* ここからCVやリストに関する長さを扱う *)
Require Import Arith.

Fixpoint cvlength (A X:Set)(cv:CV A X) : nat := match cv with
  | CVLast _ => O
  | CVCons (_, cvtl) => S (cvlength A X cvtl)
  end.
Implicit Arguments cvlength [A X].

Definition cv0 : CVm := CVLast (ss, nil).

(* cvの末尾を取り出す関数 *)
Fixpoint last_of (cv:CVm) : CVm := match cv with
  | CVLast xxx => CVLast xxx
  | CVCons (_, cvtl) => last_of cvtl
  end.

(* 和を計算する関数 (sumk n = 0+1+2+...+n) *)
Fixpoint sumk n:nat := match n with
  | O => O | S p => n + sumk p end.

Fixpoint cv (n:nat) := match n with
  | O => cv0
  | S p => f2 phi (cv p)
  end.

(* 以上の定義により
 * iflatten ss = phi1 (cv^n CVLast(ss,nil))
 * みたいに思うことができる *)
(* 諸性質の証明 *)
Lemma unfold_phi_cons : forall (m:M)(cv:CVm), phi (CVCons(m,cv)) = (m,cv).
Proof.
intros m cv; unfold phi; reflexivity.
Qed.

(* 高校で習った数列の足し算の公式 Σk = (1/2)n(n+1) *)
Fact fsumk : forall n:nat, 2 * sumk n = n*(1+n).
Proof.
intro n; induction n.
simpl; reflexivity.
unfold sumk; fold sumk; unfold sumk in IHn; fold sumk in IHn.
rewrite mult_plus_distr_l. rewrite IHn. ring.
Qed.

Lemma unfold_phi_last :
 forall (m:M)(s2:Stream M)(ss2:Stream(Stream M))(ls:list(Stream M)),
  phi (CVLast (Cons(Cons m s2) ss2, ls)) =
   (m, add_prefix 
         (List.map (fun s => hd s) ls)
         (CVLast(ss2, s2::List.map (fun s => tl s) ls))).
Proof.
intros m s2 ss2 ls0. unfold phi. unfold phi'. reflexivity.
Qed.

Lemma cv_times_phi2 : forall (n:nat),
  cv n = times (f2 phi) n cv0.
intro n. induction n.
simpl. reflexivity.
unfold cv; fold cv.
cut (S n = n+1).
intro eq; rewrite eq.
rewrite IHn. rewrite times_plus. unfold comp.
unfold times at 2. reflexivity.
rewrite Plus.plus_comm. simpl. reflexivity.
Qed.
Lemma len : forall (k n:nat) (cvn:CVm),
  k = cvlength (cv n) -> cvn = cv n -> cv (k+n) = last_of (cv n).
Proof.
intro k; induction k.
(* subgoal 1 *)
intros n cvn H. simpl. induction (cv n).
 (* subgoal 11 *)
simpl; reflexivity.
 (* subgoal 12 False *)
induction p. inversion H.
(* subgoal 2 *)
intros Pn cvPn. rewrite Plus.plus_Snm_nSm.
intros H1 H2. rewrite (IHk (S Pn) (cv (S Pn))).
 (* sub 21 *)
simpl. induction (cv Pn).
  (* sub 211 False *)
inversion H1.
  (* sub 212 *)
induction p. unfold f2. rewrite unfold_phi_cons.
simpl; reflexivity.
 (* sub 22 *)
simpl. induction (cv Pn).
  (* sub 221 False *)
inversion H1.
  (* sub 222 *)
induction p. unfold f2. rewrite unfold_phi_cons.
inversion H1. reflexivity.
 (* sub 23 *)
reflexivity.
Qed.

Lemma phi2_last : forall (k:nat),
  f2 phi (CVLast (fromfrom(1+k) 1, ls k 2)) =
    add_prefix (List.map (fun s => hd s) (ls k 2)) (CVLast(fromfrom (2+k) 1, ls (1+k) 2)).
intro k. rewrite unfold_fromfrom.
unfold f2.
rewrite unfold_phi_last. rewrite unfold_from.
reflexivity.
Qed.



Lemma cvlenlen : forall (x:Stream (Stream M) * list (Stream M))(l:list M),
  cvlength (add_prefix l (CVLast x)) = List.length l.
intros x list. induction list.
(* sub 1 *) simpl; reflexivity.
(* sub 2 *) simpl. rewrite IHlist; reflexivity.
Qed.

Lemma lslen : forall i j : nat, length (ls i j) = i.
intro i; induction i.
(* sub 1*) simpl; reflexivity.
(* sub 2 *) simpl. intro j. rewrite IHi.
reflexivity.
Qed.

Lemma cv_sumk_last : forall i:nat,
  cv (sumk i) = CVLast(fromfrom (1+i) 1, ls i 2).
intro i; induction i.
(* sub 1 *)
reflexivity.
(* sub 2 *)
unfold sumk; fold sumk. rewrite plus_Snm_nSm.
rewrite (len i (S (sumk i)) (cv (S (sumk i)))).
  (* sub 21 *)
unfold cv; fold cv. rewrite IHi.
rewrite (phi2_last i).
induction (List.map (fun s => hd s) (ls i 2)).
simpl; reflexivity. simpl. simpl in IHl.
rewrite IHl. reflexivity.
  (* sub 22 *)
unfold cv; fold cv. rewrite IHi.
rewrite (phi2_last i).
rewrite cvlenlen. rewrite map_length.
rewrite lslen. reflexivity.
  (* sub 23 *)
reflexivity.
Qed.


Lemma unfold_Str_nth_tl : forall (X:Set)(k:nat)(s:Stream X),
  Str_nth_tl (S k) s = tl (Str_nth_tl k s).
Proof.
intros X k s. rewrite tl_nth_tl.
rewrite (unfold_Stream s). unfold tl. unfold Str_nth_tl at 1. reflexivity.
Qed.

Lemma nth_iflatten : forall n:nat, Str_nth n (iflatten' ss) = f1 phi (cv n).
Proof.
intros n. rewrite cv_times_phi2. rewrite <- nth_unfold.
unfold iflatten. unfold futu. unfold phi. unfold cv0.
simpl.
reflexivity.
Qed.

Lemma addpref_cons : forall (l:list M)(m:M)(cv:CVm),
  add_prefix (m::l) cv = CVCons (m, (add_prefix l cv)).
Proof.
intro l. induction l; intros m mmm.
(* sub1 *) simpl. reflexivity.
(* sub2 *) simpl. reflexivity.
Qed.

Lemma addpref_nth : forall (default:M)(n:nat)(x:Stream(Stream M)*list(Stream M))
(l:list M), n < length l ->
  f1 phi (times (f2 phi) n (add_prefix l (CVLast (x)))) =
    List.nth n l default.
Proof.
intros mmm n. induction n; intros mmmm l.
(* sub1 *) case l. intro H. inversion H.
intros m tl H. unfold f1. simpl. reflexivity.
(* sub2 *)
case l. intro H. inversion H.
intros m l' H.
rewrite (addpref_cons).
cut (S n = 1 + n).
intro eq; rewrite eq.
rewrite times_plus. unfold comp. unfold times at 2.
unfold f2 at 2. rewrite unfold_phi_cons.
rewrite IHn.
simpl. reflexivity.
simpl in H.
apply lt_S_n. apply H.
simpl. reflexivity.
Qed.


Lemma nth_map_ls : forall (default:M)(k i j:nat), k < length (ls i j) ->
  nth k (List.map (fun s=>hd s) (ls i j)) default = (i-k, j+k).
Proof.
intros mmm k. induction k; intros i j.
(* sub1 *)
case i. intro H. inversion H.
intros i' H. simpl. apply p_split. reflexivity. ring.
(* sub2 *)
case i. intro H. inversion H.
simpl. intros i' H.
rewrite IHk.
apply p_split. reflexivity. ring.
apply lt_S_n. apply H.
Qed.

Lemma h2 : forall (n i j:nat)(x:Stream(Stream M)*list(Stream M)),
  n < length (ls i j) ->
  f1 phi (times (f2 phi) n (add_prefix (List.map (fun s=>hd s) (ls i j))
    (CVLast x))) = (i-n, j+n).
Proof.
intros.
rewrite (addpref_nth (0,0)). rewrite nth_map_ls. reflexivity.
apply H. rewrite map_length. apply H.
Qed.

Inductive Str_in (X:Set) : X -> Stream X -> Prop :=
inhd : forall (x:X)(tl:Stream X), Str_in X x (Cons x tl)
intl : forall (x y:X)(tl:Stream X), Str_in X x tl -> Str_in X x (Cons y tl).
Implicit Arguments Str_in [X]. Lemma Str_in_nth : forall (X:Set)(n:nat)(x:X)(s:Stream X), Str_nth n s = x -> Str_in x s. Proof. intros X n. induction n; intros x s. (* sub1 *) case s. intros hd tl. unfold Str_nth. unfold Str_nth_tl. unfold Streams.hd. intro eq; rewrite eq. apply inhd. (* sub2 *) case s. intros hd tl. unfold Str_nth. unfold Str_nth_tl. intro H. apply intl. apply IHn. rewrite <- H. simpl. reflexivity. Qed. Implicit Arguments Str_in_nth [X].
(** ここがメインの定理! **)
Theorem main : forall m n:nat, m >= 1 -> n >= 1 ->
  Str_in (m,n) (iflatten ss).
Proof.
intros m n Hm Hn.
apply (Str_in_nth (sumk (m+n-2)+(n-1)) (m,n)).
rewrite eq_iflatten.
rewrite nth_iflatten. elim Hn.
(* sub1 *)
cut (forall k:nat, sumk k + (1-1) = sumk k).
 (* sub 11 *)
intro eq; rewrite eq.
rewrite cv_sumk_last.
rewrite unfold_fromfrom. unfold f1. rewrite unfold_phi_last.
elim Hm.
  (* sub 111 *)
simpl. reflexivity.
  (* sub 112 *)
intros m' Hm' meq.
simpl.
inversion meq. rewrite H0.
cut (m' + 1 - 1 = m').
   (* sub 1121 *)
intro m'eq; rewrite m'eq; reflexivity.
   (* sub 1122 *)
case m'. simpl. reflexivity.
intro. simpl. rewrite <- minus_n_O. ring.
 (* sub 12 *)
intro k. auto with arith.
(* sub2 *)
intros n' Hn' mmm. rewrite cv_times_phi2.
rewrite times_plus. unfold comp.
rewrite <- cv_times_phi2. rewrite cv_sumk_last.
cut (S n' - 1 = S (n'-1)).
 (* sub 21 *)
intro n'eq; rewrite n'eq.
unfold times. fold times.
unfold f2 at 2.
rewrite unfold_fromfrom. rewrite unfold_phi_last.
Check h2.
rewrite h2.
  (* sub 211 *)
Require Import Omega.
apply p_split; omega.
  (* sub 212 *)
rewrite lslen.
omega.
 (* sub 22 *)
omega.
Qed.
(*##############メインの定理証明終わり########################*)

End IFlatten.