[Coq][PFDS] How to use Module in Coq

今日のFormal Methods Forumでは、CoqでPFDS(Purely Functional Data Structure)を、というのをみんなで実施しました。参加者の誰もがMLのmodule systemになれておらず色々苦労しましたが、とりあえずこんな感じのコードになりました。 まず Exercise 2.1 の suffixes ですが、これは簡単。

Fixpoint suffixes{A:Set}(xs:list A):list (list A) :=
match xs with
| nil => nil
| _::xs' => xs :: (suffixes xs')
end.

Eval compute in (suffixes (1::2::3::4::nil)).
(* = (1 :: 2 :: 3 :: 4 :: nil)
       :: (2 :: 3 :: 4 :: nil) :: (3 :: 4 :: nil) :: (4 :: nil) :: nil
     : list (list nat) *)

consする回数を数えるヴァージョンと、回数がO(n) (というかn) である証明。

Fixpoint suffixes' {A:Set}(xs:list A)(c:nat):
  (nat * (list (list A)))%type :=
match xs with
| nil => (0,nil)
| _::xs' =>
  let (c',ys) := (suffixes' xs' c)
  in (c'+1, xs::ys)
end.
Eval compute in (suffixes' (1::2::3::4::nil) 0).

Theorem suffixes'_length : forall (A:Set)(xs:list A),
  fst (suffixes' xs 0) = length xs.
Proof.
  intros A xs.
  induction xs.
    simpl. trivial.
    simpl. destruct (suffixes' xs 0). simpl.
    simpl in IHxs. rewrite <- IHxs.  omega.
Qed. 

Coq の module の使い方はこんな感じ。 まず SET signature のモジュールを定義します。予約語回避のためあちこちに _ を追加します。

Module Type SET.
  Parameter Elem : Set.
  Parameter Set_ : Set.
  Parameter empty : Set_.
  Parameter insert : Elem -> Set_ -> Set_.
  Parameter member : Elem -> Set_ -> bool.
End SET.

次いで、ORDERED signature を定義します。

Module Type ORDERED.
  Parameter T : Set.
  Parameter eq_ : T -> T -> bool.
  Parameter lt_ : T -> T -> bool.
  Parameter gt_ : T -> T -> bool.
End ORDERED.

次が、ORDERED な型のUnbalancedSet を定義します。ElementはORDERED signatureを満たすものです。SETのsignatureを持つので<:を使って定義します。

Module Type UnbalancedSet (Element:ORDERED) <: SET.
  Definition Elem := Element.T.
  Inductive Tree :=
  | E : Tree
  | T : Tree -> Elem -> Tree -> Tree.
  Definition Set_ := Tree.
  Definition empty := E.
  Fixpoint member (x:Elem)(tr:Tree) :=
  match tr with
  | E => false
  | T a y b => 
    if (Element.lt_ x y) then (member x a)
    else (if (Element.lt_ y x) then (member x b)
          else true )
  end.
  Fixpoint insert (x:Elem)(tr:Tree) :=
  match tr with
  | E => T E x E
  | T a y b =>
    if (Element.lt_ x y) then (T (insert x a) y b)
    else (if (Element.lt_ y x) then (T a y (insert x b))
          else tr)
  end.
End UnbalancedSet.

と定義します。 ORDERED の具体例として NAT を作ります。

Fixpoint blt_nat (x y:nat):bool :=
match x,y with
| O,O => false
| O,_ => true
| _,O => false
| S x',S y' => blt_nat x' y'
end.
Eval compute in (blt_nat 2 2). (* false *)
Eval compute in (blt_nat 2 3). (* true *)
Eval compute in (blt_nat 3 2). (* false *)
Definition bgt_nat (x y:nat):bool := blt_nat y x.

Module NAT <: ORDERED.
  Definition T := nat.
  Definition eq_ := beq_nat.
  Definition lt_ := blt_nat.
  Definition gt_ := bgt_nat.
End NAT.

そして、Element:ORDERED として NAT<:ORDERED を取る UNSet を定義します。Include を使うのが大事なポイントです。

(* Unbalanced Nat Set *)
Module UNSet <: (UnbalancedSet NAT).
Include (UnbalancedSet NAT).
End UNSet.

最後にそれを使ってみます。

Definition E := UNSet.E.
Print E.
Definition T := UNSet.T.
Print T.
Print UNSet.Elem.
Print NAT.T.
Eval compute in (T E 1 E).
Eval compute in (UNSet.member 1 (T E 1 E)).
Eval compute in (UNSet.insert 2 (T E 1 E)).