GCJ 2011 Qual-A 全然だめぽ。下界のひとつを与えられたけど最小かどうか証明できてないバージョン

A.v

Require Import ZArith.
Require Import Zminmax.
Require Import List.
Open Scope Z_scope.

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order : Robo -> Z -> Order.

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

Lemma Robo_eq_dec (x y: Robo) : { x = y } + { x <> y }.
Proof. decide equality. Defined.

Lemma Order_eq_dec (x y: Order) : { x = y } + { x <> y }.
Proof. decide equality. apply Z_eq_dec. apply Robo_eq_dec. Defined.

Definition do_move (m: Move) (p: Z) :=
match m with
| Push  => p
| Left  => p-1
| Stay  => p
| Right => p+1
end.

Record State : Set := state {
  blue_pos: Z;
  orange_pos: Z;
  orders: option (list Order)
}.

Definition play_one_move (st: State) (m: Moves) :=
match orders st with
| None => st
| Some os =>
  match os with
  | nil => st
  | o::os' =>
    match m with
    | moves Push Push  => state 0 0 None
    | moves Push mo =>
      if Order_eq_dec (order Blue (blue_pos st)) o then
        state (blue_pos st) (do_move mo (orange_pos st)) (Some os')
      else
        state 0 0 None
    | moves mb Push =>
      if Order_eq_dec (order Orange (orange_pos st)) o then
        state (do_move mb (blue_pos st)) (orange_pos st) (Some os')
      else
        state 0 0 None
    | moves mb mo =>
      state (do_move mb (blue_pos st)) (do_move mo (orange_pos st)) (Some os)
    end
  end
end.

Definition play_moves (ms: list Moves) (st: State) :=
  fold_left play_one_move ms st.

Definition correct_moves (bp op: Z) (ms: list Moves) (os: list Order) :=
  let st := play_moves ms (state bp op (Some os)) in
  orders st = Some nil.

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).

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 = min_trans (bp+d) op bp' op' os.
Proof.
  induction os.
  unfold min_trans. simpl. exists 1. auto.
  unfold min_trans. simpl.
  intros.
  assert (bd = -1 \/ bd = 1).
  destruct (Zabs_dec bd); omega.
  destruct a as [[|] pp]; simpl.
  destruct (Ztrichotomy bp' pp) as [|[|]].
  exists bd. split. auto.
  replace (Zabs (bp' + bd - pp) - bp) with (Zabs (bp' - pp) - (bp + bd)).
  auto.
  rewrite (Zabs_non_eq (bp' - pp)).
  rewrite (Zabs_non_eq (bp' + bd - pp)).
  omega. omega. omega.
  exists (-1). split; auto with zarith.
  replace (Zabs (bp' + bd - pp) - bp) with (Zabs (bp' -pp) - (bp + -1)).
  auto.
  rewrite (Zabs_non_eq (bp' - pp)).
  replace (bp' + bd - pp) with bd by omega.
  omega. omega.
  exists (-bd). split. rewrite (Zabs_Zopp). auto.
  replace (Zabs (bp' + bd - pp) - bp) with (Zabs (bp' - pp) - (bp + -bd)).
  auto.
  rewrite (Zabs_eq (bp' - pp)).
  rewrite (Zabs_eq (bp' + bd - pp)).
  omega. omega. omega.

  destruct (IHos (bp + (Zmax0 (Zabs (op' - pp) - op) + 1)) 0 bp' pp bd) as [d [H1 H2]].
  auto.
  exists d. split. auto.
  unfold min_trans in H2.
  replace (bp + d + (Zmax0 (Zabs (op' - pp) - op) + 1))
     with (bp +(Zmax0 (Zabs (op' - pp) - op) + 1) + d).
  omega.
  omega.
Qed.

Lemma min_trans_0_1:
  forall (os: list Order) (bp op bp' op' od:Z),
  Zabs od = 1 ->
  exists d, Zabs d = 1 /\
    min_trans bp op bp' (op'+od) os = min_trans bp (op+d) bp' op' os.
Proof.
  induction os.
  unfold min_trans. simpl. exists 1. auto.
  unfold min_trans. simpl.
  intros.
  assert (od = -1 \/ od = 1).
  destruct (Zabs_dec od); omega.
  destruct a as [[|] pp]; simpl.

  destruct (IHos 0 (op + (Zmax0 (Zabs (bp' - pp) - bp) + 1)) pp op' od) as [d [H1 H2]].
  auto.
  exists d. split. auto.
  unfold min_trans in H2.
  replace (op + d + (Zmax0 (Zabs (bp' - pp) - bp) + 1))
     with (op +(Zmax0 (Zabs (bp' - pp) - bp) + 1) + d).
  omega.
  omega.

  destruct (Ztrichotomy op' pp) as [|[|]].
  exists od. split. auto.
  replace (Zabs (op' + od - pp) - op) with (Zabs (op' - pp) - (op + od)).
  auto.
  rewrite (Zabs_non_eq (op' - pp)).
  rewrite (Zabs_non_eq (op' + od - pp)).
  omega. omega. omega.
  exists (-1). split; auto with zarith.
  replace (Zabs (op' + od - pp) - op) with (Zabs (op' -pp) - (op + -1)).
  auto.
  rewrite (Zabs_non_eq (op' - pp)).
  replace (op' + od - pp) with od by omega.
  omega. omega.
  exists (-od). split. rewrite (Zabs_Zopp). auto.
  replace (Zabs (op' + od - pp) - op) with (Zabs (op' - pp) - (op + -od)).
  auto.
  rewrite (Zabs_eq (op' - pp)).
  rewrite (Zabs_eq (op' + od - pp)).
  omega. omega. omega.
Qed.

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.
Proof.
  induction os.
  simpl. intros. omega.

  simpl. intros.
  destruct a as [[|] _ op'].
  set (x := Zmax0 (op' - bp) + 1).
  set (y := Zmax0 (op' - (bp + bd)) + 1).
  assert (Hxy: x = y \/ x = y + 1).
  unfold x, y. unfold Zmax0.
  destruct (Ztrichotomy op' bp) as [|[|]].
  rewrite (Zmax_left 0 (op' - bp)).
  rewrite (Zmax_left 0 (op' - (bp + bd))).
  auto. omega. omega.
  rewrite (Zmax_left 0 (op' - bp)).
  replace (op' - (bp + bd)) with (-bd) by omega.
  rewrite (Zmax_left 0 (-bd)). auto.
  omega. omega.
  rewrite (Zmax_right 0 (op' - bp)).
  rewrite (Zmax_right 0 (op' - (bp + bd))).
  omega. omega. omega.

  destruct Hxy as [Hxy|Hxy]; rewrite Hxy.
  destruct (IHos 0 (op + y) 0 od); try omega.
  simpl in H1, H2.
  replace (op + od + y) with (op + y + od) by omega.
  omega.

  assert (Hod: od = 0 \/ od = 1) by omega.
  destruct Hod as [Hod|Hod]; rewrite Hod in *.
  replace (op + 0 + y) with (op + y) by omega.
  replace (op + (y + 1)) with (op + y + 1) by omega.
  destruct (IHos 0 (op + y) 0 1); try omega.
  simpl in H1, H2.
  omega.

  replace (op + 1 + y) with (op + (y + 1)) by omega.
  omega.

  set (x := Zmax0 (op' - op) + 1).
  set (y := Zmax0 (op' - (op + od)) + 1).
  assert (Hxy: x = y \/ x = y + 1).
  unfold x, y. unfold Zmax0.
  destruct (Ztrichotomy op' op) as [|[|]].
  rewrite (Zmax_left 0 (op' - op)).
  rewrite (Zmax_left 0 (op' - (op + od))).
  auto. omega. omega.
  rewrite (Zmax_left 0 (op' - op)).
  replace (op' - (op + od)) with (-od) by omega.
  rewrite (Zmax_left 0 (-od)). auto.
  omega. omega.
  rewrite (Zmax_right 0 (op' - op)).
  rewrite (Zmax_right 0 (op' - (op + od))).
  omega. omega. omega.

  destruct Hxy as [Hxy|Hxy]; rewrite Hxy.
  destruct (IHos (bp + y) 0 bd 0); try omega.
  simpl in H1, H2.
  replace (bp + bd + y) with (bp + y + bd) by omega.
  omega.

  assert (Hod: bd = 0 \/ bd = 1) by omega.
  destruct Hod as [Hod|Hod]; rewrite Hod in *.
  replace (bp + 0 + y) with (bp + y) by omega.
  replace (bp + (y + 1)) with (bp + y + 1) by omega.
  destruct (IHos (bp + y) 0 1 0); try omega.
  simpl in H1, H2.
  omega.

  replace (bp + 1 + y) with (bp + (y + 1)) by omega.
  omega.
Qed.

Lemma min_movesRel_aux_1:
  forall (os: list OrderRel) (bp op: Z) (bd od: Z),
    -1 <= bd <= 1 -> -1 <= od <= 1 ->
      min_movesRel_aux bp op os <= min_movesRel_aux (bp+bd) (op+od) os + 1.
Proof.
  intros.
  assert (Hb: bd = -1 \/ 0 <= bd <= 1) by omega.
  assert (Ho: od = -1 \/ 0 <= od <= 1) by omega.
  destruct Hb; destruct Ho.
  destruct (min_movesRel_aux_1_1 os (bp + bd) (op + od) (-bd) (-od)); try omega.
  replace (bp + bd + -bd) with bp in * by omega.
  replace (op + od + -od) with op in * by omega.
  omega.
  destruct (min_movesRel_aux_1_1 os (bp + bd) op (-bd) 0); try omega.
  replace (bp + bd + -bd) with bp in * by omega.
  replace (op + 0) with op in * by omega.
  destruct (min_movesRel_aux_1_1 os (bp+bd) op 0 od); try omega.
  replace (bp + bd + 0) with (bp + bd) in * by omega.
  omega.
  destruct (min_movesRel_aux_1_1 os bp (op + od) 0 (-od)); try omega.
  replace (bp + 0) with bp in * by omega.
  replace (op + od + -od) with op in * by omega.
  destruct (min_movesRel_aux_1_1 os bp (op + od) bd 0); try omega.
  replace (op + od + 0) with (op + od) in * by omega.
  omega.
  destruct (min_movesRel_aux_1_1 os bp op bd od); try omega.
Qed.

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.
Proof.
  intros.
  assert (exists d, -1 <= d <= 1 /\
          min_trans bp op (bp'+bd) (op'+od) os = min_trans (bp+d) op bp' (op'+od) os).
  assert (bd = -1 \/ bd = 0 \/ bd = 1). omega.
  destruct H1 as [Hb|[Hb|Hb]].
  destruct (min_trans_1_0 os bp op bp' (op'+od) bd) as [bd'].
  rewrite Hb. auto.
  exists bd'. destruct H1. split; auto. destruct (Zabs_dec bd'); omega.
  exists 0. split. omega.
  f_equal; omega.
  destruct (min_trans_1_0 os bp op bp' (op'+od) bd) as [bd'].
  rewrite Hb. auto.
  exists bd'. destruct H1. split; auto. destruct (Zabs_dec bd'); omega.
  destruct H1 as [bd' []].
  rewrite H2.
  assert (exists d, -1 <= d <= 1 /\
          min_trans (bp+bd') op bp' (op'+od) os = min_trans (bp+bd') (op+d) bp' op' os).
  assert (od = -1 \/ od = 0 \/ od = 1). omega.
  destruct H3 as [Hb|[Hb|Hb]].
  destruct (min_trans_0_1 os (bp+bd') op bp' op' od) as [od'].
  rewrite Hb. auto.
  exists od'. destruct H3. split; auto. destruct (Zabs_dec od'); omega.
  exists 0. split. omega.
  f_equal; omega.
  destruct (min_trans_0_1 os (bp+bd') op bp' op' od) as [od'].
  rewrite Hb. auto.
  exists od'. destruct H3. split; auto. destruct (Zabs_dec od'); omega.
  destruct H3 as [od' []].
  rewrite H4.
  unfold min_trans.
  specialize (min_movesRel_aux_1 (translateRel_aux bp' op' os) (bp+bd') (op+od') (-bd') (-od')).
  replace (bp + bd' + -bd') with bp by omega.
  replace (op + od' + -od') with op by omega.
  intros. apply H5. omega. omega.
Qed.

Lemma corrent_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).
Proof.
  induction ms.
  unfold correct_moves. simpl.
  intros.
  injection H. intros.
  rewrite H0.
  unfold min_trans. simpl. omega.

  replace (Z_of_nat (length (a :: ms))) with (Z_of_nat (length ms) + 1).
  unfold correct_moves, play_moves. simpl.
  intros.
  set (st := play_one_move (state bp op (Some os)) a) in *.
  case_eq st.
  intros bp' op' os' Heq.
  destruct os' as [os'|].
  assert (Hcorrect: correct_moves bp' op' ms os').
  rewrite Heq in H.
  exact H.
  generalize (IHms bp' op' os' Hcorrect).
  intro Hms.
  assert (Hsimple: -1 <= bp - bp' <= 1 -> -1 <= op - op' <= 1 -> os = os' ->
          min_trans 0 0 bp op os <= Z_of_nat (length ms) + 1).
  intros.
  specialize (min_trans_le os 0 0 bp' op' (bp-bp') (op-op')).
  replace (bp' + (bp - bp')) with bp by omega.
  replace (op' + (op - op')) with op by omega.
  intros. rewrite H2 in *. omega.

  unfold play_one_move in st.
  unfold orders in st at 1.
  destruct os as [|o os].
  unfold min_trans. simpl. intros. omega.

  destruct a as [mb mo].
  Ltac simple_case st Heq Hsimple :=
    simpl in st; unfold st in Heq; injection Heq; intros;
    apply Hsimple; auto; omega.
  destruct mb; destruct mo;
    try simple_case st Heq Hsimple.

  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Orange op) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (op - op) with 0 by omega.
  change (1 + min_trans 1 0 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H1. replace bp with (bp'+1) by omega.
  destruct (min_trans_1_0 os' 1 0 bp' op' 1) as [bd [? Hbdeq]]. auto.
  rewrite Hbdeq.
  assert (min_trans (1+bd) 0 bp' op' os' <= min_trans 0 0 bp' op' os').
  destruct (Zabs_eq_case bd 1). auto.
  rewrite H4.
  unfold min_trans.
  set (os'' := translateRel_aux bp' op' os').
  destruct (min_movesRel_aux_1_1 os'' 1 0 1 0); try omega.
  destruct (min_movesRel_aux_1_1 os'' 0 0 1 0); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  rewrite H4.
  replace (1 + - (1)) with 0 by auto.
  auto with zarith.
  omega.
  unfold st in Heq. congruence.

  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Orange op) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (op - op) with 0 by omega.
  change (1 + min_trans 1 0 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H1. replace bp with (bp'-1) by omega.
  destruct (min_trans_1_0 os' 1 0 bp' op' (-1)) as [bd [? Hbdeq]]. auto.
  replace (bp' + -1) with (bp' - 1) in Hbdeq by auto.
  rewrite Hbdeq.
  assert (min_trans (1+bd) 0 bp' op' os' <= min_trans 0 0 bp' op' os').
  destruct (Zabs_eq_case bd 1). auto.
  rewrite H4.
  unfold min_trans.
  set (os'' := translateRel_aux bp' op' os').
  destruct (min_movesRel_aux_1_1 os'' 1 0 1 0); try omega.
  destruct (min_movesRel_aux_1_1 os'' 0 0 1 0); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  rewrite H4.
  replace (1 + - (1)) with 0 by auto.
  auto with zarith.
  omega.
  unfold st in Heq. congruence.

  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Blue bp) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (bp - bp) with 0 by omega.
  change (1 + min_trans 0 1 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H2. replace op with (op'+1) by omega.
  destruct (min_trans_0_1 os' 0 1 bp' op' 1) as [od [? Hodeq]]. auto.
  rewrite Hodeq.
  assert (min_trans 0 (1+od) bp' op' os' <= min_trans 0 0 bp' op' os').
  destruct (Zabs_eq_case od 1). auto.
  rewrite H4.
  unfold min_trans.
  set (os'' := translateRel_aux bp' op' os').
  destruct (min_movesRel_aux_1_1 os'' 0 1 0 1); try omega.
  destruct (min_movesRel_aux_1_1 os'' 0 0 0 1); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  rewrite H4.
  replace (1 + - (1)) with 0 by auto.
  auto with zarith.
  omega.
  unfold st in Heq. congruence.


  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Blue bp) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (bp - bp) with 0 by omega.
  change (1 + min_trans 0 1 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H2. replace op with (op'-1) by omega.
  destruct (min_trans_0_1 os' 0 1 bp' op' (-1)) as [od [? Hodeq]]. auto.
  replace (op' + -1) with (op' - 1) in Hodeq by auto.
  rewrite Hodeq.
  assert (min_trans 0 (1+od) bp' op' os' <= min_trans 0 0 bp' op' os').
  destruct (Zabs_eq_case od 1). auto.
  rewrite H4.
  unfold min_trans.
  set (os'' := translateRel_aux bp' op' os').
  destruct (min_movesRel_aux_1_1 os'' 0 1 0 1); try omega.
  destruct (min_movesRel_aux_1_1 os'' 0 0 0 1); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  rewrite H4.
  replace (1 + - (1)) with 0 by auto.
  auto with zarith.
  omega.
  unfold st in Heq. congruence.

  unfold st in Heq. congruence.


  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Blue bp) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (bp - bp) with 0 by omega.
  change (1 + min_trans 0 1 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H2. replace op with op' by omega.
  unfold min_trans in Hms |- *.
  set (os'' := translateRel_aux bp' op' os') in Hms |- *.
  destruct (min_movesRel_aux_1_1 os'' 0 0 0 1); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  unfold st in Heq. congruence.
  
  unfold orange_pos, blue_pos in st.
  destruct (Order_eq_dec (order Orange op) o).
  rewrite <- e.
  unfold min_trans. simpl.
  replace (op - op) with 0 by omega.
  change (1 + min_trans 1 0 bp op os <= Z_of_nat (length ms) + 1).
  injection Heq.
  intros.
  rewrite H0. rewrite H1. replace bp with bp' by omega.
  unfold min_trans in Hms |- *.
  set (os'' := translateRel_aux bp' op' os') in Hms |- *.
  destruct (min_movesRel_aux_1_1 os'' 0 0 1 0); try omega.
  replace (0 + 1) with 1 in * by auto.
  replace (0 + 0) with 0 in * by auto.
  omega.
  unfold st in Heq. congruence.

  rewrite Heq in H.
  apply False_ind.
  contradict H.
  clear IHms.
  induction ms.
  simpl. discriminate.
  simpl. unfold play_one_move at 2.
  unfold orders at 2. auto.

  replace (length (a :: ms)) with (S (length ms)) by auto.
  rewrite inj_S.
  auto with zarith.
Qed.

Fixpoint find_next_pos (r: Robo) (os: list Order) :=
match os with
| nil => 0
| order r' v::os' =>
  if Robo_eq_dec r r' then
    v
  else
    find_next_pos r os'
end.

Definition Zmax0_nat z :=
match z with
| Z0 => 0%nat
| Zpos p => nat_of_P p
| Zneg p => 0%nat
end.

Definition make_move (x x': Z) :=
match x ?= x' with
| Gt => (Left, x-1)
| Eq => (Stay, x)
| Lt => (Right,x+1)
end.

Record MMresult : Set := mmresult {
  mmr_moves: list Moves;
  mmr_bpos: Z;
  mmr_opos: Z
}.

Fixpoint make_moves_b (n: nat) (bp bp': Z) (op op': Z) :=
match n with
| O =>
   let (m, op'') := make_move op op' in
   mmresult (moves Push m::nil) bp' op''
| S n' =>
   let (mb, bp'') := make_move bp bp' in
   let (mo, op'') := make_move op op' in
   let mmr := make_moves_b n' bp'' bp' op'' op' in
   mmresult (moves mb mo::mmr_moves mmr)
            (mmr_bpos mmr) (mmr_opos mmr) 
end.

Fixpoint make_moves_o (n: nat) (bp bp': Z) (op op': Z) :=
match n with
| O =>
   let (m, bp'') := make_move bp bp' in
   mmresult (moves m Push::nil) bp'' op'
| S n' =>
   let (mb, bp'') := make_move bp bp' in
   let (mo, op'') := make_move op op' in
   let mmr := make_moves_o n' bp'' bp' op'' op' in
   mmresult (moves mb mo::mmr_moves mmr)
            (mmr_bpos mmr) (mmr_opos mmr) 
end.

Fixpoint make_min_moves (bp op: Z) (os: list Order) :=
match os with
| nil => nil
| order Blue bp'::os' =>
  let op' := find_next_pos Orange os' in
  let n := Zabs_nat (bp' - bp) in
  let mmr := make_moves_b n bp bp' op op' in
  mmr_moves mmr ++ make_min_moves (mmr_bpos mmr) (mmr_opos mmr) os'
| order Orange op'::os' =>
  let bp' := find_next_pos Orange os' in
  let n := (Zabs_nat (op' - op) + 1)%nat in
  let mmr := make_moves_o n bp bp' op op' in
  mmr_moves mmr ++ make_min_moves (mmr_bpos mmr) (mmr_opos mmr) os'
end.

Inductive Move' : Set := Left' | Stay' | Right'.

Definition do_move' m x :=
match m with
| Left'  => x + 1
| Stay'  => x
| Right' => x - 1
end.

Definition to_move m :=
match m with
| Left' => Left
| Stay' => Stay
| Right' => Right
end.

Inductive Correct_movei (bp op: Z) : list Order -> list Moves -> Prop :=
| cm_nil: Correct_movei bp op nil nil
| cm_MM mb mo os ms:
  Correct_movei (do_move' mb bp) (do_move' mo op) os ms ->
  Correct_movei bp op os (moves (to_move mb) (to_move mo)::ms)
| cm_MP mb os ms:
  Correct_movei (do_move' mb bp) op os ms ->
  Correct_movei bp op (order Orange op::os) (moves (to_move mb) Push::ms)
| cm_PM mo os ms:
  Correct_movei bp (do_move' mo op) os ms ->
  Correct_movei bp op (order Blue bp::os) (moves Push (to_move mo)::ms).

Lemma correct_movei_1:
  forall ms os bp op,
    Correct_movei bp op os ms -> correct_moves bp op ms os.
Proof.
  intros.
  induction H.
  cbv. auto.
  destruct mb; destruct mo.
  simpl. unfold correct_moves in *. simpl in *.
  unfold play_one_move.
  unfold orders at 2.
  destruct os. 

Lemma correct_moves_app_hd:
  forall (bp op: Z) (ms ms': list Moves) (o: Order) (os: list Order),
    let st  := play_moves ms (state bp op (Some (o::nil))) in
    let st' := play_moves ms' (state (blue_pos st) (orange_pos st) (Some os)) in
    orders st = Some nil /\ orders st' = Some nil -> correct_moves bp op (ms++ms') os.
Proof.
  assert (Hst: forall (ms: list Moves) (bp op: Z) (o: Order) (os: list Order),
            let st  := play_moves ms (state bp op (Some (o::nil))) in
            let st' := play_moves ms (state bp op (Some (o::os)))  in
            orders st = Some nil ->
              blue_pos st = blue_pos st' /\
              orange_pos st = orange_pos st' /\
              orders st' = Some os).
  induction ms.
  simpl. intros. congruence.
  intros. simpl in st, st'.
  destruct a as [mb mo].
  unfold play_one_move, orders, blue_pos, orange_pos.
  destruct mb; destruct mo.

  intros. unfold correct_moves, play_moves.
  rewrite fold_left_app.
  exact H.
Qed.

Lemma make_min_moves_correct:
  forall (os: list Order) (bp op: Z),
    correct_moves bp op (make_min_moves bp op os) os.
Proof.
(*
  assert (Habs: forall x y, x = y \/
          x = y + Z_of_nat (Zabs_nat (x - y)) \/ y = x + Z_of_nat (Zabs_nat (x - y))).
  intros.
  assert (0%nat = Zmax0_nat (x-y) \/ exists n, n = Zmax0_nat (x-y) /\ x - y = Z_of_nat n).
  destruct (x - y).
  auto. right. simpl. exists (nat_of_P p).
  auto using Zpos_eq_Z_of_nat_o_nat_of_P.
  left. auto.
  intuition. right. destruct H0. exists x0. auto with zarith.
 *)
  assert (Hmakemv: forall x y,
          make_move x y = (Left,  x-1) \/
          make_move x y = (Stay,  x) \/
          make_move x y = (Right, x+1)).
  intros. unfold make_move.
  destruct (x ?= y); auto.

  induction os.
  unfold correct_moves. simpl. auto.
  intros.
  simpl.
  destruct a as [[] pp].
  destruct (Hmax0 pp bp) as [Hz|n [Hn Hxy]].
  rewrite <- Hz.
  simpl.
  destruct (Hmakemv op (find_next_pos Orange os)).
  rewrite H.
  unfold mmr_moves, mmr_bpos, mmr_opos.