とりあえず、これより短い手順がないこと

これより短い手順がないことを証明するには、手順とはなにかを定義しないといけません。

Inductive Move : Set := Left | Right | Push | Stay.
Inductive Moves : Set := moves : Move -> Move -> Moves.

各ロボットは１ターンに４種類の行動ができて、青のと橙のとの行動のペアが１ターンの手になります。list Movesが手順になります。

この手順が命令列を正しく実行するかの述語が必要です。

Definition correct_moves (bp op: Z) (ms: list Moves) (os: list Order) := (* 略 *).

この述語はロボットの初期位置と手順と命令列を引数にとって、その手順でロボットを動かすと命令列の通りにボタンが押されることをあらわす述語です。中身はかなりめんどくさいです。

証明したいことは、正しい手順の長さはさっきの関数の返り値以上であること

Lemma correct_moves_min:
  forall (ms: list Moves) (bp op: Z) (os: list Order),
    correct_moves bp op ms os ->
    min_trans 0 0 bp op os <= Z_of_nat (length ms).

うわあ。こんなのどうやって証明するんだよ