mzp/vvakame.md

## vvakame.md

      
    Raw
  

              vvakame.md
            
          
    わかめモナ化: Maybeモナドの証明 + Coq入門

証明の重要性


うかつにモナドと言うと刺される

例: jQueryはモナドだ - id:anatooのブログ

「jQueryはモナドである」と主張したけど、証明はなかったのですぐに刺された。
JQueryがモナドかどうかとか - たけをの日記＠天竺から帰ってきたよ

うーん… これ、いわゆる3つのモナド則じゃないよね。ココに書かれてるのはモナドの構造のこと、それもHaskellに特化したもので、圏論的な構造じゃない。抽象的に書けば、モナドは関手に2つの変換 unit と join が付随したもの（Haskell の bind はこれらから導出できる）だし、更に 左単位則、右単位則、結合則の3つの法則を満たすたものでなければならない。
この記事で何をやりたかったかはわかるんだけど、でもうまく行ってないね。もし何かをモナドと呼ぶときはもっと厳密かつ正確に話を進める必要があるし、そうでなければ、ただ大雑把な比較をしてみたってだけにしかならないよ。

jQueryは本当にモナドだった - 北海道苫小牧市出身のPGが書くブログ

さて、元ネタはこちらなのですが、独自のモナド節を唱えていて非常に怪しい。と言うことで、怪しくならないように真面目に解説してみます。

Coqとは

Coqは定理証明器とよばれるジャンルのソフトウェア。 以下のことができる。

OCamlっぽいシンタックスで型や関数の定義ができる。 (=プログラムが書ける)
定義した型や関数に関する性質を証明できる
定義した型や関数をOCaml/Haskell/Schemeに変換できる。 Scalaに変換するパッチも存在している。

Coqのインストール

http://coq.inria.fr/ からCoqをインストールしましょう。インストール方法は、Coq を始めようを参照。
トートロジーの証明

CoqIDEに以下を入力し、評価する。
Theorem my_first_theorem: forall A, 
  A -> A.
Proof.
  intros.
  tauto.
Qed.

証明モードとタクティクス

定理の定義は以下の構文で始める。
Theorem <定理名>: <定理の中身>.

定理を定義すると証明モードに切り替わる。 証明が終わるまで、定理の定義は完了しない。
証明モードでは右下に以下のような証明木が表示される。 線の上が証明の前提、下が証明すべき論理式(結論)になっている。
A : Type
X : A
============================
A

証明を進めるには、上下どちらかの論理式を変形するか、上から下が導けることを示さないといけない。Coqではどちらもタクティクスと呼ばれるコマンドを用いて行なう。
今回利用したタクティクスは以下の2つ。

intros: 結論が"A->B->…->C"という形をしているとき、A,B,…を前提に移動させる。
tauto: 前提に結論と同じ論理式が含まれる場合に、証明を完了させる。

よく使うタクティクスは使えるタクティク集にまとまっている。
my_not関数の定義

もうちょっとだけプログラムっぽい関数を定義してみる。
(* boolを反転する関数 *)
Definition my_not b := 
  match b with
    true => false 
  | false => true 
  end.

思ったとおりに動くか試してみる。
Eval compute in my_not true.

my_not関数の性質の証明

(* 2回反転させると元にもどることを証明する *)
Theorem not_invert_boolean: forall (b:bool), 
  my_not (my_not b) = b.
Proof.
  (* .. -> ..の左を結論から前提に移動させる *)
  intros.
  
  (* b = trueの場合と、b = falseの場合で場合分けをする *)
  destruct b.
    (* Case 1: b = trueの場合 *)
    simpl.  
    reflexivity.

    (* Case 2: b = falseの場合 *)
    (* 簡約する *)
    simpl.
    reflexivity.
Qed.

今回使ったタクティクス


destruct X: Xについて場合分けを行なう。
simpl: 結論を簡約(評価)する。
reflexivity: 結論がA=Aのとき、証明を完了させる。

(復習)モナドとは

Haskell風モナドの定義。 ただし return はCoqでは予約語なので、 ret に変更してある。
(ret x) >>= f = f x
m >>= ret = m
(m >>= f) >>= g = m >>= (fun x => f x >>= g)

bindとreturnの定義

Maybeモナドのbindとreturnを定義する。optionについてはCoq標準のものを流用する。
Definition bind {A B : Type} (m : option A) (f : A -> option B) : option B :=
    match m with
      None => None
    | Some v => f v
    end.
    
(* 中置演算子を割り当てる *)
Infix ">>=" := bind (at level 50).

Definition ret {A : Type} (v : A) : option A :=
  Some v.

Evalしてみる

ちょっと試してみましょう。
Eval compute in ret 1.
Eval compute in (Some 1) >>= (fun x => ret (1+x)).

モナド則 その1

さあ証明してみましょう。
Theorem monad_1: forall A B (f : A -> option B) x,
  (ret x) >>= f = f x.
Proof.
(* FILL IN HERE *)
Qed.

モナド則 その2

さあ証明してみましょう。
Theorem monad_2: forall A (m : option A),
  m >>= ret = m.
Proof.
(* FILL IN HERE *)
Qed.

モナド則 その3

さあ証明してみましょう。
Theorem monad_3: forall A B C (f : A -> option B) (g : B -> option C) m,
  (m >>= f) >>= g = m >>= (fun x => f x >>= g).
Proof.
(* FILL IN HERE *)
Qed.

Extractしよう

OCamlに変換しましょう。
Require Import ExtrOcamlBasic.
Extraction "maybeMonad.ml" bind ret.

参考文献


Maybe monad is monad — Gist
Coq
プログラミング Coq
ソフトウェアの基礎