GCJ 2011 Qual-A さらにやり直し。今度こそ完璧な証明が書けたはずだ

GCJ2011Qual-A.v

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

Set Implicit Arguments.
Unset Strict Implicit.

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

Definition robo_inv (robo: Robo) :=
match robo with
| Blue => Orange
| Orange => Blue
end.

Inductive Move (robo: Robo) : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves : Move Blue -> Move Orange -> Moves
| pushmove (roboPush: Robo) : Move (robo_inv roboPush) -> Moves.

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

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

Record ZZ : Set := zz {
  pB : Z;
  pO : Z
}.

Definition zz_cor (p : ZZ) (r: Robo) :=
match r with
| Blue   => pB p
| Orange => pO p
end.

Coercion zz_cor : ZZ >-> Funclass.

Definition setzz (r: Robo) (v: Z) (p: ZZ) :=
match r with
| Blue   => zz v (pO p)
| Orange => zz (pB p) v
end.

Definition makezz (r: Robo) (u v: Z) :=
match r with
| Blue   => zz u v
| Orange => zz v u
end.

Definition padd (p q: ZZ) :=
  zz (pB p + pB q) (pO p + pO q).

Definition paddz (r: Robo) (p: ZZ) (x: Z) :=
  setzz r (p r + x) p.

Definition do_move (r: Robo) (m: Move r) (p: ZZ) :=
match m with
| Left  => paddz r p (-1)
| Stay  => p
| Right => paddz r p 1
end.

Definition do_moves (mb: Move Blue) (mo: Move Orange) (p: ZZ) :=
  do_move mb (do_move mo p).

Inductive Correct (pfrom: ZZ) : ZZ -> list Order -> list Moves -> Prop :=
| c_nil:
    Correct pfrom pfrom nil nil
| c_moves (mb : Move Blue) (mo : Move Orange) os ms pto:
  Correct (do_moves mb mo pfrom) pto os ms ->
    Correct pfrom pto os (moves mb mo::ms)
| c_pushmove (r : Robo) (mv: Move (robo_inv r)) os ms pto:
  Correct (do_move mv pfrom) pto os ms ->
    Correct pfrom pto (order r (pfrom r)::os) (pushmove mv::ms).

Lemma correct_app:
  forall (ws ws': list Moves) (os os': list Order) pfrom pvia pto,
    Correct pfrom pvia os ws ->
    Correct pvia  pto  os' ws' ->
    Correct pfrom pto (os++os') (ws++ws').
Proof.
  intros. revert pto H0.
  induction H; [simpl;auto| | ]; repeat rewrite <- app_comm_cons; constructor; auto.
Qed.

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

Fixpoint translateRel_aux (pfrom: ZZ) (os: list Order) : list OrderRel :=
match os with
| nil => nil
| order r pbutton::os' =>
    orderRel r (Zabs (pfrom r - pbutton)) :: translateRel_aux (setzz r pbutton pfrom) os'
end.

Definition Zmax0 := Zmax 0.

Definition cost_pu (pu: ZZ) (pbutton: Z) (r: Robo) :=
  Zmax0 (pbutton - pu r) + 1.
Definition update_pu (pu: ZZ) (pbutton: Z) (r: Robo) :=
  makezz r 0 (pu (robo_inv r) + cost_pu pu pbutton r).

Fixpoint min_movesRel_aux (pu: ZZ) (os: list OrderRel) :=
match os with
| nil => 0
| orderRel r pbutton::os' =>
    cost_pu pu pbutton r + min_movesRel_aux (update_pu pu pbutton r) os'
end.

Definition min_trans (pu pfrom: ZZ) (os: list Order) :=
  min_movesRel_aux pu (translateRel_aux pfrom os).

Lemma Zabs_or: forall x y, Zabs x = y -> x = y \/ x = -y.
Proof. intros. destruct (Zabs_dec x); omega. Qed.

Lemma Z_simpl_0: forall x y, x + y - y = x.
Proof. auto with zarith. Qed.

Lemma Z_simpl_1: forall x y, x - y + y = x.
Proof. intros. omega. Qed.

Lemma Z_simpl_3: forall x y, x + - y = x - y.
Proof. intros. auto. Qed.

