自然数(エンコーディングは問わず)の加算の可換法則、結合法則、分配法則を証明。

自然数の様々な性質は既にCoqの標準ライブラリに豊富に揃っているが、これらの性質は非常にベーシックなので、一から定義して証明してみた。以下はCoqのArithライブラリも特別なタクティックも使わずに実装した。

まず、自然数全体の型 nat を定義する。

Inductive nat : Set :=
| O : nat
| S : nat -> nat.

次にこの自然数上での足し算を計算する plus 関数を定義する。

Fixpoint plus x y :=
  match x with
  | O => y
  | S x => S (plus x y)
  end
where "x + y" := (plus x y).

まず一番簡単な足し算の結合則を証明する。

Proposition p01_plus_assoc :
  forall x y z, x + (y + z) = (x + y) + z.
Proof.
intros x y z; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

次に足し算の可換性を証明しようと思うが、そのために次の2つの補題を証明しておく。
ちなみに O+x = x と S x + y = S (x + y) は定義より明らかに成り立つことなので、あえて補題を用意することはしない。

Lemma plus_O : forall x, x + O = x.
Proof.
intro x; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

Lemma plus_Sy : forall x y, x + S y = S (x + y).
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 rewrite IHx in |- *; reflexivity.
Qed.

そして、足し算の可換性。

Proposition p01_plus_comm :
  forall x y, x + y = y + x.
Proof.
intros x y; induction x; simpl.
 rewrite plus_O in |- *; reflexivity.
 rewrite IHx in |- *; rewrite plus_Sy in |- *.
 reflexivity.
Qed.

あとは分配法則だが、これには掛け算が必要なので掛け算を定義する。

Fixpoint mult x y :=
  match x with
  | O => O
  | S x => y + mult x y
  end
where "x * y" := (mult x y).

左からの分配法則は簡単である。上で証明した足し算の結合則や可換性をバリバリ使っているのがわかるだろう。

Proposition p01_distr_l :
  forall x y k, k * (x + y) = k * x + k * y.
Proof.
intros x y k; induction k; simpl in |- *.
 reflexivity.
 
 rewrite IHk in |- *.
 rewrite <- (p01_plus_assoc x y _) in |- *.
 rewrite (p01_plus_assoc y (k * x) (k * y)) in |- *.
 rewrite (p01_plus_comm y (k * x)) in |- *.
 rewrite <- (p01_plus_assoc (k * x) y (k * y)) in |- *.
 rewrite (p01_plus_assoc x (k * x) _) in |- *.
 reflexivity.
Qed.

掛け算の可換性があれば右からの分配法則も示せるので、掛け算の可換性を証明。足し算の可換性と同様にいくつかの補題を証明して使った。

Lemma mult_O :
  forall x, x * O = O.
Proof.
intros x; induction x; simpl in |- *.
 reflexivity.
 apply IHx.
Qed.

Lemma mult_Sy :
  forall x y, x * S y = x + x * y.
Proof.
intros x y; induction x; simpl in |- *.
 reflexivity.
 
 rewrite IHx in |- *.
 rewrite (p01_plus_assoc y x (x * y)) in |- *.
 rewrite (p01_plus_comm y x) in |- *.
 rewrite <- (p01_plus_assoc x y (x * y)) in |- *.
 reflexivity.
Qed.

Lemma mult_comm :
  forall x y, x * y = y * x.
Proof.
intros x y; induction x; simpl in |- *.
 rewrite mult_O in |- *; reflexivity.
 
 rewrite mult_Sy in |- *.
 rewrite IHx in |- *.
 reflexivity.
Qed.

右からの分配法則。

Proposition p01_distr_r :
  forall x y k, (x + y) * k = x * k + y * k.
Proof.
intros x y k.
rewrite (mult_comm (x + y) k) in |- *.
rewrite (mult_comm x k) in |- *.
rewrite (mult_comm y k) in |- *.
apply p01_distr_l.
Qed.

Proof Party の問題をCoqで挑戦してみた。

Coq Proof Party

Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。

東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん

Coqでハノイの塔に関する証明

Coq ハノイ Tower of Hanoi

Coqが今流行っているらしい。

twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。
なんか巷でCoqがはやっているようなので - 菊やんの雑記帳

なんかおもしろそうなので一つ簡単な命題を証明してみた。

