ズッキーニのプログラミング実験場

プログラミング + アカデミック + 何か面白いこと。 記載されているものは基本的に私が所属する団体とは関係がありません。

   Jun 21

[Coq]リストのモナドを定義してみる

by zuqqhi2 at 2013年6月21日
Pocket

Coq リスト モナド

リストモナドの定義

Haskellのモナドを定義してみることを考える。
まず、モナドに必要なのは以下の三つの性質である。

  • f(return(A),g) = g(A)
  • f(A,return) = A
  • f(f(A, g),h) = f(A, (x -> f(g(B), h)))

また、以下の2つの関数も必要となる。

  • return
  • f(a,b) = b(a)

以上に沿うように書いてみたモナドのクラスは以下のようになった。

Class MyMonad (M: Type -> Type) := {
    myreturn : forall {A}, A -> M A
  ; mybind : forall {A B}, M A -> (A -> M B) -> M B
  ; myleft_identify : forall A B (a: A) (f: A -> M B), mybind (myreturn a) f = f a
  ; myright_identify : forall A (m: M A), mybind m myreturn = m
  ; myassociativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C), mybind (mybind m f) g = mybind m (fun x => mybind(f x) g)
}.

次にリストのモナドインスタンスを定義してみる。

Instance MList: MyMonad list := {
   myreturn A x := x :: nil
 ; mybind A B m f := mymap A B f m
}.

さて、ここまでは通ったけど、証明ができないな。。。
mybindのところにhaskellのconcat関数見たいのがあれば行けそうだ!

証明

モナド則とリストモナドを定義したが、証明がうまくいかなかった。。。

そこで良い方法がないかと検索していたらflat_mapなる関数を見つけた。
これを使ってリストモナドの定義と証明をしてみる。

まずはモナドの定義の再掲とリストモナドの再定義。

Class MyMonad (M: Type -> Type) := {
    myreturn : forall {A}, A -> M A
  ; mybind : forall {A B}, M A -> (A -> M B) -> M B
  ; myleft_identify : forall A B (a: A) (f: A -> M B), mybind (myreturn a) f = f a
  ; myright_identify : forall A (m: M A), mybind m myreturn = m
  ; myassociativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C), mybind (mybind m f) g = mybind m (fun x => mybind(f x) g)
}.

Instance MList: MyMonad list := {
   myreturn A x := x :: nil
 ; mybind A B m f := flat_map f m
}.

早速証明開始。

Proof.
  intros A B a f.
  simpl.

------------------------------------
3 subgoal
A : Type
B : Type
a : A
f : A -> list B
______________________________________(1/3)
f a ++ nil = f a
______________________________________(2/3)
forall (A : Type) (m : list A), flat_map (fun x : A => x :: nil) m = m
______________________________________(3/3)
forall (A B C : Type) (m : list A) (f : A -> list B) (g : B -> list C),
flat_map g (flat_map f m) = flat_map (fun x : A => flat_map g (f x)) m

ん?simpl.しても変わらない。
まだ証明されていないのか?
とりあえず、 リストモナドの前に証明しよう!

Lemma nil_app : forall (A : Type)(a : list A),
  a ++ nil = a.
Proof.
  intros.
  induction a.
  simpl.
  reflexivity.
  simpl.
  rewrite IHa.
  reflexivity.
Qed.

帰納法でさくっと証明完了。

さて、戻ってリストモナドの証明の続きをしよう。

  rewrite nil_app.
  reflexivity.
  
  intros.
  induction m.
  simpl.
  reflexivity.
  simpl.
  rewrite IHm.
  reflexivity.

  intros.
  induction m.
    simpl.
    reflexivity.
    simpl.
    rewrite <- IHm.

---------------------------------

1 subgoals
A : Type
B : Type
C : Type
a : A
m : list A
f : A -> list B
g : B -> list C
IHm : flat_map g (flat_map f m) = flat_map (fun x : A => flat_map g (f x)) m
______________________________________(1/1)
flat_map g (f a ++ flat_map f m) =
flat_map g (f a) ++ flat_map g (flat_map f m)

んー。
良い感じで進んでたけど、また詰まったな。
リストモナドの前に戻って、flat_map f (a ++ b) = flat_map f(a) ++ flat_map f (b)の
証明をしよう!

Lemma flat_map_app : forall (A B : Type)(l l' : list A)(f : A -> list B),
  flat_map f (l++l') = flat_map f l ++ flat_map f l'.
Proof.
  induction l.
    simpl.
    intros.
    reflexivity.

    intros.
    simpl.
    rewrite IHl.
    rewrite app_ass.
    reflexivity.
Qed.

これも帰納法でさくっとできた。

よし!後は最後の大詰めだ!

    rewrite flat_map_app.
    reflexivity.
Qed.

やった!
できた!

Related Posts

  • 2013年7月13日 [Coq]証明駆動開発で2値化 part1 やりたいこと 証明駆動開発で画像の2値化(白か黒の2種類の値のみにする)をする関数を作成してみる。 Coq とりあえず2値化関数をCoqで定義する。 […]
  • 2015年3月25日 Coqによる 証明駆動開発 超入門 証明駆動開発 とは 証明駆動開発 とは証明によってプログラムが期待通りの性質を有しているかを確かめながら開発する手法のこと。 ユニットテストの一部で使用可能な方法。 証明駆動開発 […]
  • 2012年10月8日 WordPressでテーマに合うようにプロフィール表示してみる せっかくだから自己紹介の部分をWordPress上に書きたいなと 思って検索したらいいサイト見つけた! WordPress上にプロフィールを表示してみよう これを見ながら自分が使っているテーマに合うように sidebar.phpに次のコードをサイドバーの […]
  • 2013年7月14日 [Ruby][Rspec]ファイル出力のテスト やりたいこと Rspecでファイル出力するバッチのテストを書きたい。 プログラム バッチ mongoDBからデータをcsvファイルに出力する。 Rspec Target I want to write test code for […]
  • 2014年11月16日 [Node.js][Meetup]東京Node学園祭2014でLTしてきた 東京Node学園際2014でLTしてきた。 以下そのスライド。 20141115_node_school_festival_lt from Hidetomo Suzuki もっと使いこなせるようになりたい。。。 I gave a LT of […]
  • jenkins nginx2014年4月2日 [Jenkins]Coffee Script Coverage Karmaでカバレッジを測る Coffee Script Coverage 計測をする流れは以下。 Karmaセッティング 必要なライブラリ Cakefileのセッティング coffee […]
Pocket

You can follow any responses to this entry through the RSS 2.0 feed. Both comments and pings are currently closed.