Hint Rewrite
  Zplus_0_l Zplus_0_r Zminus_diag Zminus_plus Zplus_opp_r Zplus_opp_l
  Z_simpl_0
  Z_simpl_1
  Z_simpl_3
  : zs.

Ltac zsimpl := autorewrite with zs.

Lemma psimpl_1: forall r p x, (paddz r p x) r = p r + x.
Proof. destruct r; simpl; auto. Qed.

Lemma psimpl_2: forall r p x, (paddz r p x) (robo_inv r) = p (robo_inv r).
Proof. destruct r; simpl; auto. Qed.

Lemma psimpl_3: forall r p x y, setzz r x (paddz r p y) = setzz r x p.
Proof. destruct r; simpl; auto. Qed.

Lemma psimpl_4: forall p, zz (pB p) (pO p) = p.
Proof. destruct p; auto. Qed.

Lemma psimpl_5: forall r p (mv: Move r), do_move mv p (robo_inv r) = p (robo_inv r).
Proof. destruct r; destruct mv; destruct p; simpl; auto. Qed.

Lemma psimpl_6: forall r p (mv: Move r) x, setzz r x (do_move mv p) = setzz r x p.
Proof. destruct r; destruct mv; destruct p; simpl; auto. Qed.

Hint Rewrite
  psimpl_1
  psimpl_2
  psimpl_3
  psimpl_4
  psimpl_5
  psimpl_6
  : zz.

