Created
May 14, 2011 01:40
-
-
Save kik/971586 to your computer and use it in GitHub Desktop.
GCJ 2011 Qual-A さらにやり直し。今度こそ完璧な証明が書けたはずだ
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment