ゆとりポイントの逆襲

とりあえずロボットの初期位置をひとつだけずらした状態でmin_transを呼び出すと値が２以上減ることはないということを証明しましょう。

Lemma min_trans_le:
  forall (os: list Order) (bp op bp' op' bd od :Z),
    -1 <= bd <= 1 -> -1 <= od <= 1 ->
    min_trans bp op (bp'+bd) (op'+od) os <= min_trans bp op bp' op' os + 1.

初期位置がひとつ違うということは、最初にボタンを押すロボットが１ターン早くボタンを押せる場合があるわけです。１ターン早くボタンを押すと、もう片方のロボットにたまるゆとりポイントが１だけ少なくなります。ゆとりポイントが減ると、そのロボットが次のボタンを押すのにかかるターン数が１ターン余計にかかる場合があるわけです。ボタンを押すのに１ターン余計にかかると最初のロボットにたまるゆとりポイントが増える場合があります。ゆとりポイントが増えるとボタンを１ターン早く押せます。もはやわけがわかりません。

このようにループ間で参照される変数というのを特徴付けるのは非常に難しいのです。

というわけで、問題はゆとりポイントの増減が結果にどう影響するのかということになりました。結論からいうと

Lemma min_movesRel_aux_1_1:
  forall (os: list OrderRel) (bp op: Z) (bd od: Z),
    0 <= bd <= 1 -> 0 <= od <= 1 ->
      min_movesRel_aux (bp+bd) (op+od) os <= min_movesRel_aux bp op os <= min_movesRel_aux (bp+bd) (op+od) os + 1.

ようするに、各ロボットのゆとりポイントを高々１だけ増やしても、結果は変わらないか１減るかの場合しかないわけです。この不等式を定式化するのにほとんどの時間を費やしました。前に書いたようにゆとりポイントが増えると、後で他のロボットのポイントが減ることになったりするので、この不等式を両方同時に帰納法で証明しないといけません。