Definition Robo_eq_decinv: forall (r r': Robo), { r = r' } + { r = robo_inv r' }.
Proof. destruct r; destruct r'; auto. Defined.

Ltac psimpl := autorewrite with zz.

Ltac zsolve :=
  solve [ omega
        | rewrite Zabs_eq; zsolve
        | rewrite Zabs_non_eq; zsolve
        | rewrite Zmax_left; zsolve
        | rewrite Zmax_right; zsolve
        ].

Ltac zzsolve :=
  unfold update_pu, cost_pu, padd, paddz, Zmax0 in *; simpl in *;
  repeat match goal with
    | [ r: Robo |- _ ] => destruct r; simpl in *
    | [ |- zz _ _ = zz _ _ ] => f_equal
    | [ |- _ ] => progress autorewrite with zz zs in *
    | [ |- _ ] => zsolve
  end.

Lemma Zabs_lemma_1:
  forall x y z d, (d = -1 \/ d = 0 \/ d = 1) ->
    exists e, (e = -1 \/ e = 0 \/ e = 1) /\
      Zabs (x + d - y) - z = Zabs (x - y) - (z + e).
Proof.
  intros.
  destruct (Ztrichotomy x y) as [|[|]];
    destruct H as [|[|]];
      solve [ exists d; zsolve | exists (-d); zsolve ].
Qed.


Lemma min_trans_u1:
  forall (os: list Order) (pu pfrom: ZZ) (r: Robo) (mv: Move r),
  exists mv': Move r,
    min_trans pu (do_move mv pfrom) os = min_trans (do_move mv' pu) pfrom os.
Proof.
  induction os.
  intros; unfold min_trans; simpl; exists (Stay _); auto.

  intros.
  destruct a as [r' pp]; simpl.
  destruct (Robo_eq_decinv r' r); rewrite e; clear e r'.
  set (dfrom := do_move mv (zz 0 0) r).
  destruct (@Zabs_lemma_1 (pfrom r) pp (pu r) dfrom) as [du [Hdu Heq]]; auto.
    destruct mv; unfold dfrom; zzsolve.
  replace (pfrom r + dfrom) with (do_move mv pfrom r) in Heq.
    2:unfold do_move, dfrom; destruct mv; zzsolve.
  destruct Hdu as [Hdu|[Hdu|Hdu]];
    [ exists (Left _) | exists (Stay _) | exists (Right _) ];
    unfold min_trans; simpl; unfold update_pu, cost_pu;
    psimpl; rewrite Heq; rewrite Hdu; zsimpl; reflexivity.

  unfold min_trans. simpl.
  match goal with
  | [ |- context[min_movesRel_aux ?X ?Y] ] =>
    destruct (IHos X (setzz (robo_inv r) pp pfrom) r mv) as [mv' Heq]; auto
  end.
  exists mv'.
  f_equal. destruct mv; destruct mv'; unfold do_move; zzsolve.
  unfold min_trans in Heq; destruct mv; destruct mv'; zzsolve; rewrite Heq; f_equal; zzsolve.
Qed.

Lemma min_movesRel_aux_1_1:
  forall (os: list OrderRel) (pu: ZZ) (pd: ZZ),
    (forall r, 0 <= pd r <= 1) ->
      min_movesRel_aux (padd pu pd) os <=
        min_movesRel_aux pu os <=
          min_movesRel_aux (padd pu pd) os + 1.
Proof.
  induction os; intros; simpl; try omega.

  generalize (H Blue); generalize (H Orange); simpl; intros.
  destruct a as [r pp].
  unfold update_pu, cost_pu.
  set (x := Zmax0 (pp - pu r) + 1).
  set (y := Zmax0 (pp - padd pu pd r) + 1).
  assert (Hxy: x = y \/ x = y + 1).
  destruct (Ztrichotomy pp (pu r)) as [|[|]];
    unfold x, y; zzsolve.

  destruct Hxy as [Hxy|Hxy]; rewrite Hxy; clear x Hxy.
  destruct (IHos (makezz r 0 (pu (robo_inv r) + y)) (setzz r 0 pd)).
  intros; zzsolve.
  replace (makezz r 0 (padd pu pd (robo_inv r) + y))
     with (padd (makezz r 0 (pu (robo_inv r) + y)) (setzz r 0 pd));
  zzsolve.

  set (od := pd (robo_inv r)).
  assert (Hod: od = 0 \/ od = 1).
    unfold od; zzsolve.
  destruct Hod as [Hod|Hod]; unfold od in Hod; clear od.
  destruct (IHos (makezz r 0 (pu (robo_inv r) + y)) (makezz r 0 1)).
  intros; zzsolve.
  replace (padd pu pd (robo_inv r) + y)
     with (pu (robo_inv r) + y);
  replace (makezz r 0 (pu (robo_inv r) + (y + 1)))
     with (padd (makezz r 0 (pu (robo_inv r) + y)) (makezz r 0 1));
    zzsolve.

  replace (pu (robo_inv r) + (y + 1))
     with (padd pu pd (robo_inv r) + y); zzsolve.
Qed.

Lemma min_movesRel_aux_1:
  forall (os: list OrderRel) (pu: ZZ) (mb: Move Blue) (mo: Move Orange),
    min_movesRel_aux pu os <= min_movesRel_aux (do_moves mb mo pu) os + 1.
Proof.
  intros.
  set (bd := do_moves mb mo (zz 0 0) Blue).
  set (od := do_moves mb mo (zz 0 0) Orange).
  
  assert (Hb: bd = -1 \/ 0 <= bd <= 1). 
    destruct mb; destruct mo; unfold bd; simpl; auto with zarith.
  assert (Ho: od = -1 \/ 0 <= od <= 1). 
    destruct mb; destruct mo; unfold od; simpl; auto with zarith.
  replace (do_moves mb mo pu) with (padd pu (zz bd od)).
    2:destruct mb; destruct mo; unfold bd, od; zzsolve; auto.
  destruct Hb; destruct Ho.
  destruct (@min_movesRel_aux_1_1 os (padd pu (zz bd od)) (zz (-bd) (-od)));
    intros; zzsolve.
  destruct (@min_movesRel_aux_1_1 os (padd pu (zz bd 0)) (zz (-bd) 0));
  destruct (@min_movesRel_aux_1_1 os (padd pu (zz bd 0)) (zz 0 od));
    intros; zzsolve.
  destruct (@min_movesRel_aux_1_1 os (padd pu (zz 0 od)) (zz 0 (-od)));
  destruct (@min_movesRel_aux_1_1 os (padd pu (zz 0 od)) (zz bd 0));
    intros; zzsolve.
  destruct (@min_movesRel_aux_1_1 os pu (zz bd od));
    intros; zzsolve.
Qed.

Lemma min_trans_le:
  forall (os: list Order) (pu pfrom: ZZ) (mb: Move Blue) (mo: Move Orange),
    min_trans pu pfrom os <= min_trans pu (do_moves mb mo pfrom) os + 1.
Proof.
  intros.
  pose (Hw := min_trans_u1 os).
  unfold do_moves.
  destruct (Hw pu (do_move mo pfrom) Blue mb) as [db' Hdbeq]; auto.
  rewrite Hdbeq.

  destruct (Hw (do_move db' pu) pfrom Orange mo) as [do' Hdoeq]; auto.
  rewrite Hdoeq.
  replace (do_move do' (do_move db' pu)) with (do_moves db' do' pu).
    2:destruct db'; destruct do'; destruct pu; simpl; zzsolve.
  apply min_movesRel_aux_1.
Qed.

Lemma corrent_moves_min:
  forall (ms: list Moves) (pfrom pto: ZZ) (os: list Order),
    Correct pfrom pto os ms ->
    min_trans (zz 0 0) pfrom os <= Z_of_nat (length ms).
Proof.
  intros.
  induction H. unfold min_trans. simpl. omega.

  simpl. rewrite Zpos_P_of_succ_nat.
  specialize (@min_trans_le os (zz 0 0) pfrom mb mo).
  intros.
  omega.

  unfold min_trans.
  simpl. rewrite Zpos_P_of_succ_nat. unfold update_pu, cost_pu. zsimpl. simpl.
  rewrite Zplus_comm.
  
  destruct (@min_trans_u1 os (zz 0 0) pfrom (robo_inv r) mv) as [mv' Hdeq].
  rewrite Hdeq in *.
  replace (setzz r (pfrom r) pfrom) with pfrom by (destruct pfrom; zzsolve).

  assert (Hmon: forall x, min_trans (makezz r 0 (x+1)) pfrom os <= min_trans (makezz r 0 x) pfrom os).
  intros.
  unfold min_trans.
  destruct (@min_movesRel_aux_1_1 (translateRel_aux pfrom os) (makezz r 0 x) (makezz r 0 1)).
  intros; zzsolve. zzsolve.
  generalize (Hmon (-1)); generalize (Hmon 0); intros.
  autorewrite with zs in *.
  unfold min_trans in *.
  destruct mv'; zzsolve.
Qed.

Definition min_trans_find_fun (os: list Order) (pu pfrom: ZZ) (r: Robo) (pbutton: Z) :=
match Z_lt_le_dec pbutton (pfrom r) with
| left _ => Left r
| right _ =>
    match Z_eq_dec pbutton (pfrom r) with
    | left _ => Stay r
    | right _ => Right r
    end
end.

Lemma min_trans_find:
  forall (os: list Order) (pu pfrom: ZZ) (r: Robo) (pbutton: Z),
    pu r >= 0 ->
    let mv := min_trans_find_fun os pu pfrom r pbutton in
      min_trans pu (do_move mv pfrom) (order r pbutton::os) =
      min_trans (paddz r pu 1) pfrom (order r pbutton::os).
Proof.
  intros.
  assert (Hdeq: cost_pu (paddz r pu 1) (Zabs (pfrom r - pbutton)) r =
          cost_pu pu (Zabs (do_move mv pfrom r - pbutton)) r).
  unfold mv, min_trans_find_fun.
  destruct (Z_lt_le_dec pbutton (pfrom r));
    [ | destruct (Z_eq_dec pbutton (pfrom r)) as [Heq|] ]; unfold cost_pu, do_move.
  f_equal; f_equal; zzsolve.
  rewrite Heq; zzsolve.
  f_equal; f_equal; zzsolve.

  unfold min_trans. simpl.
  unfold update_pu.
  rewrite Hdeq. psimpl. auto.
Qed.

Fixpoint min_trans_find_funr (os: list Order) (pu pfrom: ZZ) (r: Robo) :=
match os with
| nil => Stay r
| order r' pbutton::os' =>
  if Robo_eq_decinv r' r then
    min_trans_find_fun os' pu pfrom r pbutton
  else
    min_trans_find_funr os'
      (update_pu pu (Zabs (pfrom r' - pbutton)) r')
      (setzz r' pbutton pfrom)
      r
end.

Lemma min_trans_find2:
  forall (os: list Order) (pu pfrom: ZZ) (r: Robo),
    pu r >= 0 ->
    let mv := min_trans_find_funr os pu pfrom r in
      min_trans pu (do_move mv pfrom) os =
      min_trans (paddz r pu 1) pfrom os.
Proof.
  induction os.
  intros; unfold min_trans; simpl; omega.
  intros.
  destruct a as [r' pbutton'].
  unfold min_trans_find_funr in mv.
  destruct (Robo_eq_decinv r' r).
  rewrite e in *.
  apply min_trans_find; auto.

  fold min_trans_find_funr in mv.
  lapply (IHos (update_pu pu (Zabs (pfrom r' - pbutton')) r') (setzz r' pbutton' pfrom) r).
    2:specialize (Zle_max_l 0 (Zabs (pfrom r' - pbutton') - pu r')); zzsolve.

  intros.
  unfold mv in *. clear mv.
  rewrite e in *.

  revert H0.
  generalize (min_trans_find_funr os
               (update_pu pu (Zabs (pfrom (robo_inv r) -pbutton')) (robo_inv r))
               (setzz (robo_inv r) pbutton' pfrom)).
  intros mv Heq.
  unfold min_trans in *; simpl; f_equal;
    unfold do_move in *; destruct mv; zzsolve;
    rewrite Heq; f_equal; zzsolve.
Qed.


Definition min_trans_find_fun2 (os: list Order) (pfrom: ZZ) :=
  let mo := min_trans_find_funr os (zz 1 0) pfrom Orange in
  let mb := min_trans_find_funr os (zz 0 0) (do_move mo pfrom) Blue in
    (mb, mo).


Lemma min_trans_find3:
  forall (os: list Order) (pfrom: ZZ),
    let (mb, mo) := min_trans_find_fun2 os pfrom in
      min_trans (zz 1 1) pfrom os = min_trans (zz 0 0) (do_moves mb mo pfrom) os.
Proof.
  unfold min_trans_find_fun2.
  intros.
  lapply (@min_trans_find2 os (zz 1 0) pfrom Orange).
    2:zzsolve.
  set (mo := min_trans_find_funr os (zz 1 0) pfrom Orange).
  intros.
  lapply (@min_trans_find2 os (zz 0 0) (do_move mo pfrom) Blue).
    2:zzsolve.
  intros.
  simpl in *.
  unfold do_moves.
  congruence.
Qed.

Lemma min_trans_u11:
  forall (os: list Order) (pfrom: ZZ) (r: Robo) (pbutton: Z),
    let os' := order r pbutton::os in
      pfrom r <> pbutton ->
      min_trans (zz 1 1) pfrom os' + 1 = min_trans (zz 0 0) pfrom os'.
Proof.
  intros.
  unfold os'.
  unfold min_trans.
  simpl.
  unfold update_pu.
  set (pb := Zabs (pfrom r - pbutton)).
  assert (pb > 0).
    destruct (Ztrichotomy (pfrom r) pbutton); unfold pb; zsolve.
  replace (cost_pu (zz 1 1) pb r) with (cost_pu (zz 0 0 ) pb r - 1).
  ring_simplify.
  f_equal. f_equal.
  destruct r; unfold cost_pu; unfold makezz; f_equal;
  rewrite Zplus_comm; zzsolve.
  unfold cost_pu. zzsolve.
Qed.

Lemma min_trans_find4:
  forall (os: list Order) (pfrom: ZZ) (r: Robo) (pbutton: Z),
    let os' := order r pbutton::os in
      pfrom r <> pbutton ->
      let (mb, mo) := min_trans_find_fun2 os' pfrom in
        min_trans (zz 0 0) (do_moves mb mo pfrom) os' + 1 = min_trans (zz 0 0) pfrom os'.
Proof.
  intros.
  specialize (min_trans_find3 os' pfrom).
  intro Heq. unfold min_trans_find_fun2 in *.
  rewrite <- Heq.
  apply min_trans_u11; auto.
Qed.

Lemma min_trans_u10:
  forall (os: list Order) (pfrom: ZZ) (r: Robo) (pbutton: Z),
    let os' := order r pbutton::os in
      pfrom r = pbutton ->
      min_trans (makezz r 0 1) pfrom os + 1 = min_trans (zz 0 0) pfrom os'.
Proof.
  intros.
  unfold os'.
  unfold min_trans.
  simpl.
  rewrite H.
  rewrite Zplus_comm.
  f_equal.
  zzsolve.
  f_equal.
  zzsolve.
  f_equal.
  rewrite <- H.
  zzsolve; auto.
Qed.

Lemma min_trans_find5:
  forall (os: list Order) (pfrom: ZZ) (r: Robo) (pbutton: Z),
    let os' := order r pbutton::os in
      pfrom r = pbutton ->
      let mv := min_trans_find_funr os (zz 0 0) pfrom (robo_inv r) in
        min_trans (zz 0 0) (do_move mv pfrom) os + 1 = min_trans (zz 0 0) pfrom os'.
Proof.
  intros.
  lapply (@min_trans_find2 os (zz 0 0) pfrom (robo_inv r)).
    2:zzsolve.
  intros Heq. hnf in Heq.
  unfold mv.
  rewrite Heq.
  replace (paddz (robo_inv r) (zz 0 0) 1) with (makezz r 0 1) by zzsolve.
  apply min_trans_u10.
  auto.
Qed.

Definition clear_head_order (os: list Order) (mv: Moves) :=
match mv with
| moves _ _ => os
| pushmove _ _ => tail os
end.

Definition correct_pushmove (os: list Order) (pfrom: ZZ) (mv: Moves) :=
match mv with
| moves _ _ => True
| pushmove r mv =>
    match os with
    | nil => False
    | order r' pbutton::os => r = r' /\ pfrom r = pbutton
    end
end.

Definition do_moves' (mv: Moves) (pfrom: ZZ) :=
match mv with
| moves mb mo => do_moves mb mo pfrom
| pushmove r mv => do_move mv pfrom
end.

Definition min_trans_find_f (os: list Order) (pfrom: ZZ) :=
match os with
| nil => moves (Stay _) (Stay _)
| order r pbutton::os' =>
    if Z_eq_dec (pfrom r) pbutton then
      let mv := min_trans_find_funr os' (zz 0 0) pfrom (robo_inv r) in
        pushmove mv
    else
      let (mb, mo) := min_trans_find_fun2 os pfrom in
        moves mb mo
end.

Lemma min_trans_find6:
  forall (os: list Order) (pfrom: ZZ),
     os <> nil ->
     let mv := min_trans_find_f os pfrom in
       correct_pushmove os pfrom mv /\
       min_trans (zz 0 0) (do_moves' mv pfrom) (clear_head_order os mv) + 1 =
       min_trans (zz 0 0) pfrom os.
Proof.
  intros.
  destruct os as [|[r pbutton]].
  congruence.
  unfold min_trans_find_f in *.
  unfold clear_head_order, mv.
  destruct (Z_eq_dec (pfrom r) pbutton).
  split.
    simpl; auto.
  apply min_trans_find5; auto.

  split.
    simpl; auto.
  simpl; apply min_trans_find4; auto.
Qed.

Lemma min_trans_noneg:
  forall (os: list Order) (pu pfrom: ZZ),
     0 <= min_trans pu pfrom os.
Proof.
  induction os as [|[r pb]].
  intros. unfold min_trans. simpl. omega.
  intros. unfold min_trans in *. simpl.
  apply Zplus_le_0_compat; auto.
  unfold cost_pu.
  unfold Zmax0.
  apply Zplus_le_0_compat; auto with zarith.
  apply Zle_max_l.
Qed.

Lemma min_trans_zero:
  forall (os: list Order) (pu pfrom: ZZ),
    os = nil <-> min_trans pu pfrom os = 0.
Proof.
  intros.
  destruct os as [|[r pb]].
  unfold min_trans. simpl. split; auto.
  split. congruence.
  intros. contradict H.
  assert (0 < min_trans pu pfrom (order r pb :: os)).
  unfold min_trans. simpl.
  replace 0 with (0 + 0) by auto.
  apply Zplus_lt_le_compat.
  unfold cost_pu.
  replace 0 with (0 + 0) by auto.
  apply Zplus_le_lt_compat.
  unfold Zmax0.
  apply Zle_max_l.
  omega.
  apply min_trans_noneg.
  omega.
Qed.

Fixpoint min_trans_find_list_r (n: nat) (os: list Order) (pfrom: ZZ) :=
match n with
| O => nil
| S n' =>
  let mv := min_trans_find_f os pfrom in
    mv :: min_trans_find_list_r n' (clear_head_order os mv) (do_moves' mv pfrom)
end.

Lemma min_trans_ex_aux:
  forall (n: nat) (os: list Order) (pfrom: ZZ),
    min_trans (zz 0 0) pfrom os = Z_of_nat n ->
    let ws := min_trans_find_list_r n os pfrom in
      exists pend, Correct pfrom pend os ws /\ n = length ws.
Proof.
  induction n.
  intros.
  exists pfrom.
  destruct (min_trans_zero os (zz 0 0) pfrom).
  unfold ws. simpl.
  rewrite H1. split. constructor. auto. auto.

  intros.
  destruct os as [|[r pb]].
  intros.
  exfalso. contradict H. unfold min_trans. simpl. rewrite Zpos_P_of_succ_nat. omega.
  
  hnf in ws.
  destruct (@min_trans_find6 (order r pb::os) pfrom) as [Hc Heq].
    discriminate.

  set (mv := min_trans_find_f (order r pb :: os) pfrom) in *.
  destruct (IHn (clear_head_order (order r pb :: os) mv) (do_moves' mv pfrom)) as [pend [Hcr Hlen]].
  rewrite inj_S in H. omega.
  exists pend.
  split.
  destruct mv as [mb mo | r' m]; simpl in Hc, Hcr.
  constructor. auto.
  destruct Hc as [Hceq1 Hceq2].
  unfold ws.
  rewrite <- Hceq2 in *. rewrite <- Hceq1 in *.
  constructor. auto.
  unfold ws. simpl. congruence.
Qed.

Definition min_trans_find_list (os: list Order) (pfrom: ZZ) :=
  min_trans_find_list_r (Zabs_nat (min_trans (zz 0 0) pfrom os)) os pfrom.

Lemma min_trans_ex:
  forall (os: list Order) (pfrom: ZZ),
    let ws := min_trans_find_list os pfrom in
      exists pend, Correct pfrom pend os ws /\
      min_trans (zz 0 0) pfrom os = Z_of_nat (length ws).
Proof.
  intros.
  set (n := min_trans (zz 0 0) pfrom os).
  assert (n = Z_of_nat (Zabs_nat n)).
  unfold n.
  rewrite inj_Zabs_nat.
  rewrite Zabs_eq; auto.
  apply min_trans_noneg.
  destruct (@min_trans_ex_aux (Zabs_nat n) os pfrom) as [pend []].
  unfold n in *. auto.
  exists pend;
  split; auto.
  unfold n in *.
  unfold ws. 
  unfold min_trans_find_list in *.
  congruence. 
Qed.

Definition minimum_moves (os: list Order) : list Moves :=
  min_trans_find_list os (zz 1 1).

Definition correct_moves (os: list Order) (ws: list Moves) :=
  exists pend, Correct (zz 1 1) pend os ws.

Theorem minimum_moves_is_correct:
  forall (os: list Order),
    let ws := minimum_moves os in
      correct_moves os ws.
Proof.
  intros.
  unfold ws, minimum_moves, correct_moves.
  destruct (min_trans_ex os (zz 1 1)) as [pend []].
  exists pend; auto.
Qed.

Theorem minimum_moves_is_minimum:
  forall (os: list Order),
    let ws := minimum_moves os in
      forall ws', correct_moves os ws' ->
        (length ws <= length ws')%nat.
Proof.
  intros.
  unfold ws, minimum_moves, correct_moves.
  destruct (min_trans_ex os (zz 1 1)) as [pend []].
  apply inj_le_rev.
  rewrite <- H1.
  destruct H as [pend'].
  apply corrent_moves_min with pend'.
  auto.
Qed.

Example sample_nil : list Order :=
  nil.

Example sample_1 :=
  order Orange 4::
  nil.

Example sample_2 :=
  order Orange 2::
  order Blue 1::
  order Blue 2::
  order Orange 4::
  nil.

Eval vm_compute in (min_trans (zz 0 0) (zz 1 1) sample_nil).
Eval vm_compute in (min_trans (zz 0 0) (zz 1 1) sample_1).
Eval vm_compute in (min_trans (zz 0 0) (zz 1 1) sample_2).

Eval vm_compute in (minimum_moves  sample_1).
Eval vm_compute in (minimum_moves  sample_2).

Extraction Language Ocaml.
Extract Inductive list => "list" [ "[]" "(::)" ].

Extraction "A.ml" minimum_moves sample_1.