証明したこと

Lemma answer_length : forall n from to rest,
   length (answer n from to rest) = pow 2 n - 1.

Coqのnat型は引き算がとっても難しいので, この手の証明はまず以下の補助的なLemmaを先に証明するのが吉だ。

Lemma answer_length_aux : forall n from to rest,
   length (answer n from to rest) + 1 = pow 2 n.

ただ、これはanswerの手数が2^n-1であることを示しただけで、それが最短手数である証明にはなっていないことに注意しよう。

証明の全体は以下のとおり。

(* 
http://github.com/kik/sandbox/blob/c1b16b684feb7482f0582480a43b2db4a9be3ce0/coq/Hanoi.v のコードと一緒に使ってね。
 *)

Fixpoint pow x n :=
  match n with
  | O => 1
  | S p => x * pow x p
  end.

Lemma answer_length_aux : forall n from to rest,
   length (answer n from to rest) + 1 = pow 2 n.
Proof.
induction n.
 reflexivity.
 
 unfold answer in |- *; fold answer in |- *.
 intros.
 rewrite app_length in |- *; rewrite app_length in |- *.
 rewrite <- plus_assoc in |- *.
 rewrite <- plus_assoc in |- *.
 rewrite IHn in |- *.
 rewrite plus_assoc in |- *.
 rewrite IHn in |- *.
 simpl in |- *.
 rewrite plus_0_r in |- *.
 reflexivity.
Qed.


Lemma answer_length : forall n from to rest, length (answer n from to rest) = pow 2 n - 1.
Proof.
intros.
rewrite <- (answer_length_aux n from to rest) in |- *.
rewrite plus_comm in |- *.
rewrite <- pred_of_minus in |- *.
simpl; reflexivity.
Qed.

Coqによる証明駆動開発で Merge Sort プログラムをつくってみた

Coq Merge Sort Proof Driven Development 証明駆動開発 マージソート Function Functional Scheme

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。

プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket。

思ったより簡単ではなく、いろいろなテクニックが必要で非常に勉強になった。Coq初心者の人はMergeSortの問題をとりあえずの目標にして証明を頑張ると非常に効率がいいのではないかと思う。

私は、だいたい以下の流れでプログラムした。

  • Sortedという命題を作り、リストがソート済みであるという状態を定義する
  • mergesort関数があるとして、満たすべき性質(i)を定理として記述する
  • mergesort関数を定義する
    • mergesort関数に必要な補助関数 merge関数を定義して諸性質を証明する
    • mergesort関数に必要な補助関数 split関数を定義して諸性質を証明する
    • mergeとsplitを使ってmergesort関数を定義する
  • (i)を証明する


プログラムを作ろうと思ったら、実装する前にそのプログラムがどういう性質があればよいかを記述しよう。これができれば、あとはコンパイラが通るまで頑張るだけだ。コンパイラが通れば完了で、テストは必要ない。

この考えかたは証明駆動開発(Proof Driven Development)と呼ばれるらしい。

参考: d.y.d. 16:40 08/05/15 Proof Driven Development

以下、開発した手順にそって詳細を説明する。

準備

まず準備として対象とするリストの要素の型を A として、その要素上で大小比較ができることを仮定する。

型 A と A 上の大小比較演算子を\le{~}^{\prime}(小なりイコールダッシュ)とかの記号で表す。

Sortedという命題を作り、リストがソート済みであるという状態を定義する

Sortedという命題(Proposition)を次の様に定義する。

Definition Sorted (xs: list A) : Prop :=
  forall x y i j,
  i < j ->
  Some x = nth_error xs i ->
  Some y = nth_error xs j ->
    x <=' y.

nth_error関数はListモジュールにあるlistのn番目を取ってきて、オプション型で値を返す関数だ。これはだいたいi\lt jならばxs[i]\le{~}^{\prime}xs[j]であることを表現している。

Inductiveな定義で再帰的に定義する方法もあるが、今回はより一般的なかたちで定義した。ただ、それだと証明するときにちょっと大変になるのでその差を無くすために次の補題を証明しておく。

