diff options
Diffstat (limited to 'backend/Parallelmove.v')
| -rw-r--r-- | backend/Parallelmove.v | 2529 |
1 files changed, 2529 insertions, 0 deletions
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v new file mode 100644 index 00000000..f95416eb --- /dev/null +++ b/backend/Parallelmove.v @@ -0,0 +1,2529 @@ +(** Translation of parallel moves into sequences of individual moves *) + +(** 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. + + 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. + + 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># +*) + +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)). +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. +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. +Qed. + +Lemma step_inv_NoOverlap: + forall (s1 s2 : State) r, + step s1 s2 -> notemporary r -> stepInv s1 -> NoOverlap r s1 -> NoOverlap r s2. +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. +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)). +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. +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. +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. +Qed. + +Lemma dstep_inv: + forall (r1 r2 : State), dstep r1 r2 -> stepInv r1 -> stepInv r2. +Proof. +intros. +apply (stepp_inv r1 r2); auto. +apply dstep_step; auto. +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. +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. +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. + +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. +Qed. + +Lemma getsrc_map: forall p, getsrc p = map (fun x => fst x) p. +Proof. +induction p. +simpl; auto. +destruct a; simpl. +rewrite IHp; auto. +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). +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). +Qed. + +Lemma notindst_nW: forall a p, Loc.notin a (getdst p) -> noWrite p a. +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. +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. +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. +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. +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. +Qed. |