GCJ 2011 Qual-A をssreflectで書いてみた。なんかOpaqueなデータが多くて計算できないし抽出もできなさげになった。ssreflectの雰囲気を見る用

GCJ2011Qual-Assr.v

Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import choice fintype tuple finfun ssralg.
Require Import ssrz smallord.
Require Import ZArith.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

Inductive Robo : Set := Blue | Orange.
Inductive Order : Set := order of Robo & Z.

Definition robo_inv (r : Robo) :=
  if r is Blue then Orange else Blue.

Notation "! r" := (robo_inv r) (at level 35, right associativity).

Inductive Move (robo : Robo) : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves of Move Blue & Move Orange
| pushmove (roboPush : Robo) of Move (! roboPush).

Module FinTypes.

Definition ord_of_Robo (r : Robo) : Ord8 :=
  if r is Blue then a0 else a1.

Definition Robo_of_ord (n : Ord8) :=
  if n is a0 then Blue else Orange.

Lemma Robo_pickleK : cancel ord_of_Robo Robo_of_ord.
Proof. by case. Qed.

Variable r: Robo.

Definition ord_of_Move (m : Move r) : Ord8 :=
  match m with
  | Left  => a0
  | Stay  => a1
  | Right => a2
  end.

Definition Move_of_ord (n : Ord8) : Move r :=
  match n with
  | a0 => Left  _
  | a1 => Stay  _
  | a2 => Right _
  | _  => Stay  _
  end.

Lemma Move_pickleK : cancel ord_of_Move Move_of_ord.
Proof. by case. Qed.

Module Exports.

Definition Robo_eqMixin := CanEqMixin Robo_pickleK.
Canonical Structure Robo_eqType := Eval hnf in EqType Robo Robo_eqMixin.
Definition Robo_choiceMixin := CanChoiceMixin Robo_pickleK.
Canonical Structure Robo_choiceType := Eval hnf in ChoiceType Robo Robo_choiceMixin.
Definition Robo_countMixin := CanCountMixin Robo_pickleK.
Canonical Structure Robo_countType := Eval hnf in CountType Robo Robo_countMixin.
Definition Robo_finMixin := CanFinMixin Robo_pickleK.
Canonical Structure Robo_finType := Eval hnf in FinType Robo Robo_finMixin.

Definition Move_eqMixin := CanEqMixin Move_pickleK.
Canonical Structure Move_eqType := Eval hnf in EqType (Move r) Move_eqMixin.
Definition Move_choiceMixin := CanChoiceMixin Move_pickleK.
Canonical Structure Move_choiceType := Eval hnf in ChoiceType (Move r) Move_choiceMixin.
Definition Move_countMixin := CanCountMixin Move_pickleK.
Canonical Structure Move_countType := Eval hnf in CountType (Move r) Move_countMixin.
Definition Move_finMixin := CanFinMixin Move_pickleK.
Canonical Structure Move_finType := Eval hnf in FinType (Move r) Move_finMixin.

End Exports.
End FinTypes.

Export FinTypes.Exports.

Print Canonical Projections.

Import GRing.Theory.

Open Scope Z_scope.
Open Scope ring_scope.
Bind Scope ring_scope with Z.

Definition Pos := {ffun Robo -> Z}.

Definition posm (b o : Z) : Pos :=
  [ffun r => if r is Blue then b else o].

