ここまでくれば、どんな手順を渡されても、最初の一手は基本的にロボットを一歩動かすだけなので、簡単な作業になります。最初の一手は青の動かし方が４通りあって、橙の動かし方が４通りありますから全部で (coq Scripting *16 SUBGOALS* Holes)---------残…

ここまで証明できればあと少しです。初期位置の違いはゆとりポイントの初期値の違いと等価なはずです。 Lemma min_trans_1_0: forall (os: list Order) (bp op bp' op' bd:Z), Zabs bd = 1 -> exists d, Zabs d = 1 /\ min_trans bp op (bp'+bd) op' os = mi…

とりあえずロボットの初期位置をひとつだけずらした状態でmin_transを呼び出すと値が２以上減ることはないということを証明しましょう。 Lemma min_trans_le: forall (os: list Order) (bp op bp' op' bd od :Z), -1 <= bd <= 1 -> -1 <= od <= 1 -> min_tra…

状態Ａから適当に１ターン動かして状態Ｂになったとします。Ａでの結果をmin_trans(A)としてＢのときをmin_trans(B)と書くことにすると min_trans(A) ≦ min_trans(B) + 1であることを証明できれば、min_transより短い手順で解くことは出来ません。どんなにが…

これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。 Inductive Move : Set := Left | Right | Push | Stay. Inductive Moves : Set := moves : Move -> Move -> Moves.各ロボットは１ターンに４種類の行動ができて、青の…

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

証明することは、この関数が最小手数を返していることです。最小手数であるというのはどういうことかというと、 どんな手順でロボットを動かしても、これより短くできない手数 のことです。というのは残念ながらよくある間違いです。 ある手順でロボットを動…

起きたらすでに残り14時間とかどこかおかしい。A問題はこんなかんじ 青と橙のロボットがいます。ロボットを動かして指令通りの順番でボタンを押させます。指令は「O 2, B 1, B 2, O 4」のようにどのロボットがどのボタンを押すかの列で与えられます。各ロボ…