GCJ 2011 Qual-A やり直し。今度は正しいパスを得られてるけど、最小生の証明ができてない。まだ途中

A2.v

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

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

Inductive Move : Set := Left | Right | Stay.
Inductive Moves : Set :=
| moves : Move -> Move -> Moves
| pushBlue: Move -> Moves
| pushOrange: 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
| Left  => p-1
| Stay  => p
| Right => p+1
end.

Inductive Correct (bp op: Z) : Z -> Z -> list Order -> list Moves -> Prop :=
| c_nil: Correct bp op bp op nil nil
| c_moves mb mo os ms bend oend:
  Correct (do_move mb bp) (do_move mo op) bend oend os ms ->
  Correct bp op bend oend os (moves mb mo::ms)
| cm_pushOrange mb os ms bend oend:
  Correct (do_move mb bp) op bend oend os ms ->
  Correct bp op bend oend (order Orange op::os) (pushOrange mb::ms)
| cm_pushBlue mo os ms bend oend:
  Correct bp (do_move mo op) bend oend os ms ->
  Correct bp op bend oend (order Blue bp::os) (pushBlue mo::ms).

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

Record MMResult : Set := mmresult {
  mmr_moves: list Moves;
  mmr_bp: Z;
  mmr_op: Z
}.

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

Lemma make_move_case:
  forall (x x': Z),
    let m := make_move x x' in
    m = (Left, x'+1) \/ m = (Stay, x') \/ m = (Right, x'-1).
Proof.
  intros.
  unfold make_move in m.
  destruct (x ?= x'); auto.
Qed.

Fixpoint make_moves_aux n bp op bp' op' ws :=
match n with
| O => mmresult ws bp' op'
| S n' =>
  let (mb, bp'') := make_move bp bp' in
  let (mo, op'') := make_move op op' in
  make_moves_aux n' bp op bp'' op'' (moves mb mo::ws)
end.

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

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

Lemma Z_lemma_2: forall x, x - x = 0.
Proof. intros. omega. Qed.

Ltac zsimpl :=
  repeat (rewrite Z_lemma_0 || rewrite Z_lemma_1 || rewrite Z_lemma_2).
Ltac zsimplin H :=
  repeat (rewrite Z_lemma_0 in H || rewrite Z_lemma_1 in H || rewrite Z_lemma_2 in H).

Lemma make_moves_aux_correct:
  forall n bp op bp' op' bp'' op'' ws,
    let mmr := make_moves_aux n bp op bp' op' ws in
    Correct bp' op' bp'' op'' nil ws ->
    Correct (mmr_bp mmr) (mmr_op mmr) bp'' op'' nil (mmr_moves mmr).
Proof.
  induction n.
  simpl. auto.

  intros.
  unfold mmr.
  simpl.
  destruct (make_move_case bp bp') as [Hm|[Hm|Hm]];
    rewrite Hm; clear Hm;
  destruct (make_move_case op op') as [Hm|[Hm|Hm]];
    rewrite Hm; clear Hm;
  apply IHn; constructor; simpl;
  zsimpl; auto.
Qed.

Definition make_moves n bp op bp' op' := make_moves_aux n bp op bp' op' nil.

Lemma make_moves_correct:
  forall n bp op bp' op',
    let mmr := make_moves n bp op bp' op' in
    Correct (mmr_bp mmr) (mmr_op mmr) bp' op' nil (mmr_moves mmr).
Proof.
  intros. apply make_moves_aux_correct. constructor.
Qed.

Definition make_pushBlue (bp op bp' op': Z) :=
  let n := Zabs_nat (bp - bp') in
  let mmr := make_moves n bp op bp' op' in
  let (mo, op'') := make_move op (mmr_op mmr) in
  mmresult (pushBlue mo::mmr_moves mmr) (mmr_bp mmr) op''.

Definition make_pushOrange (bp op bp' op': Z) :=
  let n := Zabs_nat (op - op') in
  let mmr := make_moves n bp op bp' op' in
  let (mb, bp'') := make_move bp (mmr_bp mmr) in
  mmresult (pushOrange mb::mmr_moves mmr) bp'' (mmr_op mmr).

Lemma Zabs_lemma_0:
  forall x y, 0%nat = Zabs_nat (x - y) -> x = y.
Proof.
  intros. apply inj_eq in H. rewrite inj_Zabs_nat in H. simpl in H.
  destruct (Zabs_dec (x - y)); omega.
Qed.

Lemma Zabs_lemma_1:
  forall x y n, S n = Zabs_nat (x - y) -> x < y \/ x > y.
Proof.
  intros.
  destruct (Ztrichotomy x y) as [|[|]]; auto.
  rewrite H0 in H. zsimplin H. simpl in H. omega.
Qed.

Lemma Zabs_lemma_2:
  forall x y n, S n = Zabs_nat (x - y) -> x < y -> n = Zabs_nat (x - (y - 1)).
Proof.
  intros. apply inj_eq in H. apply inj_eq_rev.
  rewrite inj_Zabs_nat in *.
  rewrite inj_S in H.
  rewrite Zabs_non_eq in *; omega.
Qed.

Lemma Zabs_lemma_3:
  forall x y n, S n = Zabs_nat (x - y) -> x > y -> n = Zabs_nat (x - (y + 1)).
Proof.
  intros. apply inj_eq in H. apply inj_eq_rev.
  rewrite inj_Zabs_nat in *.
  rewrite inj_S in H.
  rewrite Zabs_eq in *; omega.
Qed.


Lemma make_moves_aux_bp:
  forall n bp op bp' op' ws, n = Zabs_nat (bp - bp') ->
    let mmr := make_moves_aux n bp op bp' op' ws in
    mmr_bp mmr = bp.
Proof.
  induction n; simpl; intros.
  symmetry. auto using Zabs_lemma_0.
  generalize (make_move op op').
  destruct p as [mo op''].
  destruct (Zabs_lemma_1 _ _ _ H) as [Hb|Hb];
    unfold make_move; rewrite Hb;
    auto using Zabs_lemma_2, Zabs_lemma_3.
Qed.

Lemma make_moves_aux_op:
  forall n bp op bp' op' ws, n = Zabs_nat (op - op') ->
    let mmr := make_moves_aux n bp op bp' op' ws in
    mmr_op mmr = op.
Proof.
  induction n; simpl; intros.
  symmetry. auto using Zabs_lemma_0.
  generalize (make_move bp bp').
  destruct p as [mo bp''].
  destruct (Zabs_lemma_1 _ _ _ H) as [Hb|Hb];
    unfold make_move; rewrite Hb;
    auto using Zabs_lemma_2, Zabs_lemma_3.
Qed.

Lemma cons_app_lemma:
  forall A (x: A) xs, x::xs = (x::nil)++xs.
Proof. auto. Qed.

Lemma make_pushBlue_correct:
  forall bp op bp' op',
    let mmr := make_pushBlue bp op bp' op' in
    Correct (mmr_bp mmr) (mmr_op mmr) bp' op' (order Blue bp::nil) (mmr_moves mmr).
Proof.
  intros bp op bp' op'.
  unfold make_pushBlue.
  specialize (make_moves_aux_bp (Zabs_nat (bp - bp')) bp op bp' op' nil).
  unfold make_moves.
  set (mmr := make_moves_aux (Zabs_nat (bp - bp')) bp op bp' op' nil).
  intro Hbp.
  destruct (make_move_case op (mmr_op mmr)) as [Ho|[Ho|Ho]];
    rewrite Ho; clear Ho; simpl;
  rewrite (cons_app_lemma Order); rewrite (cons_app_lemma Moves);
  rewrite <- Hbp; auto;
  apply correct_app with (mmr_bp mmr) (mmr_op mmr);try apply make_moves_correct;
  constructor; simpl; zsimpl; constructor.
Qed.

Lemma make_pushOrange_correct:
  forall bp op bp' op',
    let mmr := make_pushOrange bp op bp' op' in
    Correct (mmr_bp mmr) (mmr_op mmr) bp' op' (order Orange op::nil) (mmr_moves mmr).
Proof.
  intros bp op bp' op'.
  unfold make_pushOrange.
  specialize (make_moves_aux_op (Zabs_nat (op - op')) bp op bp' op' nil).
  unfold make_moves.
  set (mmr := make_moves_aux (Zabs_nat (op - op')) bp op bp' op' nil).
  intro Hbp.
  destruct (make_move_case bp (mmr_bp mmr)) as [Ho|[Ho|Ho]];
    rewrite Ho; clear Ho; simpl;
  rewrite (cons_app_lemma Order); rewrite (cons_app_lemma Moves);
  rewrite <- Hbp; auto;
  apply correct_app with (mmr_bp mmr) (mmr_op mmr);try apply make_moves_correct;
  constructor; simpl; zsimpl; constructor.
Qed.

Definition app_mmr mmr mmr' :=
  mmresult (mmr_moves mmr ++ mmr_moves mmr') (mmr_bp mmr) (mmr_op mmr).

Fixpoint make_correct_moves_aux (bp op: Z) (os: list Order) :=
match os with
| nil => mmresult nil bp op
| order Blue bp'::os' =>
    let mmr  := make_correct_moves_aux bp' op os' in
    let mmr' := make_pushBlue bp' op (mmr_bp mmr) (mmr_op mmr) in
    app_mmr mmr' mmr
| order Orange op'::os' =>
    let mmr  := make_correct_moves_aux bp op' os' in
    let mmr' := make_pushOrange bp op' (mmr_bp mmr) (mmr_op mmr) in
    app_mmr mmr' mmr
end.

Lemma make_correct_moves_aux_correct:
  forall os bp op,
    let mmr := make_correct_moves_aux bp op os in
    exists bp', exists op',
      Correct (mmr_bp mmr) (mmr_op mmr) bp' op' os (mmr_moves mmr).
Proof.
  induction os.
  simpl. intros. exists bp. exists op. constructor.
  intros.
  simpl in mmr.
  destruct a as [[|] pp];
    [
      set (bp0 := pp) in *;
      set (op0 := op) in *;
      set (make := make_pushBlue) in *
    |
      set (bp0 := bp) in *;
      set (op0 := pp) in *;
      set (make := make_pushOrange) in *
    ];
    destruct (IHos bp0 op0) as [bp' [op' Hc]];
    exists bp'; exists op';
    set (mmr1 := make_correct_moves_aux bp0 op0 os) in *;
    set (mmr2 := make bp0 op0 (mmr_bp mmr1) (mmr_op mmr1)) in *;
    unfold mmr; simpl; rewrite cons_app_lemma;
    apply correct_app with (mmr_bp mmr1) (mmr_op mmr1); auto.
  apply make_pushBlue_correct.
  apply make_pushOrange_correct.
Qed.

Definition make_correct_moves (bp op: Z) (os: list Order) :=
let mmr1 := make_correct_moves_aux bp op os in
let nb := Zabs_nat (bp - (mmr_bp mmr1)) in
let mmr2 := make_moves nb bp op (mmr_bp mmr1) (mmr_op mmr1) in
let no := Zabs_nat (op - (mmr_op mmr2)) in
let mmr3 := make_moves no bp op (mmr_bp mmr2) (mmr_op mmr2) in
app_mmr mmr3 (app_mmr mmr2 mmr1).

Lemma make_moves_eq:
  forall n bp op op',
    let mmr := make_moves n bp op bp op' in
    mmr_bp mmr = bp.
Proof.
  unfold make_moves.
  intro n.
  generalize (nil: list Moves).
  induction n.
  simpl. auto.
  simpl.
  intros.
  generalize (make_move op op').
  destruct p as [mo op''].
  unfold make_move.
  rewrite Zcompare_refl.
  auto.
Qed.

Lemma make_correct_moves_correct:
  forall os bp op,
    let mmr := make_correct_moves bp op os in
    exists bp', exists op',
      Correct bp op bp' op' os (mmr_moves mmr).
Proof.
  intros.
  destruct (make_correct_moves_aux_correct os bp op) as [bp' [op' Hc]].
  unfold make_correct_moves in mmr.
  set (mmr1 := make_correct_moves_aux bp op os) in *.
  set (nb := Zabs_nat (bp - (mmr_bp mmr1))) in *.
  set (mmr2 := make_moves nb bp op (mmr_bp mmr1) (mmr_op mmr1)) in *.
  set (no := Zabs_nat (op - (mmr_op mmr2))) in *.
  set (mmr3 := make_moves no bp op (mmr_bp mmr2) (mmr_op mmr2)) in *.
  exists bp'. exists op'.
  unfold mmr.
  assert (Hb:  mmr_bp mmr2 = bp).
  apply (make_moves_aux_bp nb bp op (mmr_bp mmr1) (mmr_op mmr1) nil); auto.
  assert (Hb': mmr_bp mmr3 = bp).
  unfold mmr3.
  rewrite Hb.
  apply (make_moves_eq no bp op (mmr_op mmr2)).
  assert (Ho:  mmr_op mmr3 = op).
  apply (make_moves_aux_op no bp op (mmr_bp mmr2) (mmr_op mmr2) nil); auto.
  simpl. replace os with (nil++nil++os) by auto.
  apply correct_app with bp (mmr_op mmr2).
  rewrite <- Hb' at 1. rewrite <- Hb. rewrite <- Ho.
  apply make_moves_correct.
  apply correct_app with (mmr_bp mmr1) (mmr_op mmr1).
  rewrite <- Hb.
  apply make_moves_correct.
  auto.
Qed.