Coqで多変数多項式の簡約
変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。
Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp.
ここで binop型の値は二項演算子(binary operation)の種類(＋または×)を表すものとして以下で定義されるものとし、定数項は簡単のため自然数(nat)に限るとする。
Inductive binop : Set := Plus | Times.
つまり、この定義のもとでは以下のように多項式が表現される。
| 多項式 | Coqでの表現 |
|---|---|
| Binop Plus (Var 0) (Const 1) | |
| Binop Plus (Binop Times (Var 0) (Var 0)) (Binop Times (Var 1) (Var 1) |
各変数から値への対応 (var -> nat) を環境として、ある環境ctxにおける式eの意味を次で再帰的に与える。
Fixpoint expDenote (ctx: var -> nat) (e : exp) : nat := match e with | Var v => ctx v | Const n => n | Binop b e1 e2 => (binopDenote b) (expDenote ctx e1) (expDenote ctx e2) end.
そして式e1とe2の意味が同じという事を ctx, expDenote ctx e1 = expDenote ctx e2として考える事ができる。
ここで式eに対して、定数部分に関する部分的に簡単な形にする畳み込み関数を次で定義し、その健全性を示す。
Fixpoint constFold (e : exp) : exp := match e with | Var v => Var v | Const n => Const n | Binop b e1 e2 => match (constFold e1, constFold e2) with | (Const m, Const n) => Const ((binopDenote b) m n) | (e1', e2') => Binop b e1' e2' end end.
eを深さ優先に探索し、定数同士の2項演算を評価している。
ここで、この部分的な評価関数において、式eの意味が絶対変わらないことを証明する。
Lemma const_fold_preserved : forall e ctx, expDenote ctx e = expDenote ctx (constFold e). Proof.
induction e. reflexivity. reflexivity. intro ctx; simpl; rewrite IHe1; rewrite IHe2. destruct (constFold e1); destruct (constFold e2); reflexivity. Qed.
今回のネタはCPDTのExcercise 3.2 から取ってきた。CPDTはCoqでプログラムするときに必要な知識や便利な技を紹介していて非常にためになるので、Coqプログラミングをやりたい人にはぜひともオススメである。また、現在CPDTを勉強しているグループはFormal Method勉強会やProofCafe - coqグループなどあるので、参加してみてはいかがだろうか。
ソースコード全体と問題文は以下: http://ideone.com/kGLVw
OCamlerのためのCoq便利モジュールを公開してみた
このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。
ダウンロード: http://sourceforge.jp/projects/coqbase/
具体的には以下のことを定義した。
迷路の試験問題を解いてみた
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。
Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。
まず、accessiblesという関数を定義し、以下の性質を証明した。
ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。
Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end.
この関数はstartから始まってlenの長さのパスが到達できる点(を終点とするパス)全体を返す関数を表現している。
Theorem soundness : forall x n p, In p (accessibles x n) -> Path x p /\ plength p = n.
この定理は「リスト(accesibles x n)のすべての元pはPath x pかつ長さがnである。」ということを言っている。
Theorem completeness : forall x p, Path x p -> exists p0, endof p = endof p0 /\ plength p = plength p0 /\ In p0 (accessibles x (plength p)).
これは「xからのパスpが存在するならば、pと同じ終点にたどり着き、pと同じ長さであるようなp0が(accesibles x (plength p))の中に存在する。」ということ。
停止しない処理をCoqで記述できないため、結果を無限リストとして定義し、OCamlに渡した。OCaml側では無限リストを順番に見ていき、解があれば出力する。
上記の定理より、パスの長さに関して同一視するとすべてのゴールへたどるパスは得られる無限リストに含まれており、無限リストは短い順に並んでいる。よって無限リストを順番にみた結果見つかった解が最短であることが保証される。
ソースコード全体は以下。
http://bitbucket.org/yoshihiro503/maze_solver/src/
実行結果
$ cat input.txt ************************** *S* * * * * * * ************* * * * * ************ * * * * ************** *********** * * ** *********************** * * G * * * *********** * * * * ******* * * * * * **************************
$ time ./run < input.txt ************************** *S* *$$$$$ * *$* *$ * $************* * *$*$$$* $$************ * *$$$ * $$$$$ * **************$*********** * $$$$$$$$$$$$$ * **$*********************** * $$$$$*$$$$$$$$$$$$$$G * * * $$$ *********** * * * * ******* * * * * * ************************** real 0m0.129s user 0m0.124s sys 0m0.000s
Coqで多重再帰のデータ構造を証明する
Coqでは一重の再帰的なデータは例えば次の様に定義できる。
Inductive list (A: Set) : Set := Nil | Cons (x: A) (xs: list A).
Coqでは再帰的データ型をInductiveコマンドで定義した場合、その型の他に list_ind というものがついでに定義される。
list_indは次の様な型を持っている。
Coq < Check list_ind. list_ind : forall (A : Set) (P : list A -> Prop), P (Nil A) -> (forall (x : A) (xs : list A), P xs -> P (Cons A x xs)) -> forall l : list A, P l
このlist_indは帰納法に関して非常に強力である。
リストを引数に持つような任意の述語Pに対して apply list_ind. をすればこのlistに関して構造的な帰納法で証明をすることができる。
また、そのための特別な induction という tactic さえ用意されている。
ただし、この *_ind は多重再帰のデータ型に関してはしょぼい物になってしまうという問題を発見した。*1
多重再帰のデータ型とは例えば相互再帰になっているものや次の様に再帰構造が入れ子になっているものだ。
module HTML. Inductive elem : Set := | PCDATA (_: string) | TAG (_: list elem).
このとき先ほどと同様に elem_ind が定義されるが、それは次の型になっている。
Coq < Check elem_ind. elem_ind : forall P : elem -> Prop, (forall s : string, P (PCDATA s)) -> (forall l : list elem, P (TAG l)) -> forall e : elem, P e
しかしこの形だとTAGの場合の帰納法の仮定で、小要素に関して帰納的に証明することができない。
この問題を解決するために以下の項を定義した。
Fixpoint elem_ind0 (P : elem -> Prop) (H1 : forall s : string, P (PCDATA s)) (H2 : P (TAG nil)) (H3 : forall e es, P e -> P (TAG es) -> P (TAG (e :: es))) (e : elem) : P e := match e as x return P x with | PCDATA s => H1 s | TAG es => list_ind (fun xs => P (TAG xs)) H2 (fun a l H => H3 a l (elem_ind0 P H1 H2 H3 a) H) es end.
ちょっと苦労したが、これで以下の型の項を得ることができた。これを使えばelem型の帰納法もばっちりだ。
Check elem_ind0 : forall P : elem -> Prop, (forall s : string, P (PCDATA s)) -> (P (TAG nil)) -> (forall e es, P e -> P (TAG es) -> P (TAG (e :: es))) -> forall e : elem, P e
*1:これはv8.2pl1時点の話。将来的にこの問題は改善するかもしれない。
Proof Party の問題をCoqで挑戦してみた。
Proof Party に行けないけど、参加してるつもりで問題に挑戦してみた。今日は名古屋で一人証明パーティ。パズルと応用問題は解いていない。
東京は遠いので、Proof Partyの次回がもしあれば 名古屋か関西で開催していただければありがたいです。> ranhaさん
Coqでハノイの塔に関する証明
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 プログラムをつくってみた
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
以下、開発した手順にそって詳細を説明する。
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番目を取ってきて、オプション型で値を返す関数だ。これはだいたいならば
であることを表現している。
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).
ラスボスとは言いながらも実はこれまでの補題を使えば簡単にやっつけることができる。これで、今日からソートは安心して行うことができるね。よかったよかった。
