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.

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

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