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

と、実際に動くプログラムが完成して、しかもこれが最短であることも証明できた。