Lemma sorted_ind : forall x xs,
  Sorted xs -> (forall y, In y xs -> x <=' y) -> Sorted (x :: xs).

Lemma sorted_ind_inv : forall x xs,
  Sorted (x :: xs) -> Sorted xs /\ (forall y, In y xs -> x <=' y).

mergesort関数があるとして、満たすべき性質(i)を定理として記述する

今回の開発の目標として満たすべき性質を「任意のリストに対して、mergesortの結果が必ずsortされている」とする。それはCoqでは以下の様に記述できる。

Theorem mergesort_sorted : forall xs, Sorted (mergesort xs).

この定理を書いてコンパイルが通れば完成である。以下ではmergesortの実装と、この定理の証明を記述してコンパイルが通るようにすればいいだけだ。証明駆動開発バンザイ！

mergesort関数を定義する

mergesort関数は補助関数mergeとsplitを使って次の様に定義がしたい。

定義 merge (xs ys : list A) :=
  match (xs, ys) with
  | (nil, ys) => ys
  | (xs, nil) => xs
  | (x::xs, y::ys) =>
     if x <=?' y then
       x :: merge xs (y::ys)
     else
       y :: merge (x::xs) ys
  end.

定義 split (xs : list A) :=
  match xs with
  | nil => (nil, nil)
  | x::nil => (x::nil, nil)
  | x::y::zs =>
     match split zs with
     | (xs, ys) => (x::xs, y::ys)
     end
  end.

定義 mergesort (xs : list A) :=
  match xs with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs =>
     match split (x::y::zs) with
     | (xs, ys) => merge (mergesort xs, mergesort ys)
     end
  end.

mergeもsplitもmergesortもすべて再帰的な関数である。Coqでは停止性が保証される関数しか定義することができないので、再帰的な関数はちょっとした工夫が必要だ。それぞれの関数を順番に定義していこう。

mergesort関数に必要な補助関数 merge関数を定義して諸性質を証明する

じゃあ、merge関数を定義しよう。今回この関数が一番難しかった。でもmerge関数に関する部分が本質的にかなり重要な部分なのでmergeができたら、あとはほとんどオマケと思っていいだろう。

merge関数は引数が複数有り、停止することが構造的に明らかではない。停止性が明らかでないような再帰関数の定義はFunctionというキーワードを使って定義する。Functionキーワードでmeasure指定をして定義すると、引数が何らかの意味で減少していることを後から証明すればちゃんと定義できる。ただ、減少する引数は一つである必要があるのでリストのペアを引数に取るようにした。

Functionによる関数定義でmeasure指定をした時のの構文は以下のような感じ。

"Function" <関数名> "(" (<引数名>":"<型>) ","... ")"
  "{" "measure" <メジャー関数> <減少する引数名> "}" ":" <型> ":="
  <関数の内容> "."

メジャー関数のところはだいたい大きさをはかる関数を書けば大丈夫。リストだったらlength関数、リストのペアならその合計を返す関数を書こう。

Definition pair_length (xsys: list A * list A) :=
  length (fst xsys) + length (snd xsys).

Function merge (xsys: list A * list A) {measure pair_length xsys} : list A :=
  match xsys with
  | (nil, ys) => ys
  | (xs, nil) => xs
  | (x::xs, y::ys) =>
     if x <=?' y then
       x :: merge (xs, y::ys)
     else
       y :: merge (x::xs, ys)
  end.

こう定義した時点でコンパイルすると「Error: There are pending proofs」と言われるので対話的に証明ができるチャンスだ！ coqtopでこのファイルを読み込んで対話的証明をしよう。証明する内容は「この関数の各再帰呼び出しで指定した引数のサイズが減っているということ」だ。

  $ coqtop -l MergeSort.v
Welcome to Coq 8.2pl1 (September 2009)

merge_tcc <

ここでShow.と打つと現在の示すべきことが表示される。二回の再帰呼び出しのそれぞれでリストのペアの長さの合計が減っていることを示せればOKだ。これは非常に簡単だ。

証明が完了するとめでたくmerge関数が定義できる。Functionで定義した場合はそれだけでなく、この関数の再帰呼び出しに関する帰納法ができるmerge_indも定義されるので、mergeに関する証明にガンガン使っていこう。

ただ、このmerge_indは引数がリストのペアにして定義したためちょっと使いにくい。使いやすくするために引数を複数引数にカリー化した merge_ind_curry を補助的に作ったので、以降ではこっちを使うことにする。

ここでは以下の性質を証明した。

  • mergeされたリストに含まれている要素は、もとの引数のリストのどちらかに含まれている。
Lemma merge_incl: forall xs ys x,
  In x (merge (xs,ys)) -> In x xs \/ In x ys.
  • 整列したリスト同士をmergeすると結果も整列する。
Lemma merge_ok : forall xs ys,
  Sorted xs -> Sorted ys -> Sorted (merge (xs, ys)).
mergesort関数に必要な補助関数 split関数を定義して諸性質を証明する

split関数は再起するが、停止することが構造的に明らか(再帰呼び出しがsubtermに適用される)なのでFixpointで定義できる。

Fixpoint split (xs: list A) :=
  match xs with
  | nil => (nil, nil)
  | x::nil => (x::nil, nil)
  | x::y::zs =>
     match split zs with
     | (xs, ys) => (x::xs, y::ys)
     end
  end.

ただ、Functionで定義したときの *_ind みたいなものは定義されないのでそういうときはFunctionで定義するか次の一行を書き加えよう。これでsplit_indという便利な命題が使えるようになる。

Functional Scheme split_ind := Induction for split Sort Prop.

　*_ind は普通はあんまり必要ないけれど、splitみたいに再帰呼び出しが二個前ごとに呼ばれるような関数だと便利なときがある。次のsplit関数の長さに関する補題を示すがそこでsplit_indは大活躍した。詳細が気になる人はソースコードを見てみよう。

Lemma split_length : forall zs xs ys,
  split zs = (xs, ys) -> length zs = length xs + length ys.
mergeとsplitを使ってmergesort関数を定義する

mergesort関数もやはり再帰関数だ。しかも停止性が明らかではないのでこの場合はFunctionで定義するのが有効だ。splitの結果は必ず長さが短くなるか等しいので長さに関して減ることを示す作戦でいこう。その場合はmeasureキーワードを使う。今回は引数は一つのリストなのでサイズを計る関数は単にlengthでおk。

Function mergesort (xs : list A) {measure length xs} : list A :=
  match xs with
  | nil => nil
  | x::nil => x::nil
  | x::y::zs =>
     match split (x::y::zs) with
     | (xs, ys) => merge (mergesort xs, mergesort ys)
     end
  end.

対話的証明でsplitの結果のリストがそれぞれ短くなっていることを証明できれば定義完了だ。Functionによる定義なので便利な mergesort_ind も得ることができる。

(i)を証明する

さあ、やっと目標の定理を証明すべきときがやってきた。今回のプロジェクトのラスボスだ。はりきって挑もう。

Theorem mergesort_sorted : forall xs, Sorted (mergesort xs).

ラスボスとは言いながらも実はこれまでの補題を使えば簡単にやっつけることができる。これで、今日からソートは安心して行うことができるね。よかったよかった。

OCaml合宿に行ってきた

OCaml OCaml合宿 ocaml-nagoya 車内証明

ocaml-nagoyaのプログラミング合宿に参加してきました。

一泊二日で長野の麻績(おみ)に行って、鍋も食べ、焼肉も食べ、酒も飲み、コーディングもして、発表もするというハードなスケジュールでしたが、久しぶりにocaml-nagoyaのメンバーにも会えて非常に充実した時間を過ごすことができました。

合宿の内容をyoshihiro503フィルターでまとめると

  • id:zyxwv さんがCoqを一日でかなり習得しちゃった。
  • FundepというGHC拡張を使ったid:keigoiさんの型レベルプログラミングが変態すぎる。
  • id:suer さんが「Coqle」という証明検索エンジン(Coq版のHoogle?)を作ろうとする。
  • 行き帰りの車で車内証明が盛り上がる。

行き帰りは10人乗りの車(マイクロバス？)で無線LAN有り、コンセント有りの非常に充実した環境でわいわいしながら移動しました。合宿に使った別荘は非常に広く、涼しくて快適でした。

合宿所と車はocaml-nagoyaのメンバーの方のご好意で使わせていただきました。大変感謝しています。

Coqで型クラス(Haskell風 モナドの定義)

Coq Monad Haskell モナド 型クラス Class Instance

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。

Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。

Coqでの型クラスは次のように宣言するみたいだ。

Class HMonad (M: Type -> Type) := {
   mreturn : forall {A}, A -> M A
 ; mbind : forall {A B}, M A -> (A -> M B) -> M B
}.

*1

この定義だとHaskellのモナドとあんまり変わらないが、Coqは証明も第一級の値なので、なんらか満たしてほしい性質を型で指定することができる。モナドはモナド則を満たしてほしいので、モナド則をみたしていないといけないクラスにしよう。

モナド則を加えるとちょうどこんな感じになった。

Class HMonad (M: Type -> Type) := {
  (* fields *)
   mreturn : forall {A}, A -> M A
 ; mbind : forall {A B}, M A -> (A -> M B) -> M B
  (* axioms モナド則 *)
 ; left_identity : forall A B (a: A) (f: A -> M B), mbind (mreturn a) f = f a
 ; right_identity : forall A (m: M A), mbind m mreturn = m
 ; associativity : forall A B C (m:M A) (f: A -> M B) (g: B -> M C),
       mbind (mbind m f) g = mbind m (fun x => mbind (f x) g)
}.

よし、じゃあ早速なにかインスタンスを作ってみよう。とりあえず簡単そうなMaybeにしよう。

証明の実装とか言われてもよくわかんないので、とりあえずmreturnとmbindの二つの関数だけを定義してみる。

Instance Maybe: HMonad option := {
   mreturn A x := Some x
 ; mbind A B m f :=
     match m with
     | None => None
     | Some x => f x
     end
}.

Coqのインスタンス定義では足りないフィールドがあっても対話的に与えることができる。モナド則の証明とかは対話的に証明した方が簡単そうなので、残りは対話的に与えよう。

coqtopのトップレベルでソースコードを書くか、ソースファイルを作って "-l" オプションで起動しよう。対話的な定理証明の始まりだ。

$ coqtop -l HMonad.v
Coq < 3 subgoals
  
  ============================
   forall (A B : Type) (a : A) (f : A -> option B), f a = f a

subgoal 2 is:
  ...
subgoal 3 is:
  ...

今回の証明はゴールにmatch式が出てきて盛りだくさんに見えるけど、こういうときは場合分けをすれば簡単だ。場合分けをするにはcaseタクティックが便利だ。ガンガン使おう。証明が全て終われば、モナド則が保証されたMaybeモナドの完成だ！

証明を含むソースコード全体は以下。

*1:ここでの{}で囲われたパラメータの書き方もCoq 8.2以降で追加された構文で、Agdaのそれと同じようなことを表している。つまり、このフィールドを使う側で{}で囲われたパラメータを書かなくても推論してくれるようにする構文だ。Coq 8.1以前では、Implicit Argumentsほげほげとか書かなくてはいけなかったのが、ちょっとシンプルに書けるようになっている。

続きを読む

OCaml Meeting と FLTV に行ってきました。

OCaml OCamlMeeting

OCaml Meeting に行ってきました。
id:camlspotterさんid:osiireさんid:keigoiさんharreさんid:mzpさんid:Gemmaさんそしてid:zyxwvさんおつかれさまでした。

OCaml入門者向けから、上級者向けまでさまざまな講演があって非常に楽しめました。OCamlという言語だけの会合でこれだけの人数が集まったのはすごいですね。

当日の講演のビデオと発表資料は以下のURLから得られます。
http://ocaml.jp/?Users%20Meeting

懇親会では北海道関数型言語勉強会からいらっしゃったtmaedaさんとお話できました。tmaedaさんは小さい会社でRubyを使っているということですが、Haskellなどの関数型言語にも興味があるとのことでした。

少年オッカムルのid:hamatsu1974さんと名刺交換できなかったのが残念。

OCaml Meetingの懇親会後(20時くらい)、FLTV(Future Language TV)の懇親会に乱入すべくチームラボに行ってみました。
しかし行ってみると、まだ発表中であと3人とのこと。かなり押している状況でした。

その日中に名古屋への終電が21:38だったので、結局kinabaさんのセッションの途中までしか参加できませんでした。
それでもがんばりやのid:ranhaさんとちょっとだけお話できたし、id:nihaさんにもお会いできてよかったです。
id:keigoiさん tmaedaさんありがとうございました。

こういう未来志向のイベントは素晴らしいと思うのでぜひfullで参加したかった。。。
次回はOCaml Meetingとかぶらないことを希望します。