[Coq] Monads in Coq

社内勉強会でMonad入門の話をして、その時にCoqを用いて説明しました。
あまりHaskellに慣れてないのでCoq使ったんですが、CoqではMonad則を証明する必要があるので、実は寧ろ説明に適していました。
HaskellだとMonad則がなぜ必要なのか示すのが面倒そう（任意の関数、なんてのはQuickCheckでも作れ無さそうな気がする）ですが、CoqではそもそもMonad則を満たすことを示さないと、Monadを使えません。
サンプルコードでは、

• Maybeモナド、Listモナドについて示してあります。
• サザエさんの家族構成を用いて、MaybeやListのサンプルコードを書いています。

Class Monad (M:Type -> Type):Type := {
  return' : forall {A}, A -> M A;
  bind : forall {A B}, M A -> (A -> M B) -> M B;
  left_unit : forall A B (a:A)(f:A -> M B),
    bind (return' a) f = f a;
  right_unit : forall A (ma:M A),
    bind ma return' = ma;
  assoc : forall A B C (ma:M A)(f:A -> M B)
    (g:B -> M C), bind (bind ma f ) g =
    bind ma (fun a => bind (f a) g)
}.
Notation "m >>= f" := 
  (bind m f) (left associativity, at level 49).

Notation "'do' a <- e ; c" := 
  (e >>= (fun a => c)) 
  (at level 59, right associativity).

Instance Maybe : Monad option := {
  return' A a := Some a;
  bind A B ma f :=
    match ma with
    | None => None
    | Some a => f a
    end
}.
Proof.
  intros; auto.
  intros; destruct ma; auto.
  intros; destruct ma; [destruct (f a)|]; auto.
Defined.

Eval compute in (Some 1 >>= (fun x => return' (x + 1))).
Eval compute in (None >>= (fun x => return' (x + 1))).

Inductive Isono:Set :=
  Namihei | Fune | Masuo | Sazae | Katsuo | Wakame | Tara.

Definition father(x:Isono):option Isono :=
match x with
| Tara => Some Masuo
| Sazae | Katsuo | Wakame => Some Namihei
| _ => None
end.

Definition mother(x:Isono):option Isono :=
match x with
| Tara => Some Sazae
| Sazae | Katsuo | Wakame => Some Fune
| _ => None
end.

Definition f_of_m(s:Isono):option Isono :=
match (mother s) with
| None => None
| Some x => father x
end.

Definition f_of_m'(s:Isono):option Isono :=
  do x <- mother s;
  father x.

Eval compute in (f_of_m' Tara).
Eval compute in (f_of_m' Katsuo).

Require Import List.
Lemma flat_map_app : forall (A B:Type)(xs ys:list A)(f:A -> list B),
 flat_map f (xs++ys) = flat_map f xs ++ flat_map f ys.
Proof.
 induction xs.
   simpl. auto.
   simpl. intros. erewrite IHxs. erewrite app_ass. auto.
Qed.

Instance List : Monad list := {
  return' A x := x :: nil;
  bind A B m f := flat_map f m
}.
Proof.
(* left_unit *)
intros A B a f. simpl. erewrite <- app_nil_end. auto.
(* right_unit *)
intros A m. induction m.
 simpl. auto.
 simpl. rewrite IHm. auto.
(* assoc *)
intros A B C m f g. induction m.
 simpl. auto.
 simpl. rewrite <- IHm.
 erewrite flat_map_app. auto.
Defined.

Definition children(x:Isono):list Isono :=
match x with
| Namihei | Fune => Sazae::Katsuo::Wakame::nil
| Sazae | Masuo => Tara::nil
| _ => nil
end.

Eval compute in (children Fune).
Eval compute in (children Katsuo).

Definition grandchildren(x:Isono):list Isono :=
  do y <- children x;
     children y. 

Eval compute in (grandchildren Fune).
Eval compute in (grandchildren Katsuo).

[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)).