2011-05-15

A問題をやっと解けた。一週間もかかったよ

Coq

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

標準ライブラリの有理数って、Leibniz equalityじゃないから

Coq

微妙に使いにくいじゃないですか。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 を証明する。

2011-05-09

A問題が如何に難しかったか

Coq

起きたらすでに残り14時間とかどこかおかしい。

A問題はこんなかんじ

青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。
指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。
各ロボットは最初に1の位置にいて、各々1ターンに「左右に一歩移動」「ボタンを押す」「何もしない」の行動ができます。
指令通りのボタンを押し終えるまで最短で何ターンかかるでしょう？ただしボタンを同時に押してはいけません

はいはいグリーディー。貪欲にやれば正解です。こんなのグリーディーにやる以外にないし、あまりに自明すぎて証明する必要も感じられません。しかし、今回は最近話題のCoqで解くことにしたので、こんな当たり前のことでも証明しないといけないのです。証明すればバグに悩むこともありません。

とりあえず、ロボットのenumを作りましょう。命令はロボットと位置を表す整数のペアです。

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

で、list Orderを受け取って最短手数を返す関数を書けばいいんですよ

(* 距離を計算してゆとりポイントを負にならないように引く *)
Definition yutori_minus (x y z: Z) := Zmax 0 (Zabs (x - y) - z).

Fixpoint minimum_aux (bp op bx ox: Z) (os: list Order) :=
match os with
| nil => 0
| order Blue bp'::os' =>
    let n := yutori_minus bp' bp bx + 1 in
    n + minumum_aux bp' op 0 (ox + n) os'
| order Orange op'::os' =>
    let n := yutori_minus op' op ox + 1 in
    n + minumum_aux bp op' (bx + n) 0 os'
end.

Definition minimum (os: list Order) := minimum_aux 1 1 0 0 os.

開始地点とゆとり引数と命令列を引数にとって、次にボタンを押すロボットは全力で押しに行って、その間もう一個のロボットは何かする代わりにゆとりポイントを貯めて、次にそのロボットを動かすときはゆとりポイントを消費するようにすればできあがり。

あとはこれが最小値を返してることを証明すれば終わり！こんな綺麗な再起呼び出ししかしてない関数の証明なんて簡単です！