この記事はTheorem Proving Advent Calendar 2011の13日目の記事です。 ssreflectライブラリ紹介 この前はssreflectのtacticの紹介をやったので、ライブラリの紹介をします。ライブラリの概要は http://coqfinitgroup.gforge.inria.fr/ssreflect-1.3/ を見れ…

モナドを実行するインタープリタを書かないといけません。必要なのはaicmdを受け取って、次に実行するコマンドと残りのaicmdを返す関数です。OCaml側がその関数を順に呼び出します。とりあえずの実装なので、動くんだけど効率とかよくないし直したい。継続を…

Coqのセクションという機能を使うとグローバル変数みたいなのを使えます。 Section Hoge. Variable x : nat. Definition foo := x + 1. Definition bar := foo + 2. (* Section の中では x はグローバル変数みたいに使える *) End Hoge. (* Section を閉じる…

https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltgmonad.v二つのモナドを用意しました。cmdexモナドとaicmdモナドです。cmdexモナドは一つのスロットで実行される命令列を作ります。 putl;; zeror;; succl;; dbll;; getlこんな感じに書くと、左put…

インタープリタ https://github.com/kik/ICFPC2011/blob/master/src/coq/Ltg.vここは急いで書いたのでバグがあるかもしれない。ただ、ここはデバッグするよりも証明したほうが早いと思う。 Inductive evalue : Set := | EValue : value -> evalue | EApp : e…

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 | ValD…

例年のごとく一人で参加。時刻は全てUTCで 17日 00:00 問題が公開されたので読む。予想通り殴り合いゲーだ。 01:00 大体問題を理解したので、インタープリタを書き始めてみる。言語はOCamlを選択。というかこれ以外に選択肢がない 03:00 電車で会社に移動し…

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…

微妙に使いにくいじゃないですか。ssreflectを読んでたら、こういうのを簡単に Leibniz equality にする方法が分かったので書いてみた。https://gist.github.com/971135まず、ZP = Z * positive の上に普通に同値関係を定義する ZP_eq : ZP -> ZP -> Prop。…

ここまでくれば、どんな手順を渡されても、最初の一手は基本的にロボットを一歩動かすだけなので、簡単な作業になります。最初の一手は青の動かし方が４通りあって、橙の動かし方が４通りありますから全部で (coq Scripting *16 SUBGOALS* Holes)---------残…

ここまで証明できればあと少しです。初期位置の違いはゆとりポイントの初期値の違いと等価なはずです。 Lemma min_trans_1_0: forall (os: list Order) (bp op bp' op' bd:Z), Zabs bd = 1 -> exists d, Zabs d = 1 /\ min_trans bp op (bp'+bd) op' os = mi…

とりあえずロボットの初期位置をひとつだけずらした状態でmin_transを呼び出すと値が２以上減ることはないということを証明しましょう。 Lemma min_trans_le: forall (os: list Order) (bp op bp' op' bd od :Z), -1 <= bd <= 1 -> -1 <= od <= 1 -> min_tra…

状態Ａから適当に１ターン動かして状態Ｂになったとします。Ａでの結果をmin_trans(A)としてＢのときをmin_trans(B)と書くことにすると min_trans(A) ≦ min_trans(B) + 1であることを証明できれば、min_transより短い手順で解くことは出来ません。どんなにが…

これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。 Inductive Move : Set := Left | Right | Push | Stay. Inductive Moves : Set := moves : Move -> Move -> Moves.各ロボットは１ターンに４種類の行動ができて、青の…

なんとなく、押すボタンの位置を前回の位置からの相対距離で覚えておいたほうが簡単かなあと思っちゃったんですよ。で、相対位置に変更した命令の型と相対位置に変換する関数。 Inductive OrderRel : Set := orderRel : Robo -> comparison -> Z -> OrderRel…

証明することは、この関数が最小手数を返していることです。最小手数であるというのはどういうことかというと、 どんな手順でロボットを動かしても、これより短くできない手数 のことです。というのは残念ながらよくある間違いです。 ある手順でロボットを動…

起きたらすでに残り14時間とかどこかおかしい。A問題はこんなかんじ 青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。各ロボ…

http://d.hatena.ne.jp/nishiohirokazu/20110217こういう話は確率の問題をどのように数学で定義しているかっていう哲学的な話が繋がってないから、数式だけ見てこれとこれの違いが分からないってことになってるんだと思う。確率は突き詰めていくと、いつかは…

COUNTI: がんばった３位 HASH: がんばったのに８位 LETTER: やる時間なかった KD: がんばった３位 ARRNG: 通しただけ８位 HEART: 遊びすぎた ODDEVEN: がんばった３位 OPTI: ひょろっと書いたモンゴメリ乗算だけでは30倍遅い こんなもん作ってないで真面目に…