Definition posr (r : Robo) (p p' : Z) : Pos :=
  [ffun r' => if r == r' is true then p else p'].

Definition posr0 (r : Robo) (p : Z) : Pos := posr r p 0.

Definition move (r : Robo) (m : Move r) : Pos :=
  posr0 r (match m with
             | Left  => -1
             | Stay  =>  0
             | Right =>  1
           end).

Definition Move_of_disp (r : Robo) (dis : Z) : Move r :=
  if dis == -1 is true then Left _ else
    if dis == 1 is true then Right _ else Stay _.

Inductive Correct (pfrom: Pos) : Pos -> seq Order -> seq Moves -> Prop :=
| c_nil:
    Correct pfrom pfrom nil nil
| c_moves (mb : Move Blue) (mo : Move Orange) os ms pto:
  Correct (pfrom + move mb + move mo) pto os ms ->
    Correct pfrom pto os (moves mb mo::ms)
| c_pushmove (r : Robo) (mv: Move (! r)) os ms pto:
  Correct (pfrom + move mv) pto os ms ->
    Correct pfrom pto (order r (pfrom r)::os) (pushmove mv::ms).

Lemma ecomp: forall (T : Type) (x y z w : T), x = y -> x = z -> y = w -> z = w.
Proof. by move=> T x y z w exy <- <-. Qed.

Lemma ReqriF : forall (r : Robo), r == !r = false.
Proof. by case. Qed.

Lemma ReqirF : forall (r : Robo), !r == r = false.
Proof. by case. Qed.

Lemma RinvK : involutive robo_inv.
Proof. by case. Qed.

Definition possimpl := (ffunE, RinvK, ReqirF, ReqriF, eqxx).
Definition rsimpl := (addr0, add0r, addNr, addrN, addKr, addNKr, addrK, addrNK).
Definition rpossimpl := (possimpl, rsimpl).

Lemma PeqP : forall (p q : Pos),
  reflect (p = q) ((p Blue == q Blue) && (p Orange == q Orange)).
Proof.
  move=> p q; apply introP.
    by case/andP; move/eqP => e; move/eqP => f; apply/ffunP; case.
  by move=> h eq; rewrite eq !eq_refl in h.
Qed.

Lemma PeqPr : forall (r : Robo) (p q : Pos),
  reflect (p = q) ((p r == q r) && (p (!r) == q (!r))).
Proof.
  case; first by apply PeqP.
  by move=> *; rewrite andbC; apply PeqP.
Qed.
  
Ltac poscrush r := apply/(PeqPr r); rewrite ?rpossimpl.

Lemma correct_app:
  forall (ws ws': seq Moves) (os os': seq Order) pfrom pvia pto,
    Correct pfrom pvia os ws ->
    Correct pvia  pto  os' ws' ->
    Correct pfrom pto (os++os') (ws++ws').
Proof.
  move=> ws ws' os os' pfrom pvia pto H.
  elim: {os pfrom pvia}ws / H pto => //=; constructor; auto.
Qed.

Lemma dispK : forall r d, d \in [:: -1; 0; 1] -> move (Move_of_disp r d) = posr0 r d.
Proof.
  move=> r d.
  rewrite mem_seq3.
  by case: r; case/or3P; move/eqP => ->.
Qed.

Arguments Scope Zmax [ring_scope ring_scope].
Arguments Scope Zabs [ring_scope ring_scope].

Definition Zmax0 := Zmax 0.

Definition distance (pfrom : Pos) (pbutton : Z) (r : Robo) : Z :=
  Zabs (pbutton - pfrom r).

Definition move_cost (pu: Pos) (dist: Z) (r: Robo) : Z :=
  Zmax0 (dist - pu r) + 1.

Definition update_pu (pu : Pos) (cost: Z) (r: Robo) : Pos :=
  posr r 0 (pu (! r) + cost).

Fixpoint min_moves_aux (pu pfrom : Pos) (os : seq Order) : Z :=
  match os with
    | nil => 0
    | order r pbutton::os' =>
      let dist := distance pfrom pbutton r in
      let cost := move_cost pu dist r in
      let pu' := update_pu pu cost r in
      let pfrom' := posr r pbutton (pfrom (! r)) in
        min_moves_aux pu' pfrom' os' + cost
  end.

Definition Robo_eq_decinv: forall (r r': Robo), { r = r' } + { r = !r' }.
Proof.  by case; case; auto. Defined.

(*
Ltac zsolve :=
  try rewrite !zformula;
    let rec f :=
      solve [ move=> * ; omega
        | rewrite Zabs_eq; f
        | rewrite Zabs_non_eq; f
        | rewrite Zmax_left; f
        | rewrite Zmax_right; f
      ]
      in
      f.
*)

Lemma Zabs_lemma_1:
  forall (x y z d : Z), d \in [:: -1; 0; 1] ->
    exists2 e : Z, e \in [:: -1; 0; 1] &
      Zabs (x - (y + d)) - z = Zabs (x - y) - (z + e).
Proof.
  move=> x y z d; rewrite mem_seq3.
  have axy:= Zabs_spec (x - y).
  have axyd:= Zabs_spec (x - (y + d)).
  Ltac s de xy := by [ rewrite de | move: de xy; zomega ].
  case/or3P; case/eqP => de; case (Ztrichotomy x y) => [|[|]] xy;
    solve [ exists d; s de xy | exists (-d); s de xy].
Qed.

Lemma min_moves_aux_1 :
  forall (os: seq Order) (pu pfrom: Pos) (r: Robo) (mv: Move r),
  exists mv': Move r,
    min_moves_aux pu (pfrom + move mv) os = min_moves_aux (pu + move mv') pfrom os.
Proof.
  elim; first by move=> *; exists (Stay _).
  case=> r' pp os IHos pu pfrom r mv /=.
  case (Robo_eq_decinv r' r) => -> {r'}.
    set disp := move _.
    case (@Zabs_lemma_1 pp (pfrom r) (pu r) (disp r)).
      by rewrite ffunE; case mv; case r.
    move=> v [vi ve].
    exists (Move_of_disp r v).
    set c0 := move_cost _ _ _.
    rewrite -(_ : c0 = move_cost _ _ _); first last.
      by rewrite /c0 /distance /move_cost ffunE ve dispK ?possimpl.
    congr (min_moves_aux _ _ _ + _).
      by poscrush r.
    by rewrite ?rpossimpl.
  set pu' := update_pu _ _ _.
  set pfrom' := posr _ _ (pfrom _).
  move: (IHos pu' pfrom' r mv) => [mv' mve].
  exists mv'.
  move: mve.
  rewrite /pu' /pfrom'.
  set c0 := move_cost _ _ _.
  rewrite -(_ : c0 = move_cost _ _ _); last first.
    by congr (Zmax0 _ + 1); rewrite /distance ?rpossimpl.
  move=> mve; congr +%R.
  by apply (ecomp mve); congr min_moves_aux;
    poscrush r; rewrite // addrAC eqxx.
Qed.

Lemma min_moves_aux_1_1:
  forall (os: seq Order) (pu pfrom pd : Pos),
    (forall r : Robo, 0 <= pd r <= 1) ->
      min_moves_aux (pu + pd) pfrom os <=
        min_moves_aux pu pfrom os <=
          min_moves_aux (pu + pd) pfrom os + 1.
Proof.
  elim; first by [].
  case=> r pp os IHos pu pfrom pd Hpd /=.
  move: (distance _ _ _) => d.
  set x := move_cost _ _ _.
  set y := move_cost _ _ _.
  have: x = y \/ x = y - 1.
    rewrite /x /y /move_cost /Zmax0 ffunE.
    move: (Hpd r).
    move: (pu r) (pd r) => z w. 
    move: (Zmax_spec 0 (d - z)) (Zmax_spec 0 (d - (z + w))).
    by zomega.
  case=> -> {x}.
    set pu' := update_pu pu _ _.
    set pfrom' := posr _ _ _.
    pose pd' := posr r 0 (pd (!r)).
    rewrite (_ : update_pu _ _ _ = pu' + pd'); last first.
      rewrite /pu' /pd' /update_pu.
      by poscrush r; rewrite addrAC !eqxx.
    lapply (IHos pu' pfrom' pd'); first by zomega.
    by rewrite /pd'; case; case r; rewrite ffunE /=.
  pose rd := pd (! r).
  have: rd = 1 \/ rd = 0.
    by rewrite /rd; move: (Hpd (!r)); zomega.
  set pu' := update_pu _ _ _.
  set pfrom' := posr _ _ _.
  case=> Hrd.
    rewrite (_ : update_pu _ _ _ = pu'); first by zomega.
    apply/(PeqPr r).
    by move: Hrd; rewrite /rd !ffunE => ->; rewrite addrAC addrA addrNK !eqxx.
  pose pd' := posr r 0 1.
  rewrite (_ : update_pu _ _ _ = pu' + pd'); last first.
    rewrite /pu' /pd' /update_pu; apply/(PeqPr r).
    move: Hrd; rewrite /rd; rewrite ?rpossimpl; move=> ->.
    by rewrite addr0 -addrA !eqxx.
  lapply (IHos pu' pfrom' pd'); first by zomega.
  by rewrite /pd'; case; case r; rewrite ffunE //=.
Qed.

Lemma min_moves_aux_le:
  forall (os : seq Order) (pu pfrom : Pos) (mb: Move Blue) (mo : Move Orange),
    min_moves_aux pu pfrom os <= min_moves_aux (pu + move mb + move mo) pfrom os + 1.
Proof.
  move=> os pu pfrom mb mo.
  set bd := move mb.
  set od := move mo.
  have: bd Blue = -1 \/ 0 <= bd Blue <= 1.
    by rewrite /bd ffunE; case mb => /=; zomega.
  have: od Orange = -1 \/ 0 <= od Orange <= 1.
    by rewrite /od ffunE; case mo => /=; zomega.
  have H := @min_moves_aux_1_1 os (pu + _) pfrom _.
  case=> hod; case=> hbd.
  * lapply (H (bd + od) (-(bd + od))).
      by rewrite addrK addrA; auto with zarith.
    by case; move: hod hbd; rewrite /bd /od !ffunE /=; case mb; case mo; zomega.
  * lapply (H od (-od)); last first.
      by case; move: hod; rewrite !ffunE /=; case mo; zomega.
    rewrite addrK.
    lapply (H od bd); last first.
      by case; move: hbd; rewrite !ffunE /=; case mb; zomega.
    by rewrite addrAC; zomega.
  * lapply (H bd (-bd)); last first.
      by case; move: hbd; rewrite !ffunE /=; case mb; zomega.
    rewrite addrK.
    lapply (H bd od); last first.
      by case; move: hod; rewrite !ffunE /=; case mo; zomega.
    by zomega.
  * lapply (H 0 (bd + od)).
      by rewrite addr0 addrA; zomega.
    by case; move: hod hbd; rewrite /bd /od !ffunE /=; case mb; case mo; zomega.
Qed.

Lemma min_moves_le:
  forall (os : seq Order) (pu pfrom : Pos) (mb : Move Blue) (mo : Move Orange),
    min_moves_aux pu pfrom os <= min_moves_aux pu (pfrom + move mb + move mo) os + 1.
Proof.
  move=> os pu pfrom mb mo.
  case: (min_moves_aux_1 os pu (pfrom + move mb) mo) => mo' ->.
  case: (min_moves_aux_1 os (pu + move mo') pfrom mb) => mb' ->.
  rewrite addrAC.
  by apply: min_moves_aux_le.
Qed.

Lemma min_moves_le_correct:
  forall (ms : seq Moves) (pfrom pto : Pos) (os : seq Order),
    Correct pfrom pto os ms ->
    min_moves_aux 0 pfrom os <= Z_of_nat (size ms).
Proof.
  move=> ms pfrom pto os hc.
  elim: {pfrom pto os}ms / hc; first by done.
    move=> pfrom mb mo os ms pto hc /=.
    rewrite Zpos_P_of_succ_nat.
    move: (@min_moves_le os 0 pfrom mb mo).
    by zomega.
  move=> pfrom r mv os ms pto hc /=.
  rewrite Zpos_P_of_succ_nat.
  rewrite /distance addrN /=.
  rewrite /move_cost ffunE addrN /Zmax0 /Zmax /=.
  rewrite (_ : posr _ _ _ = pfrom); last by poscrush r.
  rewrite (_ : update_pu _ _ _ = posr r 0 1); last by poscrush r.
  case: (min_moves_aux_1 os 0 pfrom mv) => mv' ->.
  rewrite !add0r.
  set mx : Z := min_moves_aux _ _ _.
  set m1 : Z := min_moves_aux _ _ _.
  suff: m1 <= mx; first by rewrite /m1 /mx; zomega.
  pose f := min_moves_aux (posr r 0 _) pfrom os.
  have mon: forall x : Z, f (x + 1) <= f x.
    rewrite /f; move=> x.
    set  px := posr r 0 x.
    pose p1 := posr r 0 1.
    lapply (@min_moves_aux_1_1 os px pfrom p1).
      rewrite (_ : posr _ _ _ = px + p1); first by zomega.
      by poscrush r.
    by case; rewrite ffunE; case r.
  move: (mon 0) (mon (-1)); rewrite add0r addNr /f /m1 /mx.
  set p1 := posr _ _ _.
  set p0 := posr _ _ _.
  set pm := posr _ _ _.
  set px := move _.
  suff: [|| px == p1, px == p0 | px == pm].
    by case/or3P; move/eqP => ->; zomega.
  rewrite !(sameP eqP (PeqPr r _ _)).
  by rewrite ?rpossimpl; case mv'; rewrite !eqxx.
Qed.

Definition min_path_find_fun (os : seq Order) (pu pfrom : Pos) (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_path_find:
  forall (os : seq Order) (pu pfrom : Pos) (r : Robo) (pbutton : Z),
    pu r >= 0 ->
    let mv := min_path_find_fun os pu pfrom r pbutton in
      min_moves_aux pu (pfrom + move mv) (order r pbutton::os) =
      min_moves_aux (pu + posr0 r 1) pfrom (order r pbutton::os).
Proof.
  move=> os pu pfrom r pbutton hpu mv /=.
  set pu' : Pos := pu + _.
  set c0 := move_cost _ _ _.
  set c1 := move_cost _ _ _.
  have eq : c0 = c1.
    rewrite /c0 /c1 /move_cost /distance.
    rewrite /mv /min_path_find_fun /pu'.
    case Z_lt_le_dec.
      move=> hlt; congr (Zmax0 _ + _).
      by rewrite ?rpossimpl 2?Zabs_non_eq /=; move: hlt; zomega.
    case Z_eq_dec.
      move=> -> _.
      by rewrite ?rpossimpl /Zmax0 2?Zmax_left /=; move: hpu; zomega.
    move=> hne hlt; congr (Zmax0 _ + _).
    by rewrite ?rpossimpl 2?Zabs_eq /=; move: hlt hne; zomega.
  rewrite eq.
  congr +%R; congr min_moves_aux; by poscrush r.
Qed.

Fixpoint min_path_find_funr (os : seq Order) (pu pfrom : Pos) (r : Robo) :=
match os with
| nil => Stay r
| order r' pbutton :: os' =>
  if Robo_eq_decinv r' r is left _ then
    min_path_find_fun os' pu pfrom r pbutton
  else
    let dist := distance pfrom pbutton r' in
    let cost := move_cost pu dist r' in
    min_path_find_funr os'
      (update_pu pu cost r')
      (posr r' pbutton (pfrom r))
      r
end.

Lemma min_path_find2:
  forall (os : seq Order) (pu pfrom : Pos) (r : Robo),
    pu r >= 0 ->
    let mv := min_path_find_funr os pu pfrom r in
      min_moves_aux pu (pfrom + move mv) os =
      min_moves_aux (pu + posr r 1 0) pfrom os.
Proof.
  elim; first by move=> * /=.
  case=> r' pbutton' os IH pu pfrom r.
  rewrite [min_moves_aux]lock /= -lock.
  case Robo_eq_decinv => -> {r'}.
    by apply min_path_find.
  set pu' := update_pu _ _ _.
  set pfrom' := posr _ _ _.
  move=> hpu /=.
  set c0 := move_cost _ _ _.
  set c1 := move_cost _ _ _.
  have -> : c0 = c1.
    by rewrite /c0 /c1 /move_cost /distance ?rpossimpl.
  congr +%R.
  lapply (IH pu' pfrom' r); last first.
    rewrite /pu' ?rpossimpl /move_cost /Zmax0.
    set v := distance _ _ _ - _.
    have := Zle_max_l 0 v.
    by move: hpu; zomega.
  rewrite /=.
  set mv := min_path_find_funr _ _ _ _.
  move=> eq.
  apply (ecomp eq).
    congr min_moves_aux.
      by rewrite /pu' /c1 /move_cost; poscrush r.
    by poscrush r.
  congr min_moves_aux.
    rewrite /pu' /c1 /move_cost; poscrush r.
    by rewrite andbT /=; apply/eqP; zomega.
  by poscrush r.
Qed.

Definition min_path_find_fun2 (os : seq Order) (pfrom : Pos) :=
  let mo := min_path_find_funr os (posm 1 0) pfrom Orange in
  let mb := min_path_find_funr os 0 (pfrom + move mo) Blue in
    (mb, mo).

Lemma min_path_find3:
  forall (os : seq Order) (pfrom : Pos),
    let (mb, mo) := min_path_find_fun2 os pfrom in
      min_moves_aux (posm 1 1) pfrom os = min_moves_aux 0 (pfrom + move mb + move mo) os.
Proof.
  rewrite /min_path_find_fun2.
  move=> os pfrom.
  lapply (@min_path_find2 os (posm 1 0) pfrom Orange); last by rewrite ?rpossimpl.
  simpl.
  set mo := min_path_find_funr _ _ _ _.
  lapply (@min_path_find2 os 0 (pfrom + move mo) Blue); last by rewrite ?rpossimpl.
  set mb := min_path_find_funr _ _ _ _.
  rewrite add0r addrAC /=.
  move=> -> eq.
  by apply esym; apply (ecomp eq); congr min_moves_aux; poscrush Blue.
Qed.

Lemma min_moves_aux_u11:
  forall (os : seq Order) (pfrom : Pos) (r : Robo) (pbutton : Z),
    let os' := order r pbutton::os in
      pfrom r <> pbutton ->
      min_moves_aux (posm 1 1) pfrom os' + 1 = min_moves_aux 0 pfrom os'.
Proof.
  move=> os pfrom r pbutton /= hne.
  set d := distance _ _ _.
  have: d > 0.
    rewrite /d /distance.
    have := Zabs_spec (pbutton - pfrom r).
    by move: hne; zomega.
  set c0 := move_cost _ _ _.
  set c1 := move_cost _ _ _.
  move=> dpos.
  have -> : c0 = c1 - 1.
    rewrite /c0 /c1 /move_cost /Zmax0 ?rpossimpl.
    have := Zmax_spec 0 (d - 1).
    have := Zmax_spec 0 d.
    move: dpos.
    by case r; zomega.
  rewrite -addrA subrK.
  congr +%R; congr min_moves_aux.
  by rewrite /c1 /move_cost; poscrush r; case r; rewrite addrC eqxx.
Qed.

Lemma min_path_find4:
  forall (os : seq Order) (pfrom : Pos) (r : Robo) (pbutton : Z),
    let os' := order r pbutton::os in
      pfrom r <> pbutton ->
      let (mb, mo) := min_path_find_fun2 os' pfrom in
        min_moves_aux 0 (pfrom + move mb + move mo) os' + 1 = min_moves_aux 0 pfrom os'.
Proof.
  move=> os pfrom r pbutton os' neq.
  move: (min_path_find3 os' pfrom).
  move: (min_path_find_fun2 _ _) => [mb mo] <-.
  by apply min_moves_aux_u11.
Qed.

Lemma min_moves_aux_u10:
  forall (os : seq Order) (pfrom : Pos) (r : Robo) (pbutton : Z),
    let os' := order r pbutton::os in
      pfrom r = pbutton ->
      min_moves_aux (posr r 0 1) pfrom os + 1 = min_moves_aux 0 pfrom os'.
Proof.
  move=> os pfrom r pbutton /= <- {pbutton}.
  congr +%R; last by rewrite /move_cost /distance ?rpossimpl.
  congr min_moves_aux.
    by rewrite /move_cost /distance; poscrush r.
  by poscrush r.
Qed.

Lemma min_path_find5:
  forall (os : seq Order) (pfrom : Pos) (r : Robo) (pbutton : Z),
    let os' := order r pbutton::os in
      pfrom r = pbutton ->
      let mv := min_path_find_funr os 0 pfrom (!r) in
        min_moves_aux 0 (pfrom + move mv) os + 1 = min_moves_aux 0 pfrom os'.
Proof.
  rewrite [min_moves_aux]lock.
  move=> os pfrom r pbutton /= <- {pbutton}.
  lapply (@min_path_find2 os 0 pfrom (!r)); last by rewrite ?rpossimpl.
  set mv := min_path_find_funr _ _ _ _.
  move=> /= eq.
  rewrite -lock eq.
  rewrite -min_moves_aux_u10; last by [].
  congr +%R; congr min_moves_aux.
  by poscrush r.
Qed.

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

Definition correct_pushmove (os : seq Order) (pfrom : Pos) (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 : Pos) :=
match mv with
| moves mb mo => pfrom + move mb + move mo
| pushmove r mv => pfrom + move mv
end.

Definition min_path_find_f (os : seq Order) (pfrom : Pos) :=
match os with
| nil => moves (Stay _) (Stay _)
| order r pbutton::os' =>
    if pfrom r == pbutton then
      let mv := min_path_find_funr os' 0 pfrom (!r) in
        pushmove mv
    else
      let (mb, mo) := min_path_find_fun2 os pfrom in
        moves mb mo
end.

Lemma min_path_find6:
  forall (os : seq Order) (pfrom : Pos),
     os <> nil ->
     let mv := min_path_find_f os pfrom in
       correct_pushmove os pfrom mv &&
       (min_moves_aux 0 (do_moves mv pfrom) (clear_head_order os mv) + 1 ==
         min_moves_aux 0 pfrom os).
Proof.
  case; first by [].
  move=> [r pbutton] os pfrom _.
  rewrite [min_moves_aux]lock /min_path_find_f /correct_pushmove.
  case: (pfrom r =P pbutton).
    move=> <- {pbutton}.
    rewrite /= !eqxx !andTb -lock.
    by apply/eqP; apply min_path_find5.
  move=> neq.
  by rewrite andTb -lock /clear_head_order -min_path_find4 ?eqxx.
Qed.

Lemma min_moves_aux_noneg:
  forall (os : seq Order) (pu pfrom : Pos),
     0 <= min_moves_aux pu pfrom os.
Proof.
  elim; first by [].
  move=> [r pbutton] os IH pu pfrom /=.
  set c := move_cost _ _ _.
  set pu' := update_pu _ _ _.
  set pfrom' := posr _ _ _.
  move: (IH pu' pfrom').
  have: 0 <= c; last by zomega.
  rewrite /c /move_cost /Zmax0.
  set d := distance _ _ _ - _.
  have := Zmax_spec 0 d.
  by zomega.
Qed.

Lemma min_trans_zero:
  forall (os : seq Order) (pu pfrom : Pos),
    os = nil <-> min_moves_aux pu pfrom os = 0.
Proof.
  case; first by [].
  move=> [r pbutton] os pu pfrom.
  split; first by [].
  rewrite /=.
  set x := min_moves_aux _ _ _.
  have: 0 <= x; first by apply min_moves_aux_noneg.
  set y := move_cost _ _ _.
  have: 0 < y.
    rewrite /y /move_cost /Zmax0.
    set d := distance _ _ _ - _.
    have := Zmax_spec 0 d.
    by zomega.
  move=> h1 h2 h3; exfalso.
  move: h1 h2 h3; zomega.
Qed.

Fixpoint min_path_find_list_r (n : nat) (os : seq Order) (pfrom : Pos) :=
match n with
| O => nil
| S n' =>
  let mv := min_path_find_f os pfrom in
    mv :: min_path_find_list_r n' (clear_head_order os mv) (do_moves mv pfrom)
end.

Lemma min_moves_aux_ex_aux:
  forall (n : nat) (os : seq Order) (pfrom : Pos),
    min_moves_aux 0 pfrom os = Z_of_nat n ->
    let ws := min_path_find_list_r n os pfrom in
      exists pend, Correct pfrom pend os ws /\ n = size ws.
Proof.
  elim.
    move=> os pfrom /= eq.
    exists pfrom.
    move/min_trans_zero in eq.
    rewrite eq.
    by split; constructor.
  move=> n IH.
  case; first by [].
  move=> [r pbutton] os pfrom.
  set os' := _ :: os.
  lapply (@min_path_find6 os' pfrom); last by [].
  case/andP.
  set os'' := clear_head_order _ _.
  set pfrom' := do_moves _ _.
  move=> hc heq heq2; move/eqP in heq.
  case: (IH os'' pfrom').
    by move: heq heq2; rewrite inj_S; zomega.
  move=> pend [hc' heq'] ws.
  exists pend.
  split; last by rewrite /ws; congr S.
  move: hc hc'.
  rewrite /ws /correct_pushmove.
  rewrite /min_path_find_list_r -/min_path_find_list_r /os'' /os' /pfrom'.
  move: (min_path_find_f _ _); case.
    by move=> *; constructor.
  by move=> r' mv; case/andP; move/eqP => <-; move/eqP => <-; constructor.
Qed.

Definition min_path_find_list (os : seq Order) (pfrom : Pos) :=
  min_path_find_list_r (Zabs_nat (min_moves_aux 0 pfrom os)) os pfrom.

Lemma min_moves_ex:
  forall (os: seq Order) (pfrom : Pos),
    let ws := min_path_find_list os pfrom in
      exists pend, Correct pfrom pend os ws /\
      min_moves_aux 0 pfrom os = Z_of_nat (size ws).
Proof.
  move=> os pfrom.
  rewrite /min_path_find_list.
  set n := Zabs_nat _.
  set n' := min_moves_aux _ _ _.
  have eq: n' = Z_of_nat n.
    rewrite /n /n' inj_Zabs_nat Zabs_eq //.
    by apply min_moves_aux_noneg.
  case: (@min_moves_aux_ex_aux n os pfrom eq).
  move=> pend [hc <-].
  by exists pend.
Qed.

Definition minimum_moves (os : seq Order) : seq Moves :=
  min_path_find_list os (posm 1 1).

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

Theorem minimum_moves_is_correct:
  forall (os : seq Order),
    let ws := minimum_moves os in
      correct_moves os ws.
Proof.
  move=> os /=.
  rewrite /minimum_moves /correct_moves.
  move: (min_moves_ex os (posm 1 1)) => [pend [hc _]].
  by exists pend.
Qed.

Theorem minimum_moves_is_minimum:
  forall (os : seq Order),
    let ws := minimum_moves os in
      forall ws', correct_moves os ws' ->
        (size ws <= size ws')%nat.
Proof.
  move=> os /= ws' [pend' hc].
  rewrite /minimum_moves /correct_moves.
  move: (min_moves_ex os (posm 1 1)) => [pend [_ heq]].
  apply/leP; apply inj_le_rev.
  rewrite -heq.
  by apply: min_moves_le_correct hc.
Qed.

Example sample_nil : seq 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_moves_aux 0 (posm 1 1) sample_nil).
Eval vm_compute in (min_moves_aux 0 (posm 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.

*)