何をとち狂ったか

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

Inductive OrderRel : Set := orderRel : Robo -> comparison -> Z -> OrderRel.

Fixpoint translateRel_aux (bp op: Z) (os: list Order) : list OrderRel :=
match os with
| nil => nil
| order Blue bp'::os' =>
  orderRel Blue   (bp ?= bp') (Zabs (bp - bp')) :: translateRel_aux bp' op os'
| order Orange op'::os' =>
  orderRel Orange (op ?= op') (Zabs (op - op')) :: translateRel_aux bp op' os'
end.

Definition translateRel (os: list Order) := translateRel_aux 0 0 os.

というのができたわけです。どう考えても問題を複雑にしてるだけです。これを使ったときの最小手数関数は

Definition Zmax0 := Zmax 0.

Fixpoint min_movesRel_aux (bp op: Z) (os: list OrderRel) :=
match os with
| nil => 0
| orderRel Blue   _ bp'::os' =>
  let n := Zmax0 (bp' - bp) + 1in
  n + min_movesRel_aux 0 (op + n) os'
| orderRel Orange _ op'::os' =>
  let n := Zmax0 (op' - op) + 1in
  n + min_movesRel_aux (bp + n) 0 os'
end.

Definition min_trans bp op bp' op' os :=
  min_movesRel_aux bp op (translateRel_aux bp' op' os).

もはや、再起呼び出しの中で現在位置を覚えておく必要はありません。ゆとり引数だけ回していたらいいわけです。完成した「min_trans」関数は現在のゆとりポイントの初期値と初期位置と命令列を引数にとって、最小手数を返します。