diff options
Diffstat (limited to 'backend/Parallelmove.v')
| -rw-r--r-- | backend/Parallelmove.v | 2759 |
1 files changed, 260 insertions, 2499 deletions
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index f95416eb..b2ec930b 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -1,2529 +1,290 @@ -(** Translation of parallel moves into sequences of individual moves *) +Require Import Coqlib. +Require Parmov. +Require Import Values. +Require Import Events. +Require Import AST. +Require Import Locations. +Require Import Conventions. -(** The ``parallel move'' problem, also known as ``parallel assignment'', - is the following. We are given a list of (source, destination) pairs - of locations. The goal is to find a sequence of elementary - moves ([loc <- loc] assignments) such that, at the end of the sequence, - location [dst] contains the value of location [src] at the beginning of - the sequence, for each ([src], [dst]) pairs in the given problem. - Moreover, other locations should keep their values, except one register - of each type, which can be used as temporaries in the generated sequences. +Definition temp_for (l: loc) : loc := + match Loc.type l with Tint => R IT2 | Tfloat => R FT2 end. - The parallel move problem is trivial if the sources and destinations do - not overlap. For instance, -<< - (R1, R2) <- (R3, R4) becomes R1 <- R3; R2 <- R4 ->> - However, arbitrary overlap is allowed between sources and destinations. - This requires some care in ordering the individual moves, as in -<< - (R1, R2) <- (R3, R1) becomes R2 <- R1; R1 <- R3 ->> - Worse, cycles (permutations) can require the use of temporaries, as in -<< - (R1, R2, R3) <- (R2, R3, R1) becomes T <- R1; R1 <- R2; R2 <- R3; R3 <- T; ->> - An amazing fact is that for any parallel move problem, at most one temporary - (or in our case one integer temporary and one float temporary) is needed. +Definition parmove (srcs dsts: list loc) := + Parmov.parmove2 loc temp_for Loc.eq srcs dsts. - The development in this section was contributed by Laurence Rideau and - Bernard Serpette. It is described in their paper - ``Coq à la conquête des moulins'', JFLA 2005, - #<A HREF="http://www-sop.inria.fr/lemme/Laurence.Rideau/RideauSerpetteJFLA05.ps"># - http://www-sop.inria.fr/lemme/Laurence.Rideau/RideauSerpetteJFLA05.ps - #</A># -*) +Definition moves := (list (loc * loc))%type. -Require Omega. -Require Import Wf_nat. -Require Import Conventions. -Require Import Coqlib. -Require Import Bool_nat. -Require Import TheoryList. -Require Import Bool. -Require Import Arith. -Require Import Peano_dec. -Require Import EqNat. -Require Import Values. -Require Import LTL. -Require Import EqNat. -Require Import Locations. -Require Import AST. - -Section pmov. - -Ltac caseEq name := generalize (refl_equal name); pattern name at -1; case name. -Hint Resolve beq_nat_eq . - -Lemma neq_is_neq: forall (x y : nat), x <> y -> beq_nat x y = false. -Proof. -unfold not; intros. -caseEq (beq_nat x y); auto. -intro. -elim H; auto. -Qed. -Hint Resolve neq_is_neq . - -Lemma app_nil: forall (A : Set) (l : list A), l ++ nil = l. -Proof. -intros A l; induction l as [|a l Hrecl]; auto; simpl; rewrite Hrecl; auto. -Qed. - -Lemma app_cons: - forall (A : Set) (l1 l2 : list A) (a : A), (a :: l1) ++ l2 = a :: (l1 ++ l2). -Proof. -auto. -Qed. - -Lemma app_app: - forall (A : Set) (l1 l2 l3 : list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. -Proof. -intros A l1; induction l1 as [|a l1 Hrecl1]; simpl; auto; intros; - rewrite Hrecl1; auto. -Qed. - -Lemma app_rewrite: - forall (A : Set) (l : list A) (x : A), - (exists y : A , exists r : list A , l ++ (x :: nil) = y :: r ). -Proof. -intros A l x; induction l as [|a l Hrecl]. -exists x; exists (nil (A:=A)); auto. -inversion Hrecl; inversion H. -exists a; exists (l ++ (x :: nil)); auto. -Qed. - -Lemma app_rewrite2: - forall (A : Set) (l l2 : list A) (x : A), - (exists y : A , exists r : list A , l ++ (x :: l2) = y :: r ). -Proof. -intros A l l2 x; induction l as [|a l Hrecl]. -exists x; exists l2; auto. -inversion Hrecl; inversion H. -exists a; exists (l ++ (x :: l2)); auto. -Qed. - -Lemma app_rewriter: - forall (A : Set) (l : list A) (x : A), - (exists y : A , exists r : list A , x :: l = r ++ (y :: nil) ). -Proof. -intros A l x; induction l as [|a l Hrecl]. -exists x; exists (nil (A:=A)); auto. -inversion Hrecl; inversion H. -generalize H0; case x1; simpl; intros; inversion H1. -exists a; exists (x0 :: nil); simpl; auto. -exists x0; exists (a0 :: (a :: l0)); simpl; auto. -Qed. -Hint Resolve app_rewriter . - -Definition Reg := loc. - -Definition T := - fun (r : loc) => - match Loc.type r with Tint => R IT2 | Tfloat => R FT2 end. - -Definition notemporary := fun (r : loc) => forall x, Loc.diff r (T x). - -Definition Move := (Reg * Reg)%type. - -Definition Moves := list Move. - -Definition State := ((Moves * Moves) * Moves)%type. - -Definition StateToMove (r : State) : Moves := - match r with ((t, b), l) => t end. - -Definition StateBeing (r : State) : Moves := - match r with ((t, b), l) => b end. - -Definition StateDone (r : State) : Moves := - match r with ((t, b), l) => l end. - -Fixpoint noRead (p : Moves) (r : Reg) {struct p} : Prop := - match p with - nil => True - | (s, d) :: l => Loc.diff s r /\ noRead l r - end. - -Lemma noRead_app: - forall (l1 l2 : Moves) (r : Reg), - noRead l1 r -> noRead l2 r -> noRead (l1 ++ l2) r. -Proof. -intros; induction l1 as [|a l1 Hrecl1]; simpl; auto. -destruct a. -elim H; intros; split; auto. -Qed. - -Inductive step : State -> State -> Prop := - step_nop: - forall (r : Reg) (t1 t2 l : Moves), - step (t1 ++ ((r, r) :: t2), nil, l) (t1 ++ t2, nil, l) - | step_start: - forall (t1 t2 l : Moves) (m : Move), - step (t1 ++ (m :: t2), nil, l) (t1 ++ t2, m :: nil, l) - | step_push: - forall (t1 t2 b l : Moves) (s d r : Reg), - step - (t1 ++ ((d, r) :: t2), (s, d) :: b, l) - (t1 ++ t2, (d, r) :: ((s, d) :: b), l) - | step_loop: - forall (t b l : Moves) (s d r0 r0ounon : Reg), - step - (t, (s, r0ounon) :: (b ++ ((r0, d) :: nil)), l) - (t, (s, r0ounon) :: (b ++ ((T r0, d) :: nil)), (r0, T r0) :: l) - | step_pop: - forall (t b l : Moves) (s0 d0 sn dn : Reg), - noRead t dn -> - Loc.diff dn s0 -> - step - (t, (sn, dn) :: (b ++ ((s0, d0) :: nil)), l) - (t, b ++ ((s0, d0) :: nil), (sn, dn) :: l) - | step_last: - forall (t l : Moves) (s d : Reg), - noRead t d -> step (t, (s, d) :: nil, l) (t, nil, (s, d) :: l) . -Hint Resolve step_nop step_start step_push step_loop step_pop step_last . - -Fixpoint path (l : Moves) : Prop := - match l with - nil => True - | (s, d) :: l => - match l with - nil => True - | (ss, dd) :: l2 => s = dd /\ path l - end - end. - -Lemma path_pop: forall (m : Move) (l : Moves), path (m :: l) -> path l. -Proof. -simpl; intros m l; destruct m as [ms md]; case l; auto. -intros m0; destruct m0; intros; inversion H; auto. -Qed. - -Fixpoint noWrite (p : Moves) (r : Reg) {struct p} : Prop := - match p with - nil => True - | (s, d) :: l => Loc.diff d r /\ noWrite l r - end. - -Lemma noWrite_pop: - forall (p1 p2 : Moves) (m : Move) (r : Reg), - noWrite (p1 ++ (m :: p2)) r -> noWrite (p1 ++ p2) r. -Proof. -intros; induction p1 as [|a p1 Hrecp1]. -generalize H; simpl; case m; intros; inversion H0; auto. -generalize H; rewrite app_cons; rewrite app_cons. -simpl; case a; intros. -inversion H0; split; auto. -Qed. - -Lemma noWrite_in: - forall (p1 p2 : Moves) (r0 r1 r2 : Reg), - noWrite (p1 ++ ((r1, r2) :: p2)) r0 -> Loc.diff r0 r2. -Proof. -intros; induction p1 as [|a p1 Hrecp1]; simpl; auto. -generalize H; simpl; intros; inversion H0; auto. -apply Loc.diff_sym; auto. -generalize H; rewrite app_cons; simpl; case a; intros. -apply Hrecp1; inversion H0; auto. -Qed. - -Lemma noWrite_swap: - forall (p : Moves) (m1 m2 : Move) (r : Reg), - noWrite (m1 :: (m2 :: p)) r -> noWrite (m2 :: (m1 :: p)) r. -Proof. -intros p m1 m2 r; simpl; case m1; case m2. -intros; inversion H; inversion H1; split; auto. -Qed. - -Lemma noWrite_movFront: - forall (p1 p2 : Moves) (m : Move) (r0 : Reg), - noWrite (p1 ++ (m :: p2)) r0 -> noWrite (m :: (p1 ++ p2)) r0. -Proof. -intros p1 p2 m r0; induction p1 as [|a p1 Hrecp1]; auto. -case a; intros r1 r2; rewrite app_cons; rewrite app_cons. -intros; apply noWrite_swap; rewrite <- app_cons. -simpl in H |-; inversion H; unfold noWrite; fold noWrite; auto. -Qed. - -Lemma noWrite_insert: - forall (p1 p2 : Moves) (m : Move) (r0 : Reg), - noWrite (m :: (p1 ++ p2)) r0 -> noWrite (p1 ++ (m :: p2)) r0. -Proof. -intros p1 p2 m r0; induction p1 as [|a p1 Hrecp1]. -simpl; auto. -destruct a; simpl. -destruct m. -intros [H1 [H2 H3]]; split; auto. -apply Hrecp1. -simpl; auto. -Qed. - -Lemma noWrite_tmpLast: - forall (t : Moves) (r s d : Reg), - noWrite (t ++ ((s, d) :: nil)) r -> - forall (x : Reg), noWrite (t ++ ((x, d) :: nil)) r. -Proof. -intros; induction t as [|a t Hrect]. -simpl; auto. -generalize H; simpl; case a; intros; inversion H0; split; auto. -Qed. - -Fixpoint simpleDest (p : Moves) : Prop := - match p with - nil => True - | (s, d) :: l => noWrite l d /\ simpleDest l - end. - -Lemma simpleDest_Pop: - forall (m : Move) (l1 l2 : Moves), - simpleDest (l1 ++ (m :: l2)) -> simpleDest (l1 ++ l2). -Proof. -intros; induction l1 as [|a l1 Hrecl1]. -generalize H; simpl; case m; intros; inversion H0; auto. -generalize H; rewrite app_cons; rewrite app_cons. -simpl; case a; intros; inversion H0; split; auto. -apply (noWrite_pop l1 l2 m); auto. -Qed. - -Lemma simpleDest_pop: - forall (m : Move) (l : Moves), simpleDest (m :: l) -> simpleDest l. -Proof. -intros m l; simpl; case m; intros _ r [X Y]; auto. -Qed. - -Lemma simpleDest_right: - forall (l1 l2 : Moves), simpleDest (l1 ++ l2) -> simpleDest l2. -Proof. -intros l1; induction l1 as [|a l1 Hrecl1]; auto. -intros l2; rewrite app_cons; intros; apply Hrecl1. -apply (simpleDest_pop a); auto. -Qed. - -Lemma simpleDest_swap: - forall (m1 m2 : Move) (l : Moves), - simpleDest (m1 :: (m2 :: l)) -> simpleDest (m2 :: (m1 :: l)). -Proof. -intros m1 m2 l; simpl; case m1; case m2. -intros _ r0 _ r2 [[X Y] [Z U]]; auto. -(repeat split); auto. -apply Loc.diff_sym; auto. -Qed. - -Lemma simpleDest_pop2: - forall (m1 m2 : Move) (l : Moves), - simpleDest (m1 :: (m2 :: l)) -> simpleDest (m1 :: l). -Proof. -intros; apply (simpleDest_pop m2); apply simpleDest_swap; auto. -Qed. - -Lemma simpleDest_movFront: - forall (p1 p2 : Moves) (m : Move), - simpleDest (p1 ++ (m :: p2)) -> simpleDest (m :: (p1 ++ p2)). -Proof. -intros p1 p2 m; induction p1 as [|a p1 Hrecp1]. -simpl; auto. -rewrite app_cons; rewrite app_cons. -case a; intros; simpl in H |-; inversion H. -apply simpleDest_swap; simpl; auto. -destruct m. -cut (noWrite ((r1, r2) :: (p1 ++ p2)) r0). -cut (simpleDest ((r1, r2) :: (p1 ++ p2))). -intro; (repeat split); elim H3; elim H2; intros; auto. -apply Hrecp1; auto. -apply noWrite_movFront; auto. -Qed. - -Lemma simpleDest_insert: - forall (p1 p2 : Moves) (m : Move), - simpleDest (m :: (p1 ++ p2)) -> simpleDest (p1 ++ (m :: p2)). -Proof. -intros p1 p2 m; induction p1 as [|a p1 Hrecp1]. -simpl; auto. -rewrite app_cons; intros. -simpl. -destruct a as [a1 a2]. -split. -destruct m; simpl in H |-. -apply noWrite_insert. -simpl; split; elim H; intros [H1 H2] [H3 H4]; auto. -apply Loc.diff_sym; auto. -apply Hrecp1. -apply simpleDest_pop2 with (a1, a2); auto. -Qed. - -Lemma simpleDest_movBack: - forall (p1 p2 : Moves) (m : Move), - simpleDest (p1 ++ (m :: p2)) -> simpleDest ((p1 ++ p2) ++ (m :: nil)). -Proof. -intros. -apply (simpleDest_insert (p1 ++ p2) nil m). -rewrite app_nil; apply simpleDest_movFront; auto. -Qed. - -Lemma simpleDest_swap_app: - forall (t1 t2 t3 : Moves) (m : Move), - simpleDest (t1 ++ (m :: (t2 ++ t3))) -> simpleDest ((t1 ++ t2) ++ (m :: t3)). -Proof. -intros. -apply (simpleDest_insert (t1 ++ t2) t3 m). -rewrite <- app_app. -apply simpleDest_movFront; auto. -Qed. - -Lemma simpleDest_tmpLast: - forall (t : Moves) (s d : Reg), - simpleDest (t ++ ((s, d) :: nil)) -> - forall (r : Reg), simpleDest (t ++ ((r, d) :: nil)). -Proof. -intros t s d; induction t as [|a t Hrect]. -simpl; auto. -simpl; case a; intros; inversion H; split; auto. -apply (noWrite_tmpLast t r0 s); auto. -Qed. - -Fixpoint noTmp (b : Moves) : Prop := - match b with - nil => True - | (s, d) :: l => - (forall r, Loc.diff s (T r)) /\ - ((forall r, Loc.diff d (T r)) /\ noTmp l) - end. - -Fixpoint noTmpLast (b : Moves) : Prop := - match b with - nil => True - | (s, d) :: nil => forall r, Loc.diff d (T r) - | (s, d) :: l => - (forall r, Loc.diff s (T r)) /\ - ((forall r, Loc.diff d (T r)) /\ noTmpLast l) - end. - -Lemma noTmp_app: - forall (l1 l2 : Moves) (m : Move), - noTmp l1 -> noTmpLast (m :: l2) -> noTmpLast (l1 ++ (m :: l2)). -Proof. -intros. -induction l1 as [|a l1 Hrecl1]. -simpl; auto. -simpl. -caseEq (l1 ++ (m :: l2)); intro. -destruct a. -elim H; intros; auto. -inversion H; auto. -elim H3; auto. -intros; destruct a as [a1 a2]. -elim H; intros H2 [H3 H4]; auto. -(repeat split); auto. -rewrite H1 in Hrecl1; apply Hrecl1; auto. -Qed. - -Lemma noTmpLast_popBack: - forall (t : Moves) (m : Move), noTmpLast (t ++ (m :: nil)) -> noTmp t. -Proof. -intros. -induction t as [|a t Hrect]. -simpl; auto. -destruct a as [a1 a2]. -rewrite app_cons in H. -simpl. -simpl in H |-. -generalize H; caseEq (t ++ (m :: nil)); intros. -destruct t; inversion H0. -elim H1. -intros H2 [H3 H4]; (repeat split); auto. -rewrite <- H0 in H4. -apply Hrect; auto. -Qed. - -Fixpoint getsrc (p : Moves) : list Reg := - match p with - nil => nil - | (s, d) :: l => s :: getsrc l - end. - -Fixpoint getdst (p : Moves) : list Reg := - match p with - nil => nil - | (s, d) :: l => d :: getdst l - end. - -Fixpoint noOverlap_aux (r : Reg) (l : list Reg) {struct l} : Prop := - match l with - nil => True - | b :: m => (b = r \/ Loc.diff b r) /\ noOverlap_aux r m - end. - -Definition noOverlap (p : Moves) : Prop := - forall l, In l (getsrc p) -> noOverlap_aux l (getdst p). - -Definition stepInv (r : State) : Prop := - path (StateBeing r) /\ - (simpleDest (StateToMove r ++ StateBeing r) /\ - (noOverlap (StateToMove r ++ StateBeing r) /\ - (noTmp (StateToMove r) /\ noTmpLast (StateBeing r)))). - -Definition Value := val. - -Definition Env := locset. - -Definition get (e : Env) (r : Reg) := Locmap.get r e. - -Definition update (e : Env) (r : Reg) (v : Value) : Env := Locmap.set r v e. - -Fixpoint sexec (p : Moves) (e : Env) {struct p} : Env := - match p with - nil => e - | (s, d) :: l => let e' := sexec l e in - update e' d (get e' s) - end. - -Fixpoint pexec (p : Moves) (e : Env) {struct p} : Env := - match p with - nil => e - | (s, d) :: l => update (pexec l e) d (get e s) - end. - -Lemma get_update: - forall (e : Env) (r1 r2 : Reg) (v : Value), - get (update e r1 v) r2 = - (if Loc.eq r1 r2 then v else if Loc.overlap r1 r2 then Vundef else get e r2). -Proof. -intros. -unfold update, get, Locmap.get, Locmap.set; trivial. -Qed. - -Lemma get_update_id: - forall (e : Env) (r1 : Reg) (v : Value), get (update e r1 v) r1 = v. -Proof. -intros e r1 v; rewrite (get_update e r1 r1); auto. -case (Loc.eq r1 r1); auto. -intros H; elim H; trivial. -Qed. - -Lemma get_update_diff: - forall (e : Env) (r1 r2 : Reg) (v : Value), - Loc.diff r1 r2 -> get (update e r1 v) r2 = get e r2. -Proof. -intros; unfold update, get, Locmap.get, Locmap.set. -case (Loc.eq r1 r2); intro. -absurd (r1 = r2); [apply Loc.diff_not_eq; trivial | trivial]. -caseEq (Loc.overlap r1 r2); intro; trivial. -absurd (Loc.diff r1 r2); [apply Loc.overlap_not_diff; assumption | assumption]. -Qed. - -Lemma get_update_ndiff: - forall (e : Env) (r1 r2 : Reg) (v : Value), - r1 <> r2 -> not (Loc.diff r1 r2) -> get (update e r1 v) r2 = Vundef. -Proof. -intros; unfold update, get, Locmap.get, Locmap.set. -case (Loc.eq r1 r2); intro. -absurd (r1 = r2); assumption. -caseEq (Loc.overlap r1 r2); intro; trivial. -absurd (Loc.diff r1 r2); (try assumption). -apply Loc.non_overlap_diff; assumption. -Qed. - -Lemma pexec_swap: - forall (m1 m2 : Move) (t : Moves), - simpleDest (m1 :: (m2 :: t)) -> - forall (e : Env) (r : Reg), - get (pexec (m1 :: (m2 :: t)) e) r = get (pexec (m2 :: (m1 :: t)) e) r. -Proof. -intros; destruct m1 as [m1s m1d]; destruct m2 as [m2s m2d]. -generalize H; simpl; intros [[NEQ NW] [NW2 HSD]]; clear H. -case (Loc.eq m1d r); case (Loc.eq m2d r); intros. -absurd (m1d = m2d); - [apply Loc.diff_not_eq; apply Loc.diff_sym; assumption | - rewrite e0; rewrite e1; trivial]. -caseEq (Loc.overlap m2d r); intro. -absurd (Loc.diff m2d m1d); [apply Loc.overlap_not_diff; rewrite e0 | idtac]; - (try assumption). -subst m1d; rewrite get_update_id; rewrite get_update_diff; - (try rewrite get_update_id); auto. -caseEq (Loc.overlap m1d r); intro. -absurd (Loc.diff m1d m2d); - [apply Loc.overlap_not_diff; rewrite e0 | apply Loc.diff_sym]; assumption. -subst m2d; (repeat rewrite get_update_id); rewrite get_update_diff; - [rewrite get_update_id; trivial | apply Loc.diff_sym; trivial]. -caseEq (Loc.overlap m1d r); caseEq (Loc.overlap m2d r); intros. -(repeat rewrite get_update_ndiff); - (try (apply Loc.overlap_not_diff; assumption)); trivial. -assert (~ Loc.diff m1d r); - [apply Loc.overlap_not_diff; assumption | - intros; rewrite get_update_ndiff; auto]. -rewrite get_update_diff; - [rewrite get_update_ndiff; auto | apply Loc.non_overlap_diff; auto]. -cut (~ Loc.diff m2d r); [idtac | apply Loc.overlap_not_diff; auto]. -cut (Loc.diff m1d r); [idtac | apply Loc.non_overlap_diff; auto]. -intros; rewrite get_update_diff; auto. -(repeat rewrite get_update_ndiff); auto. -cut (Loc.diff m1d r); [idtac | apply Loc.non_overlap_diff; auto]. -cut (Loc.diff m2d r); [idtac | apply Loc.non_overlap_diff; auto]. -intros; (repeat rewrite get_update_diff); auto. -Qed. - -Lemma pexec_add: - forall (t1 t2 : Moves) (r : Reg) (e : Env), - get (pexec t1 e) r = get (pexec t2 e) r -> - forall (a : Move), get (pexec (a :: t1) e) r = get (pexec (a :: t2) e) r. -Proof. -intros. -case a. -simpl. -intros a1 a2. -unfold get, update, Locmap.set, Locmap.get. -case (Loc.eq a2 r); case (Loc.overlap a2 r); auto. -Qed. - -Lemma pexec_movBack: - forall (t1 t2 : Moves) (m : Move), - simpleDest (m :: (t1 ++ t2)) -> - forall (e : Env) (r : Reg), - get (pexec (m :: (t1 ++ t2)) e) r = get (pexec (t1 ++ (m :: t2)) e) r. -Proof. -intros t1 t2 m; induction t1 as [|a t1 Hrect1]. -simpl; auto. -rewrite app_cons. -intros; rewrite pexec_swap; auto; rewrite app_cons; auto. -apply pexec_add. -apply Hrect1. -apply (simpleDest_pop2 m a); auto. -Qed. - -Lemma pexec_movFront: - forall (t1 t2 : Moves) (m : Move), - simpleDest (t1 ++ (m :: t2)) -> - forall (e : Env) (r : Reg), - get (pexec (t1 ++ (m :: t2)) e) r = get (pexec (m :: (t1 ++ t2)) e) r. -Proof. -intros; rewrite <- pexec_movBack; eauto. -apply simpleDest_movFront; auto. -Qed. - -Lemma pexec_mov: - forall (t1 t2 t3 : Moves) (m : Move), - simpleDest ((t1 ++ (m :: t2)) ++ t3) -> - forall (e : Env) (r : Reg), - get (pexec ((t1 ++ (m :: t2)) ++ t3) e) r = - get (pexec ((t1 ++ t2) ++ (m :: t3)) e) r. -Proof. -intros t1 t2 t3 m. -rewrite <- app_app. -rewrite app_cons. -intros. -rewrite pexec_movFront; auto. -cut (simpleDest (m :: (t1 ++ (t2 ++ t3)))). -rewrite app_app. -rewrite <- pexec_movFront; auto. -apply simpleDest_swap_app; auto. -apply simpleDest_movFront; auto. -Qed. - -Definition diff_dec: - forall (x y : Reg), ({ Loc.diff x y }) + ({ not (Loc.diff x y) }). -intros. -case (Loc.eq x y). -intros heq; right. -red; intro; absurd (x = y); auto. -apply Loc.diff_not_eq; auto. -intro; caseEq (Loc.overlap x y). -intro; right. -apply Loc.overlap_not_diff; auto. -intro; left; apply Loc.non_overlap_diff; auto. -Defined. - -Lemma get_pexec_id_noWrite: - forall (t : Moves) (d : Reg), - noWrite t d -> - forall (e : Env) (v : Value), v = get (pexec t (update e d v)) d. -Proof. -intros. -induction t as [|a t Hrect]. -simpl. -rewrite get_update_id; auto. -generalize H; destruct a as [a1 a2]; simpl; intros [NEQ R]. -rewrite get_update_diff; auto. -Qed. - -Lemma pexec_nop: - forall (t : Moves) (r : Reg) (e : Env) (x : Reg), - Loc.diff r x -> get (pexec ((r, r) :: t) e) x = get (pexec t e) x. -Proof. -intros. -simpl. -rewrite get_update_diff; auto. -Qed. - -Lemma sD_nW: forall t r s, simpleDest ((s, r) :: t) -> noWrite t r. -Proof. -induction t. -simpl; auto. -simpl. -destruct a. -intros r1 r2 H; split; [try assumption | idtac]. -elim H; - [intros H0 H1; elim H0; [intros H2 H3; (try clear H0 H); (try exact H2)]]. -elim H; - [intros H0 H1; elim H0; [intros H2 H3; (try clear H0 H); (try exact H3)]]. -Qed. - -Lemma sD_pexec: - forall (t : Moves) (s d : Reg), - simpleDest ((s, d) :: t) -> forall (e : Env), get (pexec t e) d = get e d. -Proof. -intros. -induction t as [|a t Hrect]; simpl; auto. -destruct a as [a1 a2]. -simpl in H |-; elim H; intros [H0 H1] [H2 H3]; clear H. -case (Loc.eq a2 d); intro. -absurd (a2 = d); [apply Loc.diff_not_eq | trivial]; assumption. -rewrite get_update_diff; (try assumption). -apply Hrect. -simpl; (split; assumption). -Qed. - -Lemma noOverlap_nil: noOverlap nil. -Proof. -unfold noOverlap, noOverlap_aux, getsrc, getdst; trivial. -Qed. - -Lemma getsrc_add: - forall (m : Move) (l1 l2 : Moves) (l : Reg), - In l (getsrc (l1 ++ l2)) -> In l (getsrc (l1 ++ (m :: l2))). -Proof. -intros m l1 l2 l; destruct m; induction l1; simpl; auto. -destruct a; simpl; intros. -elim H; intros H0; [left | right]; auto. -Qed. - -Lemma getdst_add: - forall (r1 r2 : Reg) (l1 l2 : Moves), - getdst (l1 ++ ((r1, r2) :: l2)) = getdst l1 ++ (r2 :: getdst l2). -Proof. -intros r1 r2 l1 l2; induction l1; simpl; auto. -destruct a; simpl; rewrite IHl1; auto. -Qed. - -Lemma getdst_app: - forall (l1 l2 : Moves), getdst (l1 ++ l2) = getdst l1 ++ getdst l2. -Proof. -intros; induction l1; simpl; auto. -destruct a; simpl; rewrite IHl1; auto. -Qed. - -Lemma noOverlap_auxpop: - forall (x r : Reg) (l : list Reg), - noOverlap_aux x (r :: l) -> noOverlap_aux x l. -Proof. -induction l; simpl; auto. -intros [H1 [H2 H3]]; split; auto. -Qed. - -Lemma noOverlap_auxPop: - forall (x r : Reg) (l1 l2 : list Reg), - noOverlap_aux x (l1 ++ (r :: l2)) -> noOverlap_aux x (l1 ++ l2). -Proof. -intros x r l1 l2; (try assumption). -induction l1 as [|a l1 Hrecl1]; simpl app. -intro; apply (noOverlap_auxpop x r); auto. -(repeat rewrite app_cons); simpl. -intros [H1 H2]; split; auto. -Qed. - -Lemma noOverlap_pop: - forall (m : Move) (l : Moves), noOverlap (m :: l) -> noOverlap l. -Proof. -induction l. -intro; apply noOverlap_nil. -unfold noOverlap; simpl; destruct m; destruct a; simpl; intros. -elim (H l0); intros; (try assumption). -elim H0; intros H1; right; [left | right]; assumption. -Qed. - -Lemma noOverlap_Pop: - forall (m : Move) (l1 l2 : Moves), - noOverlap (l1 ++ (m :: l2)) -> noOverlap (l1 ++ l2). -Proof. -intros m l1 l2; induction l1 as [|a l1 Hrecl1]; simpl. -simpl; apply noOverlap_pop. -(repeat rewrite app_cons); unfold noOverlap; destruct a; simpl. -intros H l H0; split. -elim (H l); [intros H1 H2 | idtac]; auto. -elim H0; [intros H3; left | intros H3; right; apply getsrc_add]; auto. -unfold noOverlap in Hrecl1 |-. -elim H0; intros H1; clear H0. -destruct m; rewrite getdst_app; apply noOverlap_auxPop with ( r := r2 ). -rewrite getdst_add in H. -elim H with ( l := l ); [intros H0 H2; (try clear H); (try exact H2) | idtac]. -left; (try assumption). -apply Hrecl1 with ( l := l ); auto. -intros l0 H0; (try assumption). -elim H with ( l := l0 ); [intros H2 H3; (try clear H); (try exact H3) | idtac]; - auto. -Qed. - -Lemma noOverlap_right: - forall (l1 l2 : Moves), noOverlap (l1 ++ l2) -> noOverlap l2. -Proof. -intros l1; induction l1 as [|a l1 Hrecl1]; auto. -intros l2; rewrite app_cons; intros; apply Hrecl1. -apply (noOverlap_pop a); auto. -Qed. - -Lemma pexec_update: - forall t e d r v, - Loc.diff d r -> - noRead t d -> get (pexec t (update e d v)) r = get (pexec t e) r. -Proof. -induction t; simpl. -intros; rewrite get_update_diff; auto. -destruct a as [a1 a2]; intros; case (Loc.eq a2 r); intro. -subst a2; (repeat rewrite get_update_id). -rewrite get_update_diff; auto; apply Loc.diff_sym; elim H0; auto. -case (diff_dec a2 r); intro. -(repeat rewrite get_update_diff); auto. -apply IHt; auto. -elim H0; auto. -(repeat rewrite get_update_ndiff); auto. -Qed. - -Lemma pexec_push: - forall (t l : Moves) (s d : Reg), - noRead t d -> - simpleDest ((s, d) :: t) -> - forall (e : Env) (r : Reg), - r = d \/ Loc.diff d r -> - get (pexec ((s, d) :: t) (sexec l e)) r = - get (pexec t (sexec ((s, d) :: l) e)) r. -Proof. -intros; simpl. -elim H1; intros e1. -rewrite e1; rewrite get_update_id; auto. -rewrite (sD_pexec t s d); auto; rewrite get_update_id; auto. -rewrite pexec_update; auto. -rewrite get_update_diff; auto. -Qed. - -Definition exec (s : State) (e : Env) := - pexec (StateToMove s ++ StateBeing s) (sexec (StateDone s) e). - -Definition sameEnv (e1 e2 : Env) := - forall (r : Reg), notemporary r -> get e1 r = get e2 r. - -Definition NoOverlap (r : Reg) (s : State) := - noOverlap ((r, r) :: (StateToMove s ++ StateBeing s)). - -Lemma noOverlapaux_swap2: - forall (l1 l2 : list Reg) (m l : Reg), - noOverlap_aux l (l1 ++ (m :: l2)) -> noOverlap_aux l (m :: (l1 ++ l2)). -Proof. -intros l1 l2 m l; induction l1; simpl noOverlap_aux; auto. -intros; elim H; intros H0 H1; (repeat split); auto. -simpl in IHl1 |-. -elim IHl1; [intros H2 H3; (try exact H2) | idtac]; auto. -apply (noOverlap_auxpop l m). -apply IHl1; auto. -Qed. - -Lemma noTmp_noReadTmp: forall t, noTmp t -> forall s, noRead t (T s). -Proof. -induction t; simpl; auto. -destruct a as [a1 a2]; intros. -split; [idtac | apply IHt]; elim H; intros H1 [H2 H3]; auto. -Qed. - -Lemma noRead_by_path: - forall (b t : Moves) (r0 r1 r7 r8 : Reg), - simpleDest ((r7, r8) :: (b ++ ((r0, r1) :: nil))) -> - path (b ++ ((r0, r1) :: nil)) -> Loc.diff r8 r0 -> noRead b r8. -Proof. -intros; induction b as [|a b Hrecb]; simpl; auto. -destruct a as [a1 a2]; generalize H H0; rewrite app_cons; intros; split. -simpl in H3 |-; caseEq (b ++ ((r0, r1) :: nil)); intro. -destruct b; inversion H4. -intros l H4. -rewrite H4 in H3. -destruct m. -rewrite H4 in H2; simpl in H2 |-. -elim H3; [intros H5 H6; (try clear H3); (try exact H5)]. -rewrite H5. -elim H2; intros [H3 [H7 H8]] [H9 [H10 H11]]; (try assumption). -apply Hrecb. -apply (simpleDest_pop (a1, a2)); apply simpleDest_swap; auto. -apply (path_pop (a1, a2)); auto. -Qed. - -Lemma noOverlap_swap: - forall (m1 m2 : Move) (l : Moves), - noOverlap (m1 :: (m2 :: l)) -> noOverlap (m2 :: (m1 :: l)). -Proof. -intros m1 m2 l; simpl; destruct m1 as [m1s m1d]; destruct m2 as [m2s m2d]. -unfold noOverlap; simpl; intros. -assert (m1s = l0 \/ (m2s = l0 \/ In l0 (getsrc l))). -elim H0; [intros H1 | intros [H1|H2]]. -right; left; (try assumption). -left; (try assumption). -right; right; (try assumption). -(repeat split); - (elim (H l0); [intros H2 H3; elim H3; [intros H4 H5] | idtac]; auto). -Qed. - -Lemma getsrc_add1: - forall (r1 r2 : Reg) (l1 l2 : Moves), - getsrc (l1 ++ ((r1, r2) :: l2)) = getsrc l1 ++ (r1 :: getsrc l2). -Proof. -intros r1 r2 l1 l2; induction l1; simpl; auto. -destruct a; simpl; rewrite IHl1; auto. -Qed. - -Lemma getsrc_app: - forall (l1 l2 : Moves), getsrc (l1 ++ l2) = getsrc l1 ++ getsrc l2. -Proof. -intros; induction l1; simpl; auto. -destruct a; simpl; rewrite IHl1; auto. -Qed. - -Lemma Ingetsrc_swap: - forall (m : Move) (l1 l2 : Moves) (l : Reg), - In l (getsrc (m :: (l1 ++ l2))) -> In l (getsrc (l1 ++ (m :: l2))). -Proof. -intros; destruct m as [m1 m2]; simpl; auto. -simpl in H |-. -elim H; intros H0; auto. -rewrite H0; rewrite getsrc_add1; auto. -apply (in_or_app (getsrc l1) (l :: getsrc l2)); auto. -right; apply in_eq; auto. -apply getsrc_add; auto. -Qed. - -Lemma noOverlap_movFront: - forall (p1 p2 : Moves) (m : Move), - noOverlap (p1 ++ (m :: p2)) -> noOverlap (m :: (p1 ++ p2)). -Proof. -intros p1 p2 m; unfold noOverlap. -destruct m; rewrite getdst_add; simpl getdst; rewrite getdst_app; intros. -apply noOverlapaux_swap2. -apply (H l); apply Ingetsrc_swap; auto. -Qed. - -Lemma step_inv_loop_aux: - forall (t l : Moves) (s d : Reg), - simpleDest (t ++ ((s, d) :: nil)) -> - noTmp t -> - forall (e : Env) (r : Reg), - notemporary r -> - d = r \/ Loc.diff d r -> - get (pexec (t ++ ((s, d) :: nil)) (sexec l e)) r = - get (pexec (t ++ ((T s, d) :: nil)) (sexec ((s, T s) :: l) e)) r. -Proof. -intros; (repeat rewrite pexec_movFront); auto. -(repeat rewrite app_nil); simpl; elim H2; intros e1. -subst d; (repeat rewrite get_update_id); auto. -(repeat rewrite get_update_diff); auto. -rewrite pexec_update; auto. -apply Loc.diff_sym; unfold notemporary in H1 |-; auto. -apply noTmp_noReadTmp; auto. -apply (simpleDest_tmpLast t s); auto. -Qed. - -Lemma step_inv_loop: - forall (t l : Moves) (s d : Reg), - simpleDest (t ++ ((s, d) :: nil)) -> - noTmpLast (t ++ ((s, d) :: nil)) -> - forall (e : Env) (r : Reg), - notemporary r -> - d = r \/ Loc.diff d r -> - get (pexec (t ++ ((s, d) :: nil)) (sexec l e)) r = - get (pexec (t ++ ((T s, d) :: nil)) (sexec ((s, T s) :: l) e)) r. -Proof. -intros; apply step_inv_loop_aux; auto. -apply (noTmpLast_popBack t (s, d)); auto. -Qed. - -Definition sameExec (s1 s2 : State) := - forall (e : Env) (r : Reg), - (let A := - getdst - ((StateToMove s1 ++ StateBeing s1) ++ (StateToMove s2 ++ StateBeing s2)) - in - notemporary r -> - (forall x, In x A -> r = x \/ Loc.diff r x) -> - get (exec s1 e) r = get (exec s2 e) r). - -Lemma get_noWrite: - forall (t : Moves) (d : Reg), - noWrite t d -> forall (e : Env), get e d = get (pexec t e) d. -Proof. -intros; induction t as [|a t Hrect]; simpl; auto. -generalize H; destruct a as [a1 a2]; simpl; intros [NEQ R]. -unfold get, Locmap.get, update, Locmap.set. -case (Loc.eq a2 d); intro; auto. -absurd (a2 = d); auto; apply Loc.diff_not_eq; (try assumption). -caseEq (Loc.overlap a2 d); intro. -absurd (Loc.diff a2 d); auto; apply Loc.overlap_not_diff; auto. -unfold get, Locmap.get in Hrect |-; apply Hrect; auto. -Qed. - -Lemma step_sameExec: - forall (r1 r2 : State), step r1 r2 -> stepInv r1 -> sameExec r1 r2. -Proof. -intros r1 r2 STEP; inversion STEP; - unfold stepInv, sameExec, NoOverlap, exec, StateToMove, StateBeing, StateDone; - (repeat rewrite app_nil); intros [P [SD [NO [TT TB]]]]; intros. -rewrite pexec_movFront; simpl; auto. -case (Loc.eq r r0); intros e0. -subst r0; rewrite get_update_id; apply get_noWrite; apply sD_nW with r; - apply simpleDest_movFront; auto. -elim H2 with ( x := r ); - [intros H3; absurd (r = r0); auto | - intros H3; rewrite get_update_diff; auto; apply Loc.diff_sym; auto | idtac]. -(repeat (rewrite getdst_app; simpl)); apply in_or_app; left; apply in_or_app; - right; simpl; auto. -(repeat rewrite pexec_movFront); auto. -rewrite app_nil; auto. -apply simpleDest_movBack; auto. -apply pexec_mov; auto. -repeat (rewrite <- app_cons; rewrite app_app). -apply step_inv_loop; auto. -repeat (rewrite <- app_app; rewrite app_cons; auto). -repeat (rewrite <- app_app; rewrite app_cons; auto). -apply noTmp_app; auto. -elim H2 with ( x := d ); - [intros H3; left; auto | intros H3; right; apply Loc.diff_sym; auto - | try clear H2]. -repeat (rewrite getdst_app; simpl). -apply in_or_app; left; apply in_or_app; right; simpl; right; apply in_or_app; - right; simpl; left; trivial. -rewrite pexec_movFront; auto; apply pexec_push; auto. -apply noRead_app; auto. -apply noRead_app. -apply (noRead_by_path b b s0 d0 sn dn); auto. -apply (simpleDest_right t); auto. -apply (path_pop (sn, dn)); auto. -simpl; split; [apply Loc.diff_sym | idtac]; auto. -apply simpleDest_movFront; auto. -elim H4 with ( x := dn ); [intros H5 | intros H5 | try clear H4]. -left; (try assumption). -right; apply Loc.diff_sym; (try assumption). -repeat (rewrite getdst_app; simpl). -apply in_or_app; left; apply in_or_app; right; simpl; left; trivial. -rewrite pexec_movFront; auto. -rewrite app_nil; auto. -apply pexec_push; auto. -rewrite <- (app_nil _ t). -apply simpleDest_movFront; auto. -elim (H3 d); (try intros H4). -left; (try assumption). -right; apply Loc.diff_sym; (try assumption). -(repeat rewrite getdst_app); simpl; apply in_or_app; left; apply in_or_app; - right; simpl; left; trivial. -Qed. - -Lemma path_tmpLast: - forall (s d : Reg) (l : Moves), - path (l ++ ((s, d) :: nil)) -> path (l ++ ((T s, d) :: nil)). -Proof. -intros; induction l as [|a l Hrecl]. -simpl; auto. -generalize H; (repeat rewrite app_cons). -case a; generalize Hrecl; case l; intros; auto. -destruct m; intros. -inversion H0; split; auto. -Qed. - -Lemma step_inv_path: - forall (r1 r2 : State), step r1 r2 -> stepInv r1 -> path (StateBeing r2). -Proof. -intros r1 r2 STEP; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - intros [P [SD [TT TB]]]; (try (simpl; auto; fail)). -simpl; case m; auto. -generalize P; rewrite <- app_cons; rewrite <- app_cons. -apply (path_tmpLast r0). -generalize P; apply path_pop. -Qed. - -Lemma step_inv_simpleDest: - forall (r1 r2 : State), - step r1 r2 -> stepInv r1 -> simpleDest (StateToMove r2 ++ StateBeing r2). -Proof. -intros r1 r2 STEP; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - (repeat rewrite app_nil); intros [P [SD [TT TB]]]. -apply (simpleDest_Pop (r, r)); assumption. -apply simpleDest_movBack; assumption. -apply simpleDest_insert; rewrite <- app_app; apply simpleDest_movFront. -rewrite <- app_cons; rewrite app_app; auto. -generalize SD; (repeat rewrite <- app_cons); (repeat rewrite app_app). -generalize (simpleDest_tmpLast (t ++ ((s, r0ounon) :: b)) r0 d); auto. -generalize SD; apply simpleDest_Pop. -rewrite <- (app_nil _ t); generalize SD; apply simpleDest_Pop. -Qed. - -Lemma noTmp_pop: - forall (m : Move) (l1 l2 : Moves), noTmp (l1 ++ (m :: l2)) -> noTmp (l1 ++ l2). -Proof. -intros; induction l1 as [|a l1 Hrecl1]; generalize H. -simpl; case m; intros; inversion H0; inversion H2; auto. -rewrite app_cons; rewrite app_cons; simpl; case a. -intros; inversion H0; inversion H2; auto. -Qed. - -Lemma step_inv_noTmp: - forall (r1 r2 : State), step r1 r2 -> stepInv r1 -> noTmp (StateToMove r2). -Proof. -intros r1 r2 STEP; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - intros [P [SD [NO [TT TB]]]]; generalize TT; (try apply noTmp_pop); auto. -Qed. - -Lemma noTmp_noTmpLast: forall (l : Moves), noTmp l -> noTmpLast l. -Proof. -intros; induction l as [|a l Hrecl]; (try (simpl; auto; fail)). -generalize H; simpl; case a; generalize Hrecl; case l; - (intros; inversion H0; inversion H2; auto). -Qed. - -Lemma noTmpLast_pop: - forall (m : Move) (l : Moves), noTmpLast (m :: l) -> noTmpLast l. -Proof. -intros m l; simpl; case m; case l. -simpl; auto. -intros; inversion H; inversion H1; auto. -Qed. - -Lemma noTmpLast_Pop: - forall (m : Move) (l1 l2 : Moves), - noTmpLast (l1 ++ (m :: l2)) -> noTmpLast (l1 ++ l2). -Proof. -intros; induction l1 as [|a l1 Hrecl1]; generalize H. -simpl; case m; case l2. -simpl; auto. -intros. -elim H0; [intros H1 H2; elim H2; [intros H3 H4; (try exact H4)]]. -(repeat rewrite app_cons); simpl; case a. -generalize Hrecl1; case l1. -simpl; case m; case l2; intros; inversion H0; inversion H2; auto. -intros m0 l R r r0; rewrite app_cons; rewrite app_cons. -intros; inversion H0; inversion H2; auto. -Qed. - -Lemma noTmpLast_push: - forall (m : Move) (t1 t2 t3 : Moves), - noTmp (t1 ++ (m :: t2)) -> noTmpLast t3 -> noTmpLast (m :: t3). -Proof. -intros; induction t1 as [|a t1 Hrect1]; generalize H. -simpl; case m; intros r r0 [N1 [N2 NT]]; generalize H0; case t3; auto. -rewrite app_cons; intros; apply Hrect1. -generalize H1. -simpl; case m; case a; intros; inversion H2; inversion H4; auto. -Qed. - -Lemma noTmpLast_tmpLast: - forall (s d : Reg) (l : Moves), - noTmpLast (l ++ ((s, d) :: nil)) -> noTmpLast (l ++ ((T s, d) :: nil)). +Definition exec_seq (m: moves) (e: Locmap.t) : Locmap.t := + Parmov.exec_seq loc val Loc.eq m e. + +Lemma temp_for_charact: + forall l, temp_for l = R IT2 \/ temp_for l = R FT2. Proof. -intros; induction l as [|a l Hrecl]. -simpl; auto. -generalize H; rewrite app_cons; rewrite app_cons; simpl. -case a; generalize Hrecl; case l. -simpl; auto. -intros m l0 REC r r0; generalize REC; rewrite app_cons; rewrite app_cons. -case m; intros; inversion H0; inversion H2; split; auto. + intro; unfold temp_for. destruct (Loc.type l); tauto. Qed. - -Lemma step_inv_noTmpLast: - forall (r1 r2 : State), step r1 r2 -> stepInv r1 -> noTmpLast (StateBeing r2). -Proof. -intros r1 r2 STEP; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - intros [P [SD [NO [TT TB]]]]; auto. -apply (noTmpLast_push m t1 t2); auto. -apply (noTmpLast_push (d, r) t1 t2); auto. -generalize TB; rewrite <- app_cons; rewrite <- app_cons; apply noTmpLast_tmpLast. -apply (noTmpLast_pop (sn, dn)); auto. -Qed. - -Lemma noOverlapaux_insert: - forall (l1 l2 : list Reg) (r x : Reg), - noOverlap_aux x (r :: (l1 ++ l2)) -> noOverlap_aux x (l1 ++ (r :: l2)). -Proof. -simpl; intros; induction l1; simpl; split. -elim H; [intros H0 H1; (try exact H0)]. -elim H; [intros H0 H1; (try exact H1)]. -simpl in H |-. -elim H; - [intros H0 H1; elim H1; [intros H2 H3; (try clear H1 H); (try exact H2)]]. -apply IHl1. -split. -elim H; [intros H0 H1; (try exact H0)]. -rewrite app_cons in H. -apply noOverlap_auxpop with ( r := a ). -elim H; [intros H0 H1; (try exact H1)]. -Qed. - -Lemma Ingetsrc_swap2: - forall (m : Move) (l1 l2 : Moves) (l : Reg), - In l (getsrc (l1 ++ (m :: l2))) -> In l (getsrc (m :: (l1 ++ l2))). -Proof. -intros; destruct m as [m1 m2]; simpl; auto. -induction l1; simpl. -simpl in H |-; auto. -destruct a; simpl. -simpl in H |-. -elim H; [intros H0 | intros H0; (try exact H0)]. -right; left; (try assumption). -elim IHl1; intros; auto. -Qed. - -Lemma noOverlap_insert: - forall (p1 p2 : Moves) (m : Move), - noOverlap (m :: (p1 ++ p2)) -> noOverlap (p1 ++ (m :: p2)). -Proof. -unfold noOverlap; destruct m; rewrite getdst_add; simpl getdst; - rewrite getdst_app. -intros. -apply noOverlapaux_insert. -generalize (H l); intros H1; lapply H1; - [intros H2; (try clear H1); (try exact H2) | idtac]. -simpl getsrc. -generalize (Ingetsrc_swap2 (r, r0)); simpl; (intros; auto). -Qed. - -Lemma noOverlap_movBack: - forall (p1 p2 : Moves) (m : Move), - noOverlap (p1 ++ (m :: p2)) -> noOverlap ((p1 ++ p2) ++ (m :: nil)). -Proof. -intros. -apply (noOverlap_insert (p1 ++ p2) nil m). -rewrite app_nil; apply noOverlap_movFront; auto. -Qed. - -Lemma noOverlap_movBack0: - forall (t : Moves) (s d : Reg), - noOverlap ((s, d) :: t) -> noOverlap (t ++ ((s, d) :: nil)). -Proof. -intros t s d H; (try assumption). -apply noOverlap_insert. -rewrite app_nil; auto. -Qed. - -Lemma noOverlap_Front0: - forall (t : Moves) (s d : Reg), - noOverlap (t ++ ((s, d) :: nil)) -> noOverlap ((s, d) :: t). -Proof. -intros t s d H; (try assumption). -cut ((s, d) :: t = (s, d) :: (t ++ nil)). -intros e; rewrite e. -apply noOverlap_movFront; auto. -rewrite app_nil; auto. -Qed. - -Lemma noTmpL_diff: - forall (t : Moves) (s d : Reg), - noTmpLast (t ++ ((s, d) :: nil)) -> notemporary d. -Proof. -intros t s d; unfold notemporary; induction t; (try (simpl; intros; auto; fail)). -rewrite app_cons. -intros; apply IHt. -apply (noTmpLast_pop a); auto. -Qed. - -Lemma noOverlap_aux_app: - forall l1 l2 (r : Reg), - noOverlap_aux r l1 -> noOverlap_aux r l2 -> noOverlap_aux r (l1 ++ l2). -Proof. -induction l1; simpl; auto. -intros; split. -elim H; [intros H1 H2; (try clear H); (try exact H1)]. -apply IHl1; auto. -elim H; [intros H1 H2; (try clear H); (try exact H2)]. -Qed. - -Lemma noTmP_noOverlap_aux: - forall t (r : Reg), noTmp t -> noOverlap_aux (T r) (getdst t). -Proof. -induction t; simpl; auto. -destruct a; simpl; (intros; split). -elim H; intros; elim H1; intros. -right; apply H2. -apply IHt; auto. -elim H; - [intros H0 H1; elim H1; [intros H2 H3; (try clear H1 H); (try exact H3)]]. -Qed. - -Lemma noTmp_append: forall l1 l2, noTmp l1 -> noTmp l2 -> noTmp (l1 ++ l2). -Proof. -induction l1; simpl; auto. -destruct a. -intros l2 [H1 [H2 H3]] H4. -(repeat split); auto. -Qed. - -Lemma step_inv_noOverlap: - forall (r1 r2 : State), - step r1 r2 -> stepInv r1 -> noOverlap (StateToMove r2 ++ StateBeing r2). -Proof. -intros r1 r2 STEP; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - (repeat rewrite app_nil); intros [P [SD [NO [TT TB]]]]; - (try (generalize NO; apply noOverlap_Pop; auto; fail)). -apply noOverlap_movBack; auto. -apply noOverlap_insert; rewrite <- app_app; apply noOverlap_movFront; - rewrite <- app_cons; rewrite app_app; auto. -generalize NO; (repeat rewrite <- app_cons); (repeat rewrite app_app); - (clear NO; intros NO); apply noOverlap_movBack0. -assert (noOverlap ((r0, d) :: (t ++ ((s, r0ounon) :: b)))); - [apply noOverlap_Front0; auto | idtac]. -generalize H; unfold noOverlap; simpl; clear H; intros. -elim H0; intros; [idtac | apply (H l0); (right; (try assumption))]. -split; [right; (try assumption) | idtac]. -generalize TB; simpl; caseEq (b ++ ((r0, d) :: nil)); intro. -elim (app_eq_nil b ((r0, d) :: nil)); intros; auto; inversion H4. -subst l0; intros; rewrite <- H1 in TB0. -elim TB0; [intros H2 H3; elim H3; [intros H4 H5; (try clear H3 TB0)]]. -generalize (noTmpL_diff b r0 d); unfold notemporary; intro; apply H3; auto. -rewrite <- H1; apply noTmP_noOverlap_aux; apply noTmp_append; auto; - rewrite <- app_cons in TB; apply noTmpLast_popBack with (r0, d); auto. -rewrite <- (app_nil _ t); apply (noOverlap_Pop (s, d)); assumption. -Qed. - -Lemma step_inv: forall (r1 r2 : State), step r1 r2 -> stepInv r1 -> stepInv r2. -Proof. -intros; unfold stepInv; (repeat split). -apply (step_inv_path r1 r2); auto. -apply (step_inv_simpleDest r1 r2); auto. -apply (step_inv_noOverlap r1 r2); auto. -apply (step_inv_noTmp r1 r2); auto. -apply (step_inv_noTmpLast r1 r2); auto. -Qed. - -Definition step_NF (r : State) : Prop := ~ (exists s : State , step r s ). - -Inductive stepp : State -> State -> Prop := - stepp_refl: forall (r : State), stepp r r - | stepp_trans: - forall (r1 r2 r3 : State), step r1 r2 -> stepp r2 r3 -> stepp r1 r3 . -Hint Resolve stepp_refl stepp_trans . - -Lemma stepp_transitive: - forall (r1 r2 r3 : State), stepp r1 r2 -> stepp r2 r3 -> stepp r1 r3. -Proof. -intros; induction H as [r|r1 r2 r0 H H1 HrecH]; eauto. -Qed. - -Lemma step_stepp: forall (s1 s2 : State), step s1 s2 -> stepp s1 s2. -Proof. -eauto. -Qed. - -Lemma stepp_inv: - forall (r1 r2 : State), stepp r1 r2 -> stepInv r1 -> stepInv r2. -Proof. -intros; induction H as [r|r1 r2 r3 H H1 HrecH]; auto. -apply HrecH; auto. -apply (step_inv r1 r2); auto. -Qed. - -Lemma noTmpLast_lastnoTmp: - forall l s d, noTmpLast (l ++ ((s, d) :: nil)) -> notemporary d. -Proof. -induction l. -simpl. -intros; unfold notemporary; auto. -destruct a as [a1 a2]; intros. -change (noTmpLast ((a1, a2) :: (l ++ ((s, d) :: nil)))) in H |-. -apply IHl with s. -apply noTmpLast_pop with (a1, a2); auto. + +Lemma is_not_temp_charact: + forall l, + Parmov.is_not_temp loc temp_for l <-> l <> R IT2 /\ l <> R FT2. +Proof. + intros. unfold Parmov.is_not_temp. + destruct (Loc.eq l (R IT2)). + subst l. intuition. apply (H (R IT2)). reflexivity. discriminate. + destruct (Loc.eq l (R FT2)). + subst l. intuition. apply (H (R FT2)). reflexivity. + assert (forall d, l <> temp_for d). + intro. elim (temp_for_charact d); congruence. + intuition. Qed. - -Lemma step_inv_NoOverlap: - forall (s1 s2 : State) r, - step s1 s2 -> notemporary r -> stepInv s1 -> NoOverlap r s1 -> NoOverlap r s2. + +Lemma disjoint_temp_not_temp: + forall l, Loc.notin l temporaries -> Parmov.is_not_temp loc temp_for l. Proof. -intros s1 s2 r STEP notempr; inversion_clear STEP; unfold stepInv; - unfold stepInv, sameExec, sameEnv, exec, StateToMove, StateBeing, StateDone; - intros [P [SD [NO [TT TB]]]]; unfold NoOverlap; simpl. -simpl; (repeat rewrite app_nil); simpl; (repeat rewrite <- app_cons); intro; - apply noOverlap_Pop with ( m := (r0, r0) ); auto. -(repeat rewrite app_nil); simpl; rewrite app_ass; (repeat rewrite <- app_cons); - intro; rewrite ass_app; apply noOverlap_movBack; auto. -simpl; (repeat (rewrite app_ass; simpl)); (repeat rewrite <- app_cons); intro. -rewrite ass_app; apply noOverlap_insert; rewrite app_ass; - apply noOverlap_movFront; auto. -simpl; (repeat rewrite <- app_cons); intro; rewrite ass_app; - apply noOverlap_movBack0; auto. -generalize H; (repeat (rewrite app_ass; simpl)); intro. -assert (noOverlap ((r0, d) :: (((r, r) :: t) ++ ((s, r0ounon) :: b)))); - [apply noOverlap_Front0 | idtac]; auto. -generalize H0; (repeat (rewrite app_ass; simpl)); auto. -generalize H1; unfold noOverlap; simpl; intros. -elim H3; intros H4; clear H3. -split. -right; assert (notemporary d). -change (noTmpLast (((s, r0ounon) :: b) ++ ((r0, d) :: nil))) in TB |-; - apply (noTmpLast_lastnoTmp ((s, r0ounon) :: b) r0); auto. -rewrite <- H4; unfold notemporary in H3 |-; apply H3. -split. -right; rewrite <- H4; unfold notemporary in notempr |-; apply notempr. -rewrite <- H4; apply noTmP_noOverlap_aux; auto. -apply noTmp_append; auto. -change (noTmpLast (((s, r0ounon) :: b) ++ ((r0, d) :: nil))) in TB |-; - apply noTmpLast_popBack with ( m := (r0, d) ); auto. -apply (H2 l0). -elim H4; intros H3; right; [left | right]; assumption. -intro; - change (noOverlap (((r, r) :: t) ++ ((sn, dn) :: (b ++ ((s0, d0) :: nil))))) in - H1 |-. -change (noOverlap (((r, r) :: t) ++ (b ++ ((s0, d0) :: nil)))); - apply (noOverlap_Pop (sn, dn)); auto. -(repeat rewrite <- app_cons); apply noOverlap_Pop. + intros. rewrite is_not_temp_charact. + unfold temporaries in H; simpl in H. + split; apply Loc.diff_not_eq; tauto. Qed. - -Lemma step_inv_getdst: - forall (s1 s2 : State) r, - step s1 s2 -> - In r (getdst (StateToMove s2 ++ StateBeing s2)) -> - In r (getdst (StateToMove s1 ++ StateBeing s1)). + +Lemma loc_norepet_norepet: + forall l, Loc.norepet l -> list_norepet l. Proof. -intros s1 s2 r STEP; inversion_clear STEP; - unfold StateToMove, StateBeing, StateDone. -(repeat rewrite getdst_app); simpl; (repeat rewrite app_nil); intro; - apply in_or_app. -elim (in_app_or (getdst t1) (getdst t2) r); auto. -intro; right; simpl; right; assumption. -(repeat rewrite getdst_app); destruct m as [m1 m2]; simpl; - (repeat rewrite app_nil); intro; apply in_or_app. -elim (in_app_or (getdst t1 ++ getdst t2) (m2 :: nil) r); auto; intro. -elim (in_app_or (getdst t1) (getdst t2) r); auto; intro. -right; simpl; right; assumption. -elim H0; intros H1; [right; simpl; left; (try assumption) | inversion H1]. -(repeat rewrite getdst_app); simpl; (repeat rewrite app_nil); intro; - apply in_or_app. -elim (in_app_or (getdst t1 ++ getdst t2) (r0 :: (d :: getdst b)) r); auto; - intro. -elim (in_app_or (getdst t1) (getdst t2) r); auto; intro. -left; apply in_or_app; left; assumption. -left; apply in_or_app; right; simpl; right; assumption. -elim H0; intro. -left; apply in_or_app; right; simpl; left; trivial. -elim H1; intro. -right; (simpl; left; trivial). -right; simpl; right; assumption. -(repeat (rewrite getdst_app; simpl)); trivial. -(repeat (rewrite getdst_app; simpl)); intro. -elim (in_app_or (getdst t) (getdst b ++ (d0 :: nil)) r); auto; intro; - apply in_or_app; auto. -elim (in_app_or (getdst b) (d0 :: nil) r); auto; intro. -right; simpl; right; apply in_or_app; auto. -elim H3; intro. -right; simpl; right; apply in_or_app; right; simpl; auto. -inversion H4. -rewrite app_nil; (repeat (rewrite getdst_app; simpl)); intro. -apply in_or_app; left; assumption. + induction 1; constructor. + apply Loc.notin_not_in; auto. auto. Qed. - -Lemma stepp_sameExec: - forall (r1 r2 : State), stepp r1 r2 -> stepInv r1 -> sameExec r1 r2. -Proof. -intros; induction H as [r|r1 r2 r3 H H1 HrecH]. -unfold sameExec; intros; auto. -cut (sameExec r1 r2); [idtac | apply (step_sameExec r1); auto]. -unfold sameExec; unfold sameExec in HrecH |-; intros. -rewrite H2; auto. -rewrite HrecH; auto. -apply (step_inv r1); auto. -intros x H5; apply H4. -generalize H5; (repeat rewrite getdst_app); intros; apply in_or_app. -elim - (in_app_or - (getdst (StateToMove r2) ++ getdst (StateBeing r2)) - (getdst (StateToMove r3) ++ getdst (StateBeing r3)) x); auto; intro. -generalize (step_inv_getdst r1 r2 x); (repeat rewrite getdst_app); intro. -left; apply H8; auto. -intros x H5; apply H4. -generalize H5; (repeat rewrite getdst_app); intros; apply in_or_app. -elim - (in_app_or - (getdst (StateToMove r1) ++ getdst (StateBeing r1)) - (getdst (StateToMove r2) ++ getdst (StateBeing r2)) x); auto; intro. -generalize (step_inv_getdst r1 r2 x); (repeat rewrite getdst_app); intro. -left; apply H8; auto. + +Lemma parmove_prop_1: + forall srcs dsts, + List.length srcs = List.length dsts -> + Loc.norepet dsts -> + Loc.disjoint srcs temporaries -> + Loc.disjoint dsts temporaries -> + forall e, + let e' := exec_seq (parmove srcs dsts) e in + List.map e' dsts = List.map e srcs /\ + forall l, ~In l dsts -> l <> R IT2 -> l <> R FT2 -> e' l = e l. +Proof. + intros. + assert (NR: list_norepet dsts) by (apply loc_norepet_norepet; auto). + assert (NTS: forall r, In r srcs -> Parmov.is_not_temp loc temp_for r). + intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with srcs; auto. + assert (NTD: forall r, In r dsts -> Parmov.is_not_temp loc temp_for r). + intros. apply disjoint_temp_not_temp. apply Loc.disjoint_notin with dsts; auto. + generalize (Parmov.parmove2_correctness loc temp_for val Loc.eq srcs dsts H NR NTS NTD e). + change (Parmov.exec_seq loc val Loc.eq (Parmov.parmove2 loc temp_for Loc.eq srcs dsts) e) with e'. + intros [A B]. + split. auto. intros. apply B. auto. rewrite is_not_temp_charact; auto. Qed. - -Inductive dstep : State -> State -> Prop := - dstep_nop: - forall (r : Reg) (t l : Moves), dstep ((r, r) :: t, nil, l) (t, nil, l) - | dstep_start: - forall (t l : Moves) (s d : Reg), - s <> d -> dstep ((s, d) :: t, nil, l) (t, (s, d) :: nil, l) - | dstep_push: - forall (t1 t2 b l : Moves) (s d r : Reg), - noRead t1 d -> - dstep - (t1 ++ ((d, r) :: t2), (s, d) :: b, l) - (t1 ++ t2, (d, r) :: ((s, d) :: b), l) - | dstep_pop_loop: - forall (t b l : Moves) (s d r0 : Reg), - noRead t r0 -> - dstep - (t, (s, r0) :: (b ++ ((r0, d) :: nil)), l) - (t, b ++ ((T r0, d) :: nil), (s, r0) :: ((r0, T r0) :: l)) - | dstep_pop: - forall (t b l : Moves) (s0 d0 sn dn : Reg), - noRead t dn -> - Loc.diff dn s0 -> - dstep - (t, (sn, dn) :: (b ++ ((s0, d0) :: nil)), l) - (t, b ++ ((s0, d0) :: nil), (sn, dn) :: l) - | dstep_last: - forall (t l : Moves) (s d : Reg), - noRead t d -> dstep (t, (s, d) :: nil, l) (t, nil, (s, d) :: l) . -Hint Resolve dstep_nop dstep_start dstep_push . -Hint Resolve dstep_pop_loop dstep_pop dstep_last . - -Lemma dstep_step: - forall (r1 r2 : State), dstep r1 r2 -> stepInv r1 -> stepp r1 r2. -Proof. -intros r1 r2 DS; inversion_clear DS; intros SI; eauto. -change (stepp (nil ++ ((r, r) :: t), nil, l) (t, nil, l)); apply step_stepp; - apply (step_nop r nil t). -change (stepp (nil ++ ((s, d) :: t), nil, l) (t, (s, d) :: nil, l)); - apply step_stepp; apply (step_start nil t l). -apply - (stepp_trans - (t, (s, r0) :: (b ++ ((r0, d) :: nil)), l) - (t, (s, r0) :: (b ++ ((T r0, d) :: nil)), (r0, T r0) :: l) - (t, b ++ ((T r0, d) :: nil), (s, r0) :: ((r0, T r0) :: l))); auto. -apply step_stepp; apply step_pop; auto. -unfold stepInv in SI |-; generalize SI; intros [X [Y [Z [U V]]]]. -generalize V; unfold StateBeing, noTmpLast. -case (b ++ ((r0, d) :: nil)); auto. -intros m l0 [R1 [OK PP]]; auto. + +Lemma parmove_prop_2: + forall srcs dsts s d, + In (s, d) (parmove srcs dsts) -> + (In s srcs \/ s = R IT2 \/ s = R FT2) + /\ (In d dsts \/ d = R IT2 \/ d = R FT2). +Proof. + intros srcs dsts. + set (mu := List.combine srcs dsts). + assert (forall s d, Parmov.wf_move loc temp_for mu s d -> + (In s srcs \/ s = R IT2 \/ s = R FT2) + /\ (In d dsts \/ d = R IT2 \/ d = R FT2)). + unfold mu; induction 1. + split. + left. eapply List.in_combine_l; eauto. + left. eapply List.in_combine_r; eauto. + split. + right. apply temp_for_charact. + tauto. + split. + tauto. + right. apply temp_for_charact. + intros. apply H. + apply (Parmov.parmove2_wf_moves loc temp_for Loc.eq srcs dsts s d H0). Qed. - -Lemma dstep_inv: - forall (r1 r2 : State), dstep r1 r2 -> stepInv r1 -> stepInv r2. + +Lemma loc_type_temp_for: + forall l, Loc.type (temp_for l) = Loc.type l. Proof. -intros. -apply (stepp_inv r1 r2); auto. -apply dstep_step; auto. + intros; unfold temp_for. destruct (Loc.type l); reflexivity. Qed. - -Inductive dstepp : State -> State -> Prop := - dstepp_refl: forall (r : State), dstepp r r - | dstepp_trans: - forall (r1 r2 r3 : State), dstep r1 r2 -> dstepp r2 r3 -> dstepp r1 r3 . -Hint Resolve dstepp_refl dstepp_trans . - -Lemma dstepp_stepp: - forall (s1 s2 : State), stepInv s1 -> dstepp s1 s2 -> stepp s1 s2. -Proof. -intros; induction H0 as [r|r1 r2 r3 H0 H1 HrecH0]; auto. -apply (stepp_transitive r1 r2 r3); auto. -apply dstep_step; auto. -apply HrecH0; auto. -apply (dstep_inv r1 r2); auto. + +Lemma loc_type_combine: + forall srcs dsts, + List.map Loc.type srcs = List.map Loc.type dsts -> + forall s d, + In (s, d) (List.combine srcs dsts) -> + Loc.type s = Loc.type d. +Proof. + induction srcs; destruct dsts; simpl; intros; try discriminate. + elim H0. + elim H0; intros. inversion H1; subst. congruence. + apply IHsrcs with dsts. congruence. auto. Qed. - -Lemma dstepp_sameExec: - forall (r1 r2 : State), dstepp r1 r2 -> stepInv r1 -> sameExec r1 r2. -Proof. -intros; apply stepp_sameExec; auto. -apply dstepp_stepp; auto. + +Lemma parmove_prop_3: + forall srcs dsts, + List.map Loc.type srcs = List.map Loc.type dsts -> + forall s d, + In (s, d) (parmove srcs dsts) -> Loc.type s = Loc.type d. +Proof. + intros srcs dsts TYP. + set (mu := List.combine srcs dsts). + assert (forall s d, Parmov.wf_move loc temp_for mu s d -> + Loc.type s = Loc.type d). + unfold mu; induction 1. + eapply loc_type_combine; eauto. + rewrite loc_type_temp_for; auto. + rewrite loc_type_temp_for; auto. + intros. apply H. + apply (Parmov.parmove2_wf_moves loc temp_for Loc.eq srcs dsts s d H0). Qed. - -End pmov. -Fixpoint split_move' (m : Moves) (r : Reg) {struct m} : - option ((Moves * Reg) * Moves) := - match m with - (s, d) :: tail => - match diff_dec s r with - right _ => Some (nil, d, tail) - | left _ => - match split_move' tail r with - Some ((t1, r2, t2)) => Some ((s, d) :: t1, r2, t2) - | None => None - end - end - | nil => None - end. - -Fixpoint split_move (m : Moves) (r : Reg) {struct m} : - option ((Moves * Reg) * Moves) := - match m with - (s, d) :: tail => - match Loc.eq s r with - left _ => Some (nil, d, tail) - | right _ => - match split_move tail r with - Some ((t1, r2, t2)) => Some ((s, d) :: t1, r2, t2) - | None => None - end - end - | nil => None - end. +Section EQUIVALENCE. -Definition def : Move := (R IT1, R IT1). - -Fixpoint last (M : Moves) : Move := - match M with nil => def - | m :: nil => m - | m :: tail => last tail end. - -Fixpoint head_but_last (M : Moves) : Moves := - match M with - nil => nil - | m' :: nil => nil - | m' :: tail => m' :: head_but_last tail - end. - -Fixpoint replace_last_s (M : Moves) : Moves := - match M with - nil => nil - | m :: nil => - match m with (s, d) => (T s, d) :: nil end - | m :: tail => m :: replace_last_s tail - end. - -Ltac CaseEq name := generalize (refl_equal name); pattern name at -1; case name. - -Definition stepf' (S1 : State) : State := - match S1 with - (nil, nil, _) => S1 - | ((s, d) :: tl, nil, l) => - match diff_dec s d with - right _ => (tl, nil, l) - | left _ => (tl, (s, d) :: nil, l) - end - | (t, (s, d) :: b, l) => - match split_move t d with - Some ((t1, r, t2)) => - (t1 ++ t2, (d, r) :: ((s, d) :: b), l) - | None => - match b with - nil => (t, nil, (s, d) :: l) - | _ => - match diff_dec d (fst (last b)) with - right _ => - (t, replace_last_s b, (s, d) :: ((d, T d) :: l)) - | left _ => (t, b, (s, d) :: l) - end - end - end - end. - -Definition stepf (S1 : State) : State := - match S1 with - (nil, nil, _) => S1 - | ((s, d) :: tl, nil, l) => - match Loc.eq s d with - left _ => (tl, nil, l) - | right _ => (tl, (s, d) :: nil, l) - end - | (t, (s, d) :: b, l) => - match split_move t d with - Some ((t1, r, t2)) => - (t1 ++ t2, (d, r) :: ((s, d) :: b), l) - | None => - match b with - nil => (t, nil, (s, d) :: l) - | _ => - match Loc.eq d (fst (last b)) with - left _ => - (t, replace_last_s b, (s, d) :: ((d, T d) :: l)) - | right _ => (t, b, (s, d) :: l) - end - end - end - end. - -Lemma rebuild_l: - forall (l : Moves) (m : Move), - m :: l = head_but_last (m :: l) ++ (last (m :: l) :: nil). -Proof. -induction l; simpl; auto. -intros m; rewrite (IHl a); auto. -Qed. - -Lemma splitSome: - forall (l t1 t2 : Moves) (s d r : Reg), - noOverlap (l ++ ((r, s) :: nil)) -> - split_move l s = Some (t1, d, t2) -> noRead t1 s. -Proof. -induction l; simpl. -intros; discriminate. -destruct a as [a1 a2]. -intros t1 t2 s d r Hno; case (Loc.eq a1 s). -intros e H1; inversion H1. -simpl; auto. -CaseEq (split_move l s). -intros; (repeat destruct p). -inversion H0; auto. -simpl; split; auto. -change (noOverlap (((a1, a2) :: l) ++ ((r, s) :: nil))) in Hno |-. -assert (noOverlap ((r, s) :: ((a1, a2) :: l))). -apply noOverlap_Front0; auto. -unfold noOverlap in H1 |-; simpl in H1 |-. -elim H1 with ( l0 := a1 ); - [intros H5 H6; (try clear H1); (try exact H5) | idtac]. -elim H5; [intros H1; (try clear H5); (try exact H1) | intros H1; (try clear H5)]. -absurd (a1 = s); auto. -apply Loc.diff_sym; auto. -right; left; trivial. -apply (IHl m0 m s r0 r); auto. -apply (noOverlap_pop (a1, a2)); auto. -intros; discriminate. -Qed. - -Lemma unsplit_move: - forall (l t1 t2 : Moves) (s d r : Reg), - noOverlap (l ++ ((r, s) :: nil)) -> - split_move l s = Some (t1, d, t2) -> l = t1 ++ ((s, d) :: t2). -Proof. -induction l. -simpl; intros; discriminate. -intros t1 t2 s d r HnoO; destruct a as [a1 a2]; simpl; case (diff_dec a1 s); - intro. -case (Loc.eq a1 s); intro. -absurd (Loc.diff a1 s); auto. -rewrite e; apply Loc.same_not_diff. -CaseEq (split_move l s); intros; (try discriminate). -(repeat destruct p); inversion H0. -rewrite app_cons; subst t2; subst d; rewrite (IHl m0 m s r0 r); auto. -apply (noOverlap_pop (a1, a2)); auto. -case (Loc.eq a1 s); intros e H; inversion H; simpl. -rewrite e; auto. -cut (noOverlap_aux a1 (getdst ((r, s) :: nil))). -intros [[H5|H4] H0]; [try exact H5 | idtac]. -absurd (s = a1); auto. -absurd (Loc.diff a1 s); auto; apply Loc.diff_sym; auto. -generalize HnoO; rewrite app_cons; intro. -assert (noOverlap (l ++ ((a1, a2) :: ((r, s) :: nil)))); - (try (apply noOverlap_insert; assumption)). -assert (noOverlap ((a1, a2) :: ((r, s) :: nil))). -apply (noOverlap_right l); auto. -generalize H2; unfold noOverlap; simpl. -intros H5; elim (H5 a1); [idtac | left; trivial]. -intros H6 [[H7|H8] H9]. -absurd (s = a1); auto. -split; [right; (try assumption) | auto]. -Qed. - -Lemma cons_replace: - forall (a : Move) (l : Moves), - l <> nil -> replace_last_s (a :: l) = a :: replace_last_s l. -Proof. -intros; simpl. -CaseEq l. -intro; contradiction. -intros m l0 H0; auto. -Qed. - -Lemma last_replace: - forall (l : Moves) (s d : Reg), - replace_last_s (l ++ ((s, d) :: nil)) = l ++ ((T s, d) :: nil). -Proof. -induction l; (try (simpl; auto; fail)). -intros; (repeat rewrite <- app_comm_cons). -rewrite cons_replace. -rewrite IHl; auto. -red; intro. -elim (app_eq_nil l ((s, d) :: nil)); auto; intros; discriminate. -Qed. - -Lemma last_app: forall (l : Moves) (m : Move), last (l ++ (m :: nil)) = m. -Proof. -induction l; simpl; auto. -intros m; CaseEq (l ++ (m :: nil)). -intro; elim (app_eq_nil l (m :: nil)); auto; intros; discriminate. -intros m0 l0 H; (rewrite <- H; apply IHl). -Qed. - -Lemma last_cons: - forall (l : Moves) (m m0 : Move), last (m0 :: (m :: l)) = last (m :: l). -Proof. -intros; simpl; auto. -Qed. - -Lemma stepf_popLoop: - forall (t b l : Moves) (s d r0 : Reg), - split_move t d = None -> - stepf (t, (s, d) :: (b ++ ((d, r0) :: nil)), l) = - (t, b ++ ((T d, r0) :: nil), (s, d) :: ((d, T d) :: l)). -Proof. -intros; simpl; rewrite H; CaseEq (b ++ ((d, r0) :: nil)); intros. -destruct b; discriminate. -rewrite <- H0; rewrite last_app; simpl; rewrite last_replace. -case (Loc.eq d d); intro; intuition. -destruct t; (try destruct m0); simpl; auto. -Qed. - -Lemma stepf_pop: - forall (t b l : Moves) (s d r r0 : Reg), - split_move t d = None -> - d <> r -> - stepf (t, (s, d) :: (b ++ ((r, r0) :: nil)), l) = - (t, b ++ ((r, r0) :: nil), (s, d) :: l). -Proof. -intros; simpl; rewrite H; CaseEq (b ++ ((r, r0) :: nil)); intros. -destruct b; discriminate. -rewrite <- H1; rewrite last_app; simpl. -case (Loc.eq d r); intro. -absurd (d = r); auto. -destruct t; (try destruct m0); simpl; auto. -Qed. - -Lemma noOverlap_head: - forall l1 l2 m, noOverlap (l1 ++ (m :: l2)) -> noOverlap (l1 ++ (m :: nil)). -Proof. -induction l2; simpl; auto. -intros; apply IHl2. -cut (l1 ++ (m :: (a :: l2)) = (l1 ++ (m :: nil)) ++ (a :: l2)); - [idtac | rewrite app_ass; auto]. -intros e; rewrite e in H. -cut (l1 ++ (m :: l2) = (l1 ++ (m :: nil)) ++ l2); - [idtac | rewrite app_ass; auto]. -intros e'; rewrite e'; auto. -apply noOverlap_Pop with a; auto. -Qed. - -Lemma splitNone: - forall (l : Moves) (s d : Reg), - split_move l d = None -> noOverlap (l ++ ((s, d) :: nil)) -> noRead l d. -Proof. -induction l; intros s d; simpl; auto. -destruct a as [a1 a2]; case (Loc.eq a1 d); intro; (try (intro; discriminate)). -CaseEq (split_move l d); intros. -(repeat destruct p); discriminate. -split; (try assumption). -change (noOverlap (((a1, a2) :: l) ++ ((s, d) :: nil))) in H1 |-. -assert (noOverlap ((s, d) :: ((a1, a2) :: l))). -apply noOverlap_Front0; auto. -assert (noOverlap ((a1, a2) :: ((s, d) :: l))). -apply noOverlap_swap; auto. -unfold noOverlap in H3 |-; simpl in H3 |-. -elim H3 with ( l0 := a1 ); - [intros H5 H6; (try clear H1); (try exact H5) | idtac]. -elim H6; - [intros H1 H4; elim H1; - [intros H7; (try clear H1 H6); (try exact H7) | intros H7; (try clear H1 H6)]]. -absurd (a1 = d); auto. -apply Loc.diff_sym; auto. -left; trivial. -apply IHl with s; auto. -apply noOverlap_pop with (a1, a2); auto. -Qed. - -Lemma noO_diff: - forall l1 l2 s d r r0, - noOverlap (l1 ++ ((s, d) :: (l2 ++ ((r, r0) :: nil)))) -> - r = d \/ Loc.diff d r. -Proof. -intros. -assert (noOverlap ((s, d) :: (l2 ++ ((r, r0) :: nil)))); auto. -apply (noOverlap_right l1); auto. -assert (noOverlap ((l2 ++ ((r, r0) :: nil)) ++ ((s, d) :: nil))); auto. -apply (noOverlap_movBack0 (l2 ++ ((r, r0) :: nil))); auto. -assert - ((l2 ++ ((r, r0) :: nil)) ++ ((s, d) :: nil) = - l2 ++ (((r, r0) :: nil) ++ ((s, d) :: nil))); auto. -rewrite app_ass; auto. -rewrite H2 in H1. -simpl in H1 |-. -assert (noOverlap ((r, r0) :: ((s, d) :: nil))); auto. -apply (noOverlap_right l2); auto. -unfold noOverlap in H3 |-. -generalize (H3 r); simpl. -intros H4; elim H4; intros; [idtac | left; trivial]. -elim H6; intros [H9|H9] H10; [left | right]; auto. -Qed. - -Lemma f2ind: - forall (S1 S2 : State), - (forall (l : Moves), (S1 <> (nil, nil, l))) -> - noOverlap (StateToMove S1 ++ StateBeing S1) -> stepf S1 = S2 -> dstep S1 S2. -Proof. -intros S1 S2 Hneq HnoO; destruct S1 as [[t b] l]; destruct b. -destruct t. -elim (Hneq l); auto. -destruct m; simpl; case (Loc.eq r r0). -intros. -rewrite e; rewrite <- H; apply dstep_nop. -intros n H; rewrite <- H; generalize (dstep_start t l r r0); auto. -intros H; rewrite <- H; destruct m as [s d]. -CaseEq (split_move t d). -intros p H0; destruct p as [[t1 s0] t2]; simpl; rewrite H0; destruct t; simpl. -simpl in H0 |-; discriminate. -rewrite (unsplit_move (m :: t) t1 t2 d s0 s); auto. -destruct m; generalize dstep_push; intros H1; apply H1. -unfold StateToMove, StateBeing in HnoO |-. -apply (splitSome ((r, r0) :: t) t1 t2 d s0 s); auto. -apply noOverlap_head with b; auto. -unfold StateToMove, StateBeing in HnoO |-. -apply noOverlap_head with b; auto. -intros H0; destruct b. -simpl. -rewrite H0. -destruct t; (try destruct m); generalize dstep_last; intros H1; apply H1. -simpl; auto. -unfold StateToMove, StateBeing in HnoO |-. -apply splitNone with s; auto. -unfold StateToMove, StateBeing in HnoO |-. -generalize HnoO; clear HnoO; rewrite (rebuild_l b m); intros HnoO. -destruct (last (m :: b)). -case (Loc.eq d r). -intros e; rewrite <- e. -CaseEq (head_but_last (m :: b)); intros; [simpl | idtac]; - (try - (destruct t; (try destruct m0); rewrite H0; - (case (Loc.eq d d); intros h; (try (elim h; auto))))). -generalize (dstep_pop_loop nil nil); simpl; intros H3; apply H3; auto. -generalize (dstep_pop_loop ((r1, r2) :: t) nil); unfold T; simpl app; - intros H3; apply H3; clear H3; apply splitNone with s; (try assumption). -apply noOverlap_head with (head_but_last (m :: b) ++ ((r, r0) :: nil)); auto. -rewrite stepf_popLoop; auto. -generalize (dstep_pop_loop t (m0 :: l0)); simpl; intros H3; apply H3; clear H3; - apply splitNone with s; (try assumption). -apply noOverlap_head with (head_but_last (m :: b) ++ ((r, r0) :: nil)); auto. -intro; assert (Loc.diff d r). -assert (r = d \/ Loc.diff d r). -apply (noO_diff t (head_but_last (m :: b)) s d r r0); auto. -elim H1; [intros H2; absurd (d = r); auto | intros H2; auto]. -rewrite stepf_pop; auto. -generalize (dstep_pop t (head_but_last (m :: b))); intros H3; apply H3; auto. -clear H3; apply splitNone with s; (try assumption). -apply noOverlap_head with (head_but_last (m :: b) ++ ((r, r0) :: nil)); auto. -Qed. - -Lemma f2ind': - forall (S1 : State), - (forall (l : Moves), (S1 <> (nil, nil, l))) -> - noOverlap (StateToMove S1 ++ StateBeing S1) -> dstep S1 (stepf S1). -Proof. -intros S1 H noO; apply f2ind; auto. -Qed. - -Lemma appcons_length: - forall (l1 l2 : Moves) (m : Move), - length (l1 ++ (m :: l2)) = (length (l1 ++ l2) + 1%nat)%nat. -Proof. -induction l1; simpl; intros; [omega | idtac]. -rewrite IHl1; omega. -Qed. - -Definition mesure (S0 : State) : nat := - let (p, _) := S0 in let (t, b) := p in (2 * length t + length b)%nat. - -Lemma step_dec0: - forall (t1 t2 b1 b2 : Moves) (l1 l2 : Moves), - dstep (t1, b1, l1) (t2, b2, l2) -> - (2 * length t2 + length b2 < 2 * length t1 + length b1)%nat. -Proof. -intros t1 t2 b1 b2 l1 l2 H; inversion H; simpl; (try omega). -rewrite appcons_length; omega. -cut (length (b ++ ((T r0, d) :: nil)) = length (b ++ ((r0, d) :: nil))); - (try omega). -induction b; simpl; auto. -(repeat rewrite appcons_length); auto. -Qed. - -Lemma step_dec: - forall (S1 S2 : State), dstep S1 S2 -> (mesure S2 < mesure S1)%nat. -Proof. -unfold mesure; destruct S1 as [[t1 b1] l1]; destruct S2 as [[t2 b2] l2]. -intro; apply (step_dec0 t1 t2 b1 b2 l1 l2); trivial. -Qed. - -Lemma stepf_dec0: - forall (S1 S2 : State), - (forall (l : Moves), (S1 <> (nil, nil, l))) /\ - (S2 = stepf S1 /\ noOverlap (StateToMove S1 ++ StateBeing S1)) -> - (mesure S2 < mesure S1)%nat. -Proof. -intros S1 S2 [H1 [H2 H3]]; apply step_dec. -apply f2ind; trivial. -rewrite H2; reflexivity. -Qed. - -Lemma stepf_dec: - forall (S1 S2 : State), - S2 = stepf S1 /\ - ((forall (l : Moves), (S1 <> (nil, nil, l))) /\ - noOverlap (StateToMove S1 ++ StateBeing S1)) -> ltof _ mesure S2 S1. -Proof. -unfold ltof. -intros S1 S2 [H1 [H2 H3]]; apply step_dec. -apply f2ind; trivial. -rewrite H1; reflexivity. -Qed. - -Lemma replace_last_id: - forall l m m0, replace_last_s (m :: (m0 :: l)) = m :: replace_last_s (m0 :: l). -Proof. -intros; case l; simpl. -destruct m0; simpl; auto. -intros; case l0; auto. -Qed. - -Lemma length_replace: forall l, length (replace_last_s l) = length l. -Proof. -induction l; simpl; auto. -destruct l; destruct a; simpl; auto. -Qed. - -Lemma length_app: - forall (A : Set) (l1 l2 : list A), - (length (l1 ++ l2) = length l1 + length l2)%nat. -Proof. -intros A l1 l2; (try assumption). -induction l1; simpl; auto. -Qed. - -Lemma split_length: - forall (l t1 t2 : Moves) (s d : Reg), - split_move l s = Some (t1, d, t2) -> - (length l = (length t1 + length t2) + 1)%nat. -Proof. -induction l. -intros; discriminate. -intros t1 t2 s d; destruct a as [r r0]; simpl; case (Loc.eq r s); intro. -intros H; inversion H. -simpl; omega. -CaseEq (split_move l s); (try (intros; discriminate)). -(repeat destruct p); intros H H0; inversion H0. -rewrite H2; rewrite (IHl m0 m s r1); auto. -rewrite H4; rewrite <- H2; simpl; omega. -Qed. - -Lemma stepf_dec0': - forall (S1 : State), - (forall (l : Moves), (S1 <> (nil, nil, l))) -> - (mesure (stepf S1) < mesure S1)%nat. -Proof. -intros S1 H. -unfold mesure; destruct S1 as [[t1 b1] l1]. -destruct t1. -destruct b1. -generalize (H l1); intros H1; elim H1; auto. -destruct m; simpl. -destruct b1. -simpl; auto. -case (Loc.eq r0 (fst (last (m :: b1)))). -intros; rewrite length_replace; simpl; omega. -simpl; case b1; intros; simpl; omega. -destruct m. -destruct b1. -simpl. -case (Loc.eq r r0); intros; simpl; omega. -destruct m; simpl; case (Loc.eq r r2). -intros; simpl; omega. -CaseEq (split_move t1 r2); intros. -destruct p; destruct p; simpl. -rewrite (split_length t1 m0 m r2 r3); auto. -rewrite length_app; auto. -omega. -destruct b1. -simpl; omega. -case (Loc.eq r2 (fst (last (m :: b1)))); intros. -rewrite length_replace; simpl; omega. -simpl; omega. -Qed. - -Lemma stepf1_dec: - forall (S1 S2 : State), - (forall (l : Moves), (S1 <> (nil, nil, l))) -> - S2 = stepf S1 -> ltof _ mesure S2 S1. -Proof. -unfold ltof; intros S1 S2 H H0; rewrite H0. -apply stepf_dec0'; (try assumption). -Qed. - -Lemma disc1: - forall (a : Move) (l1 l2 l3 l4 : list Move), - ((a :: l1, l2, l3) <> (nil, nil, l4)). -Proof. -intros; discriminate. -Qed. - -Lemma disc2: - forall (a : Move) (l1 l2 l3 l4 : list Move), - ((l1, a :: l2, l3) <> (nil, nil, l4)). -Proof. -intros; discriminate. -Qed. -Hint Resolve disc1 disc2 . - -Lemma sameExec_reflexive: forall (r : State), sameExec r r. -Proof. -intros r; unfold sameExec, sameEnv, exec. -destruct r as [[t b] d]; trivial. -Qed. - -Definition base_case_Pmov_dec: - forall (s : State), - ({ exists l : list Move , s = (nil, nil, l) }) + - ({ forall l, (s <> (nil, nil, l)) }). -Proof. -destruct s as [[[|x tl] [|y tl']] l]; (try (right; intro; discriminate)). -left; exists l; auto. -Defined. - -Definition Pmov := - Fix - (well_founded_ltof _ mesure) (fun _ => State) - (fun (S1 : State) => - fun (Pmov : forall x, ltof _ mesure x S1 -> State) => - match base_case_Pmov_dec S1 with - left h => S1 - | right h => Pmov (stepf S1) (stepf_dec0' S1 h) end). - -Theorem Pmov_equation: forall S1, Pmov S1 = match S1 with - ((nil, nil), _) => S1 - | _ => Pmov (stepf S1) - end. -Proof. -intros S1; unfold Pmov at 1; - rewrite (Fix_eq - (well_founded_ltof _ mesure) (fun _ => State) - (fun (S1 : State) => - fun (Pmov : forall x, ltof _ mesure x S1 -> State) => - match base_case_Pmov_dec S1 with - left h => S1 - | right h => Pmov (stepf S1) (stepf_dec0' S1 h) end)). -fold Pmov. -destruct S1 as [[[|x tl] [|y tl']] l]; - match goal with - | |- match ?a with left _ => _ | right _ => _ end = _ => case a end; - (try (intros [l0 Heq]; discriminate Heq)); auto. -intros H; elim (H l); auto. -intros x f g Hfg_ext. -match goal with -| |- match ?a with left _ => _ | right _ => _ end = _ => case a end; auto. -Qed. - -Lemma sameExec_transitive: - forall (r1 r2 r3 : State), - (forall r, - In r (getdst (StateToMove r2 ++ StateBeing r2)) -> - In r (getdst (StateToMove r1 ++ StateBeing r1))) -> - (forall r, - In r (getdst (StateToMove r3 ++ StateBeing r3)) -> - In r (getdst (StateToMove r2 ++ StateBeing r2))) -> - sameExec r1 r2 -> sameExec r2 r3 -> sameExec r1 r3. -Proof. -intros r1 r2 r3; unfold sameExec, exec; (repeat rewrite getdst_app). -destruct r1 as [[t1 b1] d1]; destruct r2 as [[t2 b2] d2]; - destruct r3 as [[t3 b3] d3]; simpl. -intros Hin; intros. -rewrite H0; auto. -rewrite H1; auto. -intros. -apply (H3 x). -apply in_or_app; auto. -elim (in_app_or (getdst t2 ++ getdst b2) (getdst t3 ++ getdst b3) x); auto. -intros. -apply (H3 x). -apply in_or_app; auto. -elim (in_app_or (getdst t1 ++ getdst b1) (getdst t2 ++ getdst b2) x); auto. -Qed. - -Lemma dstep_inv_getdst: - forall (s1 s2 : State) r, - dstep s1 s2 -> - In r (getdst (StateToMove s2 ++ StateBeing s2)) -> - In r (getdst (StateToMove s1 ++ StateBeing s1)). -intros s1 s2 r STEP; inversion_clear STEP; - unfold StateToMove, StateBeing, StateDone; (repeat rewrite app_nil); - (repeat (rewrite getdst_app; simpl)); intro; auto. -Proof. -right; (try assumption). -elim (in_app_or (getdst t) (d :: nil) r); auto; (simpl; intros [H1|H1]); - [left; assumption | inversion H1]. -elim (in_app_or (getdst t1 ++ getdst t2) (r0 :: (d :: getdst b)) r); auto; - (simpl; intros). -elim (in_app_or (getdst t1) (getdst t2) r); auto; (simpl; intros). -apply in_or_app; left; apply in_or_app; left; assumption. -apply in_or_app; left; apply in_or_app; right; simpl; right; assumption. -elim H1; [intros H2 | intros [H2|H2]]. -apply in_or_app; left; apply in_or_app; right; simpl; left; auto. -apply in_or_app; right; simpl; left; auto. -apply in_or_app; right; simpl; right; assumption. -elim (in_app_or (getdst t) (getdst b ++ (d :: nil)) r); auto; (simpl; intros). -apply in_or_app; left; assumption. -elim (in_app_or (getdst b) (d :: nil) r); auto; (simpl; intros). -apply in_or_app; right; simpl; right; apply in_or_app; left; assumption. -elim H2; [intros H3 | intros H3; inversion H3]. -apply in_or_app; right; simpl; right; apply in_or_app; right; simpl; auto. -elim (in_app_or (getdst t) (getdst b ++ (d0 :: nil)) r); auto; (simpl; intros). -apply in_or_app; left; assumption. -elim (in_app_or (getdst b) (d0 :: nil) r); auto; simpl; - [intros H3 | intros [H3|H3]; [idtac | inversion H3]]. -apply in_or_app; right; simpl; right; apply in_or_app; left; assumption. -apply in_or_app; right; simpl; right; apply in_or_app; right; simpl; auto. -apply in_or_app; left; assumption. -Qed. - -Theorem STM_Pmov: forall (S1 : State), StateToMove (Pmov S1) = nil. -Proof. -intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). -clear S1; intros S1; intros Hrec; destruct S1 as [[t b] d]; - rewrite Pmov_equation; destruct t. -destruct b; auto. -apply Hrec; apply stepf1_dec; auto. -apply Hrec; apply stepf1_dec; auto. -Qed. - -Theorem SB_Pmov: forall (S1 : State), StateBeing (Pmov S1) = nil. -Proof. -intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). -clear S1; intros S1; intros Hrec; destruct S1 as [[t b] d]; - rewrite Pmov_equation; destruct t. -destruct b; auto. -apply Hrec; apply stepf1_dec; auto. -apply Hrec; apply stepf1_dec; auto. -Qed. - -Theorem Fpmov_correct: - forall (S1 : State), stepInv S1 -> sameExec S1 (Pmov S1). -Proof. -intros S1; elim S1 using (well_founded_ind (Wf_nat.well_founded_ltof _ mesure)). -clear S1; intros S1; intros Hrec Hinv; rewrite Pmov_equation; - destruct S1 as [[t b] d]. -assert - (forall (r : Reg) S1, - In r (getdst (StateToMove (Pmov (stepf S1)) ++ StateBeing (Pmov (stepf S1)))) -> - In r (getdst (StateToMove (stepf S1) ++ StateBeing (stepf S1)))). -intros r S1; rewrite (STM_Pmov (stepf S1)); rewrite SB_Pmov; simpl; intros. -inversion H. -destruct t. -destruct b. -apply sameExec_reflexive. -set (S1:=(nil (A:=Move), m :: b, d)). -assert (dstep S1 (stepf S1)); (try apply f2ind); unfold S1; auto. -elim Hinv; intros Hpath [SD [NO NT]]; assumption. -apply sameExec_transitive with (stepf S1); auto. -intros r; apply dstep_inv_getdst; auto. -apply dstepp_sameExec; auto; apply dstepp_trans with (stepf S1); auto. -apply dstepp_refl; auto. -apply Hrec; auto. -unfold ltof; apply step_dec; assumption. -apply (dstep_inv S1); assumption. -set (S1:=(m :: t, b, d)). -assert (dstep S1 (stepf S1)); (try apply f2ind); unfold S1; auto. -elim Hinv; intros Hpath [SD [NO NT]]; assumption. -apply sameExec_transitive with (stepf S1); auto. -intros r; apply dstep_inv_getdst; auto. -apply dstepp_sameExec; auto; apply dstepp_trans with (stepf S1); auto. -apply dstepp_refl; auto. -apply Hrec; auto. -unfold ltof; apply step_dec; assumption. -apply (dstep_inv S1); assumption. -Qed. - -Definition P_move := fun (p : Moves) => StateDone (Pmov (p, nil, nil)). - -Definition Sexec := sexec. - -Definition Get := get. - -Fixpoint listsLoc2Moves (src dst : list loc) {struct src} : Moves := - match src with - nil => nil - | s :: srcs => - match dst with - nil => nil - | d :: dsts => (s, d) :: listsLoc2Moves srcs dsts - end - end. - -Definition no_overlap (l1 l2 : list loc) := - forall r, In r l1 -> forall s, In s l2 -> r = s \/ Loc.diff r s. - -Definition no_overlap_state (S : State) := - no_overlap - (getsrc (StateToMove S ++ StateBeing S)) - (getdst (StateToMove S ++ StateBeing S)). - -Definition no_overlap_list := fun l => no_overlap (getsrc l) (getdst l). - -Lemma Indst_noOverlap_aux: - forall l1 l, - (forall (s : Reg), In s (getdst l1) -> l = s \/ Loc.diff l s) -> - noOverlap_aux l (getdst l1). -Proof. -intros; induction l1; simpl; auto. -destruct a as [a1 a2]; simpl; split. -elim (H a2); (try intros H0). -left; auto. -right; apply Loc.diff_sym; auto. -simpl; left; trivial. -apply IHl1; intros. -apply H; simpl; right; (try assumption). -Qed. - -Lemma no_overlap_noOverlap: - forall r, no_overlap_state r -> noOverlap (StateToMove r ++ StateBeing r). -Proof. -intros r; unfold noOverlap, no_overlap_state. -set (l1:=StateToMove r ++ StateBeing r). -unfold no_overlap; intros H l H0. -apply Indst_noOverlap_aux; intros; apply H; auto. -Qed. - -Theorem Fpmov_correctMoves: - forall p e r, - simpleDest p -> - no_overlap_list p -> - noTmp p -> - notemporary r -> - (forall (x : Reg), In x (getdst p) -> r = x \/ Loc.diff r x) -> - get (pexec p e) r = get (sexec (StateDone (Pmov (p, nil, nil))) e) r. -Proof. -intros p e r SD no_O notmp notempo. -generalize (Fpmov_correct (p, nil, nil)); unfold sameExec, exec; simpl; - rewrite SB_Pmov; rewrite STM_Pmov; simpl. -(repeat rewrite app_nil); intro. -apply H; auto. -unfold stepInv; simpl; (repeat split); (try (rewrite app_nil; assumption)); auto. -generalize (no_overlap_noOverlap (p, nil, nil)); simpl; intros; auto. -apply H0; auto; unfold no_overlap_list in H0 |-. -unfold no_overlap_state; simpl; (repeat rewrite app_nil); auto. -Qed. - -Theorem Fpmov_correct1: - forall (p : Moves) (e : Env) (r : Reg), - simpleDest p -> - no_overlap_list p -> - noTmp p -> - notemporary r -> - (forall (x : Reg), In x (getdst p) -> r = x \/ Loc.diff r x) -> - noWrite p r -> get e r = get (sexec (StateDone (Pmov (p, nil, nil))) e) r. -Proof. -intros p e r Hsd Hno_O HnoTmp Hrnotempo Hrno_Overlap Hnw. -rewrite <- (Fpmov_correctMoves p e); (try assumption). -destruct p; auto. -destruct m as [m1 m2]; simpl; case (Loc.eq m2 r); intros. -elim Hnw; intros; absurd (Loc.diff m2 r); auto. -rewrite e0; apply Loc.same_not_diff. -elim Hnw; intros H1 H2. -rewrite get_update_diff; (try assumption). -apply get_noWrite; (try assumption). -Qed. - -Lemma In_SD_diff: - forall (s d a1 a2 : Reg) (p : Moves), - In (s, d) p -> simpleDest ((a1, a2) :: p) -> Loc.diff a2 d. -Proof. -intros; induction p. -inversion H. -elim H; auto. -intro; subst a; elim H0; intros H1 H2; elim H1; intros; apply Loc.diff_sym; - assumption. -intro; apply IHp; auto. -apply simpleDest_pop2 with a; (try assumption). -Qed. - -Theorem pexec_correct: - forall (e : Env) (m : Move) (p : Moves), - In m p -> simpleDest p -> (let (s, d) := m in get (pexec p e) d = get e s). -Proof. -induction p; intros. -elim H. -destruct m. -elim (in_inv H); intro. -rewrite H1; simpl; rewrite get_update_id; auto. -destruct a as [a1 a2]; simpl. -rewrite get_update_diff. -apply IHp; auto. -apply (simpleDest_pop (a1, a2)); (try assumption). -apply (In_SD_diff r) with ( p := p ) ( a1 := a1 ); auto. -Qed. - -Lemma In_noTmp_notempo: - forall (s d : Reg) (p : Moves), In (s, d) p -> noTmp p -> notemporary d. -Proof. -intros; unfold notemporary; induction p. -inversion H. -elim H; intro. -subst a; elim H0; intros H1 [H3 H2]; (try assumption). -intro; apply IHp; auto. -destruct a; elim H0; intros _ [H2 H3]; (try assumption). -Qed. - -Lemma In_Indst: forall s d p, In (s, d) p -> In d (getdst p). -Proof. -intros; induction p; auto. -destruct a; simpl. -elim H; intro. -left; inversion H0; trivial. -right; apply IHp; auto. -Qed. - -Lemma In_SD_diff': - forall (d a1 a2 : Reg) (p : Moves), - In d (getdst p) -> simpleDest ((a1, a2) :: p) -> Loc.diff a2 d. -Proof. -intros d a1 a2 p H H0; induction p. -inversion H. -destruct a; elim H. -elim H0; simpl; intros. -subst r0. -elim H1; intros H3 H4; apply Loc.diff_sym; assumption. -intro; apply IHp; (try assumption). -apply simpleDest_pop2 with (r, r0); (try assumption). -Qed. - -Lemma In_SD_no_o: - forall (s d : Reg) (p : Moves), - In (s, d) p -> - simpleDest p -> forall (x : Reg), In x (getdst p) -> d = x \/ Loc.diff d x. -Proof. -intros s d p Hin Hsd; induction p. -inversion Hin. -destruct a as [a1 a2]; elim Hin; intros. -inversion H; subst d; subst s. -elim H0; intros H1; [left | right]; (try assumption). -apply (In_SD_diff' x a1 a2 p); auto. -elim H0. -intro; subst x. -right; apply Loc.diff_sym; apply (In_SD_diff s d a1 a2 p); auto. -intro; apply IHp; auto. -apply (simpleDest_pop (a1, a2)); assumption. -Qed. - -Lemma getdst_map: forall p, getdst p = map (fun x => snd x) p. -Proof. -induction p. -simpl; auto. -destruct a; simpl. -rewrite IHp; auto. +Variables srcs dsts: list loc. +Hypothesis LENGTH: List.length srcs = List.length dsts. +Hypothesis NOREPET: Loc.norepet dsts. +Hypothesis NO_OVERLAP: Loc.no_overlap srcs dsts. +Hypothesis NO_SRCS_TEMP: Loc.disjoint srcs temporaries. +Hypothesis NO_DSTS_TEMP: Loc.disjoint dsts temporaries. + +Definition no_overlap_dests (l: loc) : Prop := + forall d, In d dsts -> l = d \/ Loc.diff l d. + +Lemma dests_no_overlap_dests: + forall l, In l dsts -> no_overlap_dests l. +Proof. + assert (forall d, Loc.norepet d -> + forall l1 l2, In l1 d -> In l2 d -> l1 = l2 \/ Loc.diff l1 l2). + induction 1; simpl; intros. + contradiction. + elim H1; intro; elim H2; intro. + left; congruence. + right. subst l1. eapply Loc.in_notin_diff; eauto. + right. subst l2. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. + eauto. + intros; red; intros. eauto. Qed. - -Lemma getsrc_map: forall p, getsrc p = map (fun x => fst x) p. + +Lemma notin_dests_no_overlap_dests: + forall l, Loc.notin l dsts -> no_overlap_dests l. Proof. -induction p. -simpl; auto. -destruct a; simpl. -rewrite IHp; auto. + intros; red; intros. + right. eapply Loc.in_notin_diff; eauto. Qed. - -Theorem Fpmov_correct2: - forall (p : Moves) (e : Env) (m : Move), - In m p -> - simpleDest p -> - no_overlap_list p -> - noTmp p -> - (let (s, d) := m in get (sexec (StateDone (Pmov (p, nil, nil))) e) d = get e s). + +Lemma source_no_overlap_dests: + forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> no_overlap_dests s. Proof. -intros p e m Hin Hsd Hno_O HnoTmp; destruct m as [s d]; - generalize (Fpmov_correctMoves p e); intros. -rewrite <- H; auto. -apply pexec_correct with ( m := (s, d) ); auto. -apply (In_noTmp_notempo s d p); auto. -apply (In_SD_no_o s d p Hin Hsd). + intros. elim H; intro. exact (NO_OVERLAP s H0). + elim H0; intro; subst s; red; intros; + right; apply Loc.diff_sym; apply NO_DSTS_TEMP; auto; simpl; tauto. Qed. - -Lemma notindst_nW: forall a p, Loc.notin a (getdst p) -> noWrite p a. + +Lemma source_not_temp1: + forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> Loc.diff s (R IT1) /\ Loc.diff s (R FT1). Proof. -induction p; simpl; auto. -destruct a0 as [a1 a2]. -simpl. -intros H; elim H; intro; split. -apply Loc.diff_sym; (try assumption). -apply IHp; auto. + intros. elim H; intro. + split; apply NO_SRCS_TEMP; auto; simpl; tauto. + elim H0; intro; subst s; simpl; split; congruence. Qed. - -Lemma disjoint_tmp__noTmp: - forall p, - Loc.disjoint (getsrc p) temporaries -> - Loc.disjoint (getdst p) temporaries -> noTmp p. -Proof. -induction p; simpl; auto. -destruct a as [a1 a2]; simpl getsrc; simpl getdst; unfold Loc.disjoint; intros; - (repeat split). -intro; unfold T; case (Loc.type r); apply H; (try (left; trivial; fail)). -right; left; trivial. -right; right; right; right; left; trivial. -intro; unfold T; case (Loc.type r); apply H0; (try (left; trivial; fail)). -right; left; trivial. -right; right; right; right; left; trivial. -apply IHp. -apply Loc.disjoint_cons_left with a1; auto. -apply Loc.disjoint_cons_left with a2; auto. + +Lemma dest_noteq_diff: + forall d l, + In d dsts \/ d = R IT2 \/ d = R FT2 -> + l <> d -> + no_overlap_dests l -> + Loc.diff l d. +Proof. + intros. elim H; intro. + elim (H1 d H2); intro. congruence. auto. + assert (forall r, l <> R r -> Loc.diff l (R r)). + intros. destruct l; simpl. congruence. destruct s; auto. + elim H2; intro; subst d; auto. Qed. - -Theorem Fpmov_correct_IT3: - forall p rs, - simpleDest p -> - no_overlap_list p -> - Loc.disjoint (getsrc p) temporaries -> - Loc.disjoint (getdst p) temporaries -> - (sexec (StateDone (Pmov (p, nil, nil))) rs) (R IT3) = rs (R IT3). -Proof. -intros p rs Hsd Hno_O Hdistmpsrc Hdistmpdst. -generalize (Fpmov_correctMoves p rs); unfold get, Locmap.get; intros H2. -rewrite <- H2; auto. -generalize (get_noWrite p (R IT3)); unfold get, Locmap.get; intros. -rewrite <- H; auto. -apply notindst_nW. -apply (Loc.disjoint_notin temporaries). -apply Loc.disjoint_sym; auto. -right; right; left; trivial. -apply disjoint_tmp__noTmp; auto. -unfold notemporary, T. -intros x; case (Loc.type x); simpl; intro; discriminate. -intros x H; right; apply Loc.in_notin_diff with (getdst p); auto. -apply Loc.disjoint_notin with temporaries; auto. -apply Loc.disjoint_sym; auto. -right; right; left; trivial. + +Definition locmap_equiv (e1 e2: Locmap.t): Prop := + forall l, + no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e2 l = e1 l. + +Definition effect_move (src dst: loc) (e e': Locmap.t): Prop := + e' dst = e src /\ + forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e' l = e l. + +Inductive effect_seqmove: list (loc * loc) -> Locmap.t -> Locmap.t -> Prop := + | effect_seqmove_nil: forall e, + effect_seqmove nil e e + | effect_seqmove_cons: forall s d m e1 e2 e3, + effect_move s d e1 e2 -> + effect_seqmove m e2 e3 -> + effect_seqmove ((s, d) :: m) e1 e3. + +Lemma effect_move_equiv: + forall s d e1 e2 e1', + (In s srcs \/ s = R IT2 \/ s = R FT2) -> + (In d dsts \/ d = R IT2 \/ d = R FT2) -> + locmap_equiv e1 e2 -> effect_move s d e1 e1' -> + locmap_equiv e1' (Parmov.update loc val Loc.eq d (e2 s) e2). +Proof. + intros. destruct H2. red; intros. + unfold Parmov.update. destruct (Loc.eq l d). + subst l. elim (source_not_temp1 _ H); intros. + rewrite H2. apply H1; auto. apply source_no_overlap_dests; auto. + rewrite H3; auto. apply dest_noteq_diff; auto. Qed. - -Theorem Fpmov_correct_map: - forall p rs, - simpleDest p -> - no_overlap_list p -> - Loc.disjoint (getsrc p) temporaries -> - Loc.disjoint (getdst p) temporaries -> - List.map (sexec (StateDone (Pmov (p, nil, nil))) rs) (getdst p) = - List.map rs (getsrc p). -Proof. -intros; rewrite getsrc_map; rewrite getdst_map; rewrite list_map_compose; - rewrite list_map_compose; apply list_map_exten; intros. -generalize (Fpmov_correct2 p rs x). -destruct x; simpl. -unfold get, Locmap.get; intros; auto. -rewrite H4; auto. -apply disjoint_tmp__noTmp; auto. + +Lemma effect_seqmove_equiv: + forall mu e1 e1', + effect_seqmove mu e1 e1' -> + forall e2, + (forall s d, In (s, d) mu -> + (In s srcs \/ s = R IT2 \/ s = R FT2) /\ + (In d dsts \/ d = R IT2 \/ d = R FT2)) -> + locmap_equiv e1 e2 -> + locmap_equiv e1' (exec_seq mu e2). +Proof. + induction 1; intros. + simpl. auto. + simpl. apply IHeffect_seqmove. + intros. apply H1. apply in_cons; auto. + destruct (H1 s d (in_eq _ _)). + eapply effect_move_equiv; eauto. Qed. - -Theorem Fpmov_correct_ext: - forall p rs, - simpleDest p -> - no_overlap_list p -> - Loc.disjoint (getsrc p) temporaries -> - Loc.disjoint (getdst p) temporaries -> - forall l, - Loc.notin l (getdst p) -> - Loc.notin l temporaries -> - (sexec (StateDone (Pmov (p, nil, nil))) rs) l = rs l. -Proof. -intros; generalize (Fpmov_correct1 p rs l); unfold get, Locmap.get; intros. -rewrite <- H5; auto. -apply disjoint_tmp__noTmp; auto. -unfold notemporary; simpl in H4 |-; unfold T; intros x; case (Loc.type x). -elim H4; - [intros H6 H7; elim H7; [intros H8 H9; (try clear H7 H4); (try exact H8)]]. -elim H4; - [intros H6 H7; elim H7; - [intros H8 H9; elim H9; - [intros H10 H11; elim H11; - [intros H12 H13; elim H13; - [intros H14 H15; (try clear H13 H11 H9 H7 H4); (try exact H14)]]]]]. -unfold no_overlap_list, no_overlap in H0 |-; intros. -case (Loc.eq l x). -intros e; left; (try assumption). -intros n; right; (try assumption). -apply Loc.in_notin_diff with (getdst p); auto. -apply notindst_nW; auto. + +Lemma effect_parmove: + forall e e', + effect_seqmove (parmove srcs dsts) e e' -> + List.map e' dsts = List.map e srcs /\ + e' (R IT3) = e (R IT3) /\ + forall l, Loc.notin l dsts -> Loc.notin l temporaries -> e' l = e l. +Proof. + set (mu := parmove srcs dsts). intros. + assert (locmap_equiv e e) by (red; auto). + generalize (effect_seqmove_equiv mu e e' H e (parmove_prop_2 srcs dsts) H0). + intro. + generalize (parmove_prop_1 srcs dsts LENGTH NOREPET NO_SRCS_TEMP NO_DSTS_TEMP e). + fold mu. intros [A B]. + (* e' dsts = e srcs *) + split. rewrite <- A. apply list_map_exten; intros. + apply H1. apply dests_no_overlap_dests; auto. + apply NO_DSTS_TEMP; auto; simpl; tauto. + apply NO_DSTS_TEMP; auto; simpl; tauto. + (* e' IT3 = e IT3 *) + split. + assert (Loc.notin (R IT3) dsts). + apply Loc.disjoint_notin with temporaries. + apply Loc.disjoint_sym; auto. simpl; tauto. + transitivity (exec_seq mu e (R IT3)). + symmetry. apply H1. apply notin_dests_no_overlap_dests. auto. + simpl; congruence. simpl; congruence. + apply B. apply Loc.notin_not_in; auto. congruence. congruence. + (* other locations *) + intros. transitivity (exec_seq mu e l). + symmetry. apply H1. apply notin_dests_no_overlap_dests; auto. + eapply Loc.in_notin_diff; eauto. simpl; tauto. + eapply Loc.in_notin_diff; eauto. simpl; tauto. + apply B. apply Loc.notin_not_in; auto. + apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto. + apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto. Qed. + +End EQUIVALENCE. + |