2011-12-13 ssreflect ライブラリ紹介(eqType編) 
この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。
ssreflectライブラリ紹介
この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れば何か数学寄りだなというのが分かると思いますが、まあ完全に数学寄りです。しかもtrunkでは http://coqfinitgroup.gforge.inria.fr/ のように大変膨大になっております。
eqType
というわけで、一番根っこの部分にあるeqTypeを今回のメインにしましょう。
Coqを使い始めると、まあ誰でもこんな感じに書きたくなるでしょう。
Definition nat_gt0 := { x : nat | x > 0 }.
Definition nat_gt1 := { x : nat | x > 1 }.
Definition nat_gt0_succ : nat_gt0 -> nat_gt1 := (* うんたらかんたら *).
これにより、定義域を正の自然数に限定した関数 nat_gt0_succ が定義できました。プログラミングならこれでいいのですが、数学になると困ったことが起こります。例えば、この関数が単射であること:
Lemma nat_gt0_succ_inj : forall x y, nat_gt0_succ x = nat_gt0_succ y -> x = y.
これの証明は大変です。なぜかというと、xとyには各々が正であることの証明がくっついていますが、その証明が等しいことを示すのが困難だからです。すなわち、次のことを証明する必要があります。
Goal forall x (p1 p2 : x > 0), p1 = p2.
p1とp2はそれぞれxが正であることの証明で、それらが等しいことを示したいわけです。このように証明が等しいという性質をProof irrelevanceといいます。この問題の一番簡単な解決策は公理を導入することです。標準ライブラリの「Coq.Logic.ProofIrrelevance」を使うと「任意の命題がProof irrelevantである」が公理に追加されます。
ほとんどの場合で、この公理は不要です。eqTypeライブラリを使うとこの問題をほとんど解決してくれます。eqTypeは型クラスのようなもので、Canonical StructureというCoqの機能を使っています。まあほとんど型クラスのようなものです。eqTypeを実装した型Tは次の二つの値を持っています。
eq_op : T -> T -> bool. eqP : forall x y, reflect (x = y) (eq_op x y).
ここで、「reflect」は一つ目の命題と二つ目のbool値が同値であることを示します。すなわち、等値性を計算できるというのがeqTypeのもっている特長です。もちろん
eq_dec : forall x y, { x = y } + { x <> y }.
は上の二つと同値です。たったこれだけなので、導ける定理も少ないというか重要なのはただ一つだけで、「eq_irrelevance」はeqTypeを実装していれば、命題「x = y」はProof irrelevantであるになります。系として、
Lemma bool_irrelevance : forall (x y : bool) (p1 p2 : x = y), p1 = p2.
が得られます。よって、{ x : T | P x } の述語の部分を「f x = true」の形に書ける場合はこの型の値を簡単に比較できるわけです。ssreflectではbool -> PropのCoercionを「is_true」で定めているので、これは単に { x : T | f x } と書くことが出来ます。
subType
型 { x : T | f x } の持っているインターフェースを抽出した型クラスが subType になります。そして、eqTypeのsubTypeは自動的にeqTypeを実装します。他にもtupleとかmatrixなんかがsubTypeを使ってeqTypeを実装していたりします。
次回予告
次はchoiceライブラリ？ exists x, P xから { x | P x }を取り出せる性質をもった型クラスを紹介するかも。
2011-06-21 ICFPC2011参加記録(2)
■ Coq 
インタープリタ
https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltg.v
ここは急いで書いたのでバグがあるかもしれない。ただ、ここはデバッグするよりも証明したほうが早いと思う。
Inductive evalue : Set := | EValue : value -> evalue | EApp : evalue -> evalue -> evalue. Inductive eresult : Set := | EDone : value -> list trace -> board -> eresult | EFound : evalue -> list trace -> board -> eresult | EFail : list trace -> board -> eresult. step0 : player -> bool -> value -> value -> list trace -> board -> eresult.
この関数が関数適用を1つ実行する。引数は順に、プレイヤー・ゾンビ？・左の値・右の値・今までのトレース・盤面。
結果は、EDoneだと評価終了。EFoundだとまだ未評価の部分がある。EFailは失敗した。中には結果の値と追加されたトレースと評価後の盤面。
step : player -> bool -> evalue -> list trace -> board -> eresult.
この関数は次に実行すべき関数適用をみつけて、そこにstep0を適用する。実装は
Fixpoint step ev tr bd :=
match ev with
| EValue v => EDone v tr bd
| EApp (EValue v0) (EValue v1) => step0 v0 v1 tr bd
| EApp v0 ((EApp _ _) as v1) =>
match step v1 tr bd with
| EDone v1' tr bd' => EFound (EApp v0 (EValue v1')) tr bd'
| EFound v1' tr bd' => EFound (EApp v0 v1') tr bd'
| EFail tr bd' as e => e
end
| EApp ((EApp _ _) as v0) ((EValue _) as v1) =>
match step v0 tr bd with
| EDone v0' tr bd' => EFound (EApp (EValue v0') v1) tr bd'
| EFound v0' tr bd' => EFound (EApp v0' v1) tr bd'
| EFail tr bd' as e => e
end
end.
まさに教科書どおりに実装。引数を先に評価する正格評価では右側がEAppならそっちにすすんで、そうではなくて左側がEAppならそっちに進んで、そうでなければ両辺とも評価済みなので関数適用を評価。
eval : player -> bool -> nat -> evalue -> list trace -> board -> eval_result.
最後にこれで、step0を与えられた回数実行する。
残り評価回数を引数にした再帰関数を回さないのはなぜかというと、それはかなり難しいからです。グローバル変数にしたくなる気持ちがよくわかります。
■ モナド 
https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltgmonad.v
二つのモナドを用意しました。cmdexモナドとaicmdモナドです。
cmdexモナドは一つのスロットで実行される命令列を作ります。
putl;; zeror;; succl;; dbll;; getl
こんな感じに書くと、左put右zero左succ左dbl左getを順に実行します。
ExStateの型はcmdex stateiで、現在の状態を返します。stateiにはプレイヤーと盤面と実行中のスロット番号が入っています。よって
Definition p (c : card) : cmdex unit :=
let v := value_of_card c in
s <- ExState;
let v' = getf (sti_board s) (sti_player s) (sti_i s) in
if eqvalue v v' then
ret tt
else
clear;; ExRight c
みたいに書くことで、現在の状態を見て判定するようなスロットの初期化なんてのを書けたりするわけです。
aicmdモナドはAIを作ります。arunはスロット番号を指定してcmdexモナドを実行します。
arun 0 (putl;; zeror;; succl;; dbll;; getl);; arun 1 (putl;; zoerr;; getl)
AiStateはaicmd state型でスロット番号がない以外はExStateと同じです。
STモナドの機能も実装しました。
AiNew : forall T, T -> aicmd (ptr T). AiRead : forall T, ptr T -> aicmd T. AiWrite : forall T, ptr T -> T -> aicmd unit.
AiNewでポインタを作成して、AiRead/AiWriteで読み書きします。
■ セクション 
Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。
Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section の中では x はグローバル変数みたいに使える *) End Hoge. (* Section を閉じると、foo と bar は x を引数にとるようになる *) Definition baz := bar 42.
この機能とポインタを一緒に使うと変更できるグローバル変数みたいに使えます。
Section Foo.
(* 最後にスロット8に置いた、ヒーラー。まだ置いてなければ None *)
Variable heal_4095_at_8 : ptr (option value).
(* スロットnにヒーラーが設置されている？ *)
Definition check_healer n : aicmd bool :=
v <- myfld n; (* 自分とこのスロットnを読む *)
v' <- AiRead heal_4095_at_8; (* スロット8に置いたかどうか *)
match v' with
| Some v'' => ret (eqvalue v v'')
| None => ret false
end.
Definition make_healer :=
ifb check_healer 8
then
ret tt
else
arun 8 (...);; (* がんばってヒーラーを作る *)
v <- myfld 8;; (* できあがった値を読み出す *)
AiWrite heal_4095_at_8 (Some v). (* ポインタに覚えておく *)
End Foo.
みたいな感じ。これは未来のプログラム言語に違いない！
cmdexの中ではポインタの操作はできないので、ためしにcmdexを実行してうまくいくか試すなんてことができるはず。でも本当は複数のarunをグループ化してそれをしたいわけなので、ポインタ部分はaicmdから分離すべき。
今の実装は公理の中に
Axiom ptr : Type -> Type.
Axiom make_ptr : forall {T}, T -> ptr T.
Axiom read_ptr : forall {T}, ptr T -> T.
Axiom write_ptr : forall {T}, ptr T -> T -> unit.
■ モナドのインタープリタ 
モナドを実行するインタープリタを書かないといけません。必要なのはaicmdを受け取って、次に実行するコマンドと残りのaicmdを返す関数です。OCaml側がその関数を順に呼び出します。
とりあえずの実装なので、動くんだけど効率とかよくないし直したい。継続を返すようにするともっと効率がよくなる気がするし、よく考えたらCoFixpointで実装してもいい気がする。多分。
最初のフェーズはモナドの先頭部分がコマンドになるまで、bindを崩していきます。
hnf_cmd : forall A, cmdex A -> cmdex A. hnf_ai : forall A, aicmd A -> aicmd A.
がそれを行います。match in return withが飛び交う修羅場になっています。
hnf_cmdはコマンドcを受け取ると、cで場合分けして
よく考えると、ExNopは必要ないです。ret ttを使えばいいので。
hnf_aiはほとんど同じですが、arun に対しては hnf_cmd を呼び出します。
2011-06-20 ICFPC2011参加記録
例年のごとく一人で参加。
時刻は全てUTCで
17日
- 00:00 問題が公開されたので読む。予想通り殴り合いゲーだ。
- 01:00 大体問題を理解したので、インタープリタを書き始めてみる。言語はOCamlを選択。というかこれ以外に選択肢がない
- 03:00 電車で会社に移動しながら戦略を考える。最大のダメージを与えられるのはゾンビなのが分かる
- 04:00 インタープリタの続きを実装
- 10:00 このころにはインタープリタはできてたはず。SKIの使い方を考え始める
- 11:00 無限ループを参考に、S(get)(SK(dec))0が無限dec 0であることに気づくが実装できない。
- 12:00 S(Kx)yz = x(yz)に気づく。無限dec 0の動作を確認する。
- 13:00 lazyを発見する。これにより動的にgetできるようになる。
- 14:00 電車で帰宅。作戦を考える。
- 15:00 ほぼ部品は整ったので、最初のAIの作成にとりかかる。作戦はすぐに決まる。
- 21:00 最初のAIが完成する。送信。風呂って寝る。
18日
- 09:00 活動開始。今のリスト再生AIを拡張するのは無理なので、書きやすい記法を考えようとする。
- 10:00 モナドが最適なことが分かる。OCamlで書こうとするがいまいちしっくりこない。
- 11:00 OCamlの型システムと演算子定義がクソだからいけない。そういえばYnotのモナドはかっこよかった。Coqで書いてOCamlに抽出すればいいんじゃね？
- 12:00 Coqでコード書くのたのしいお
19日
■ 詳細 
https://github.com/kik/ICFPC2011
インタープリタ
ゲーム中に存在する全ての値を
type value = | ValNum of int | ValI | ValSucc | ValDbl | ValGet | ValPut | ValS | ValSf of value | ValSfg of value * value | ValK | ValKx of value | ValInc | ValDec | ValAttack | ValAttacki of value | ValAttackij of value * value | ValHelp | ValHelpi of value | ValHelpij of value * value | ValCopy | ValRevive | ValZombie | ValZombiei of value
といった感じで、完全に記述できる型を用意するのが常識だと思っていたんだけど、まわりのコード眺めてるとそうなってなくてびっくりした。
最初のAI
https://github.com/kik/ICFPC2011/blob/d67edcf101921b1fe72f449799b479cc9c6d8a1a/src/kamaboko.ml
まず、全力で5000と10000を作る。5000で三回攻撃して255を倒す。
次に、255をゾンビ化して0を速攻で倒す。
succ zombieを繰り返す
何もしないAIは650ターンで死ぬ。動くこと優先で書いたのだが、この時点ではかなり速かったらしい。
helpで倒すようにすれば256ターン減らせるので、すでに最速の2倍ちょいくらいにはなっていたらしい。
2011-05-15 Google Code Jam 2011予選
■[Coq] A問題をやっと解けた。一週間もかかったよ 
https://gist.github.com/971586
色々と工夫してみた。
ロボットと指令の定義。これは前と同じ。
Inductive Robo : Set := Blue | Orange. Inductive Order : Set := order : Robo -> Z -> Order. Definition robo_inv (robo: Robo) := match robo with | Blue => Orange | Orange => Blue end.
移動命令の定義。ボタンを押すを移動から分離した。さらにどっちのロボットへの命令なのかを型にいれることにした。
Inductive Move (robo: Robo) : Set := Left | Right | Stay. Inductive Moves : Set := | moves : Move Blue -> Move Orange -> Moves | pushmove (roboPush: Robo) : Move (robo_inv roboPush) -> Moves.
型「Move Blue」は青ロボットの移動を値として持つ。各ロボットへの命令の組は両方移動するか、片方がボタンを押して残りが移動するだけなので、上の２つだけにした。pushmoveにボタンを押すロボットを指定すると移動するほうのロボットの移動しか渡せなくなるように型を付ける。
各ロボットの座標の組の定義
Record ZZ : Set := zz {
pB : Z;
pO : Z
}.
(* 略 *)
Definition do_move (r: Robo) (m: Move r) (p: ZZ) :=
match m with
| Left => paddz r p (-1)
| Stay => p
| Right => paddz r p 1
end.
これによって、Move Blue型の値をdo_moveに渡すとBlueの座標が変化する。引数rは暗黙引数にできる。
ふたつのロボットを同時に動かす場合はこんな感じ。
Definition do_moves (mb: Move Blue) (mo: Move Orange) (p: ZZ) := do_move mb (do_move mo p).
移動命令のリストが指令のリストに正しく則っているかの述語。「Correct pfrom pto os ms」は位置pfromから命令列msでロボットを動かすと、指令列osの順にボタンを押して、最終的に位置ptoにくるという述語。
Inductive Correct (pfrom: ZZ) : ZZ -> list Order -> list Moves -> Prop :=
| c_nil:
Correct pfrom pfrom nil nil
| c_moves (mb : Move Blue) (mo : Move Orange) os ms pto:
Correct (do_moves mb mo pfrom) pto os ms ->
Correct pfrom pto os (moves mb mo::ms)
| c_pushmove (r : Robo) (mv: Move (robo_inv r)) os ms pto:
Correct (do_move mv pfrom) pto os ms ->
Correct pfrom pto (order r (pfrom r)::os) (pushmove mv::ms).
この述語が真に成るのは次の場合のみ
- ms=nilのときは、pfrom=ptoでos=nilのとき
- ms=moves mb mo::ms'のときは、pfromをmbとmoで動かした結果をpfrom'とすると、Correct pfrom' pto m's osが成立するとき
- ms=pushmove r mv::ms'のときは、pfromをmvで動かした結果をpfrom'とする。さらにos=o::os'で、oはロボットrがpfrom rでボタンを押す命令であり、Correct pfrom' pto ms' os'も成立するとき
というように問題を整理しなおしたので、多少は証明が簡単にはなって、このあと700行ぐらいがんばった結果
minimum_moves : list Order -> list Moves.
という最小の移動リストを返す関数が完成して、
Example sample_2 := order Orange 2:: order Blue 1:: order Blue 2:: order Orange 4:: nil. Eval vm_compute in (minimum_moves sample_2).
の結果
= moves (Stay Blue) (Right Orange)
:: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
:: pushmove (roboPush:=Blue) (Right (robo_inv Blue))
:: moves (Right Blue) (Right Orange)
:: pushmove (roboPush:=Blue) (Stay (robo_inv Blue))
:: pushmove (roboPush:=Orange) (Stay (robo_inv Orange))
:: nil
: list Moves
2011-05-14 Coqで有理数 with Leibniz equality
■[Coq] 標準ライブラリの有理数って、Leibniz equalityじゃないから 
微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。
https://gist.github.com/971135
まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。
次に、この同値関係で割ったときの代表元を返す関数を作る。canceled: ZP -> ZP。普通に約分しつくした形を代表元にする。
そして、魔法のような eq_irrelevance を証明する。
最後に ZP の部分集合 { x | canceled x = x } をQとする。これはもちろん代表元全体の集合だ。
仕上げに魔法のように Q_eq_dec を ZP_eq_Q_eq を証明する。