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