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.