From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- lib/Parmov.v | 308 +++++++++++++++++++++++++++++------------------------------ 1 file changed, 154 insertions(+), 154 deletions(-) (limited to 'lib/Parmov.v') diff --git a/lib/Parmov.v b/lib/Parmov.v index f96a692e..92bba559 100644 --- a/lib/Parmov.v +++ b/lib/Parmov.v @@ -61,7 +61,7 @@ Section PARMOV. (** * Registers, moves, and their semantics *) -(** The development is parameterized by the type of registers, +(** The development is parameterized by the type of registers, equipped with a decidable equality. *) Variable reg: Type. @@ -102,7 +102,7 @@ Lemma env_ext: (forall r, e1 r = e2 r) -> e1 = e2. Proof (@extensionality reg val). -(** The main operation over environments is update: it assigns +(** The main operation over environments is update: it assigns a value [v] to a register [r] and preserves the values of other registers. *) @@ -132,7 +132,7 @@ Lemma update_commut: r1 <> r2 -> update r1 v1 (update r2 v2 e) = update r2 v2 (update r1 v1 e). Proof. - intros. apply env_ext; intro; unfold update. + intros. apply env_ext; intro; unfold update. destruct (reg_eq r r1); destruct (reg_eq r r2); auto. congruence. Qed. @@ -174,7 +174,7 @@ Fixpoint exec_seq (m: moves) (e: env) {struct m}: env := Fixpoint exec_seq_rev (m: moves) (e: env) {struct m}: env := match m with | nil => e - | (s, d) :: m' => + | (s, d) :: m' => let e' := exec_seq_rev m' e in update d (e' s) e' end. @@ -274,7 +274,7 @@ Inductive state_wf: state -> Prop := Lemma dests_append: forall m1 m2, dests (m1 ++ m2) = dests m1 ++ dests m2. Proof. - intros. unfold dests. apply map_app. + intros. unfold dests. apply map_app. Qed. Lemma dests_decomp: @@ -286,7 +286,7 @@ Qed. Lemma srcs_append: forall m1 m2, srcs (m1 ++ m2) = srcs m1 ++ srcs m2. Proof. - intros. unfold srcs. apply map_app. + intros. unfold srcs. apply map_app. Qed. Lemma srcs_decomp: @@ -317,7 +317,7 @@ Lemma dests_disjoint_sym: forall m1 m2, dests_disjoint m1 m2 <-> dests_disjoint m2 m1. Proof. - unfold dests_disjoint; intros. + unfold dests_disjoint; intros. split; intros; apply list_disjoint_sym; auto. Qed. @@ -326,9 +326,9 @@ Lemma dests_disjoint_cons_left: dests_disjoint ((s, d) :: m1) m2 <-> dests_disjoint m1 m2 /\ ~In d (dests m2). Proof. - unfold dests_disjoint, list_disjoint. + unfold dests_disjoint, list_disjoint. simpl; intros; split; intros. - split. auto. firstorder. + split. auto. firstorder. destruct H. elim H0; intro. red; intro; subst. contradiction. apply H; auto. @@ -339,7 +339,7 @@ Lemma dests_disjoint_cons_right: dests_disjoint m1 ((s, d) :: m2) <-> dests_disjoint m1 m2 /\ ~In d (dests m1). Proof. - intros. rewrite dests_disjoint_sym. rewrite dests_disjoint_cons_left. + intros. rewrite dests_disjoint_sym. rewrite dests_disjoint_cons_left. rewrite dests_disjoint_sym. tauto. Qed. @@ -348,11 +348,11 @@ Lemma dests_disjoint_append_left: dests_disjoint (m1 ++ m2) m3 <-> dests_disjoint m1 m3 /\ dests_disjoint m2 m3. Proof. - unfold dests_disjoint, list_disjoint. + unfold dests_disjoint, list_disjoint. intros; split; intros. split; intros. apply H; eauto. rewrite dests_append. apply in_or_app. auto. apply H; eauto. rewrite dests_append. apply in_or_app. auto. - destruct H. + destruct H. rewrite dests_append in H0. elim (in_app_or _ _ _ H0); auto. Qed. @@ -361,7 +361,7 @@ Lemma dests_disjoint_append_right: dests_disjoint m1 (m2 ++ m3) <-> dests_disjoint m1 m2 /\ dests_disjoint m1 m3. Proof. - intros. rewrite dests_disjoint_sym. rewrite dests_disjoint_append_left. + intros. rewrite dests_disjoint_sym. rewrite dests_disjoint_append_left. intuition; rewrite dests_disjoint_sym; assumption. Qed. @@ -371,7 +371,7 @@ Lemma is_mill_cons: is_mill m /\ ~In d (dests m). Proof. unfold is_mill, dests_disjoint; intros. simpl. - split; intros. + split; intros. inversion H; tauto. constructor; tauto. Qed. @@ -381,7 +381,7 @@ Lemma is_mill_append: is_mill (m1 ++ m2) <-> is_mill m1 /\ is_mill m2 /\ dests_disjoint m1 m2. Proof. - unfold is_mill, dests_disjoint; intros. rewrite dests_append. + unfold is_mill, dests_disjoint; intros. rewrite dests_append. apply list_norepet_app. Qed. @@ -391,7 +391,7 @@ Lemma move_no_temp_append: forall m1 m2, move_no_temp m1 -> move_no_temp m2 -> move_no_temp (m1 ++ m2). Proof. - intros; red; intros. elim (in_app_or _ _ _ H1); intro. + intros; red; intros. elim (in_app_or _ _ _ H1); intro. apply H; auto. apply H0; auto. Qed. @@ -418,12 +418,12 @@ Lemma temp_last_push: is_not_temp s1 -> is_not_temp d1 -> temp_last ((s1, d1) :: (s2, d2) :: sigma). Proof. - unfold temp_last; intros. simpl. simpl in H. + unfold temp_last; intros. simpl. simpl in H. destruct (rev sigma); simpl in *. - intuition. red; simpl; intros. - elim H; intros. inversion H4. subst; tauto. tauto. - destruct p as [sN dN]. intuition. - red; intros. elim (in_app_or _ _ _ H); intros. + intuition. red; simpl; intros. + elim H; intros. inversion H4. subst; tauto. tauto. + destruct p as [sN dN]. intuition. + red; intros. elim (in_app_or _ _ _ H); intros. apply H3; auto. elim H4; intros. inversion H5; subst; tauto. elim H5. Qed. @@ -433,12 +433,12 @@ Lemma temp_last_pop: temp_last ((s1, d1) :: sigma ++ (s2, d2) :: nil) -> temp_last (sigma ++ (s2, d2) :: nil). Proof. - intros until d2. + intros until d2. change ((s1, d1) :: sigma ++ (s2, d2) :: nil) with ((((s1, d1) :: nil) ++ sigma) ++ ((s2, d2) :: nil)). - unfold temp_last. repeat rewrite rev_unit. - intuition. simpl in H1. red; intros. apply H1. - apply in_or_app. auto. + unfold temp_last. repeat rewrite rev_unit. + intuition. simpl in H1. red; intros. apply H1. + apply in_or_app. auto. Qed. (** Some properties of [is_path]. *) @@ -458,7 +458,7 @@ Proof. induction sigma; simpl; intros. constructor. red; auto. constructor. inversion H; subst; clear H. - constructor. + constructor. destruct sigma as [ | [s1 d1] sigma']; simpl; simpl in H2; auto. auto. Qed. @@ -471,12 +471,12 @@ Lemma path_sources_dests: Proof. induction sigma; simpl; intros. red; simpl; tauto. - inversion H; subst; clear H. simpl. + inversion H; subst; clear H. simpl. assert (In s (dests (sigma ++ (s0, d0) :: nil))). - destruct sigma as [ | [s1 d1] sigma']; simpl; simpl in H2; intuition. - apply incl_cons. simpl; tauto. + destruct sigma as [ | [s1 d1] sigma']; simpl; simpl in H2; intuition. + apply incl_cons. simpl; tauto. apply incl_tran with (s0 :: dests (sigma ++ (s0, d0) :: nil)). - eapply IHsigma; eauto. + eapply IHsigma; eauto. red; simpl; tauto. Qed. @@ -484,11 +484,11 @@ Lemma no_read_path: forall d1 sigma s0 d0, d1 <> s0 -> is_path (sigma ++ (s0, d0) :: nil) -> - ~In d1 (dests (sigma ++ (s0, d0) :: nil)) -> + ~In d1 (dests (sigma ++ (s0, d0) :: nil)) -> no_read (sigma ++ (s0, d0) :: nil) d1. Proof. intros. - generalize (path_sources_dests _ _ _ H0). intro. + generalize (path_sources_dests _ _ _ H0). intro. intro. elim H1. elim (H2 _ H3); intro. congruence. auto. Qed. @@ -499,7 +499,7 @@ Lemma notin_dests_cons: forall x s d m, ~In x (dests ((s, d) :: m)) <-> x <> d /\ ~In x (dests m). Proof. - intros. simpl. intuition auto. + intros. simpl. intuition auto. Qed. Lemma notin_dests_append: @@ -509,7 +509,7 @@ Proof. intros. rewrite dests_append. rewrite in_app. tauto. Qed. -Hint Rewrite is_mill_cons is_mill_append +Hint Rewrite is_mill_cons is_mill_append dests_disjoint_cons_left dests_disjoint_cons_right dests_disjoint_append_left dests_disjoint_append_right notin_dests_cons notin_dests_append: pmov. @@ -525,29 +525,29 @@ Proof. autorewrite with pmov in A; constructor; autorewrite with pmov. (* Nop *) - tauto. + tauto. red; intros. apply B. apply list_in_insert; auto. auto. auto. (* Start *) tauto. red; intros. apply B. apply list_in_insert; auto. - red. simpl. split. elim (B s d). auto. - apply in_or_app. right. apply in_eq. + red. simpl. split. elim (B s d). auto. + apply in_or_app. right. apply in_eq. red; simpl; tauto. - constructor. exact I. constructor. + constructor. exact I. constructor. (* Push *) intuition. red; intros. apply B. apply list_in_insert; auto. - elim (B d r). apply temp_last_push; auto. + elim (B d r). apply temp_last_push; auto. apply in_or_app; right; apply in_eq. constructor. simpl. auto. auto. (* Loop *) - tauto. + tauto. auto. - eapply temp_last_change_last_source; eauto. + eapply temp_last_change_last_source; eauto. eapply is_path_change_last_source; eauto. (* Pop *) @@ -557,7 +557,7 @@ Proof. eapply is_path_pop; eauto. (* Last *) - intuition. + intuition. auto. unfold temp_last. simpl. auto. constructor. @@ -577,7 +577,7 @@ Qed. reverse sequential order, then the moves [mu ++ sigma] in parallel. *) Definition statemove (st: state) (e: env) := - match st with + match st with | State mu sigma tau => exec_par (mu ++ sigma) (exec_seq_rev tau e) end. @@ -589,7 +589,7 @@ Lemma exec_par_outside: forall m e r, ~In r (dests m) -> exec_par m e r = e r. Proof. induction m; simpl; intros. auto. - destruct a as [s d]. rewrite update_o. apply IHm. tauto. + destruct a as [s d]. rewrite update_o. apply IHm. tauto. simpl in H. intuition. Qed. @@ -600,8 +600,8 @@ Lemma exec_par_lift: Proof. induction m1; simpl; intros. auto. - destruct a as [s0 d0]. simpl in H. rewrite IHm1. simpl. - apply update_commut. tauto. tauto. + destruct a as [s0 d0]. simpl in H. rewrite IHm1. simpl. + apply update_commut. tauto. tauto. Qed. Lemma exec_par_ident: @@ -609,9 +609,9 @@ Lemma exec_par_ident: is_mill (m1 ++ (r, r) :: m2) -> exec_par (m1 ++ (r, r) :: m2) e = exec_par (m1 ++ m2) e. Proof. - intros. autorewrite with pmov in H. - rewrite exec_par_lift. simpl. - replace (e r) with (exec_par (m1 ++ m2) e r). apply update_ident. + intros. autorewrite with pmov in H. + rewrite exec_par_lift. simpl. + replace (e r) with (exec_par (m1 ++ m2) e r). apply update_ident. apply exec_par_outside. autorewrite with pmov. tauto. tauto. Qed. @@ -619,7 +619,7 @@ Lemma exec_seq_app: forall m1 m2 e, exec_seq (m1 ++ m2) e = exec_seq m2 (exec_seq m1 e). Proof. - induction m1; simpl; intros. auto. + induction m1; simpl; intros. auto. destruct a as [s d]. rewrite IHm1. auto. Qed. @@ -627,7 +627,7 @@ Lemma exec_seq_rev_app: forall m1 m2 e, exec_seq_rev (m1 ++ m2) e = exec_seq_rev m1 (exec_seq_rev m2 e). Proof. - induction m1; simpl; intros. auto. + induction m1; simpl; intros. auto. destruct a as [s d]. rewrite IHm1. auto. Qed. @@ -657,8 +657,8 @@ Lemma exec_par_update_no_read: Proof. unfold no_read; induction m; simpl; intros. auto. - destruct a as [s0 d0]; simpl in *. rewrite IHm. - rewrite update_commut. f_equal. f_equal. + destruct a as [s0 d0]; simpl in *. rewrite IHm. + rewrite update_commut. f_equal. f_equal. apply update_o. tauto. tauto. tauto. tauto. Qed. @@ -682,14 +682,14 @@ Lemma exec_par_combine: Proof. induction sl; destruct dl; simpl; intros; try discriminate. split; auto. - inversion H0; subst; clear H0. + inversion H0; subst; clear H0. injection H; intro; clear H. destruct (IHsl dl H0 H4) as [A B]. set (e' := exec_par (combine sl dl) e) in *. split. - decEq. apply update_s. + decEq. apply update_s. rewrite <- A. apply list_map_exten; intros. - rewrite update_o. auto. congruence. + rewrite update_o. auto. congruence. intros. rewrite update_o. apply B. tauto. intuition. Qed. @@ -733,10 +733,10 @@ Lemma exec_par_env_equiv: Proof. unfold move_no_temp; induction m; simpl; intros. auto. - destruct a as [s d]. + destruct a as [s d]. red; intros. unfold update. destruct (reg_eq r d). - apply H0. elim (H s d); tauto. - apply IHm; auto. + apply H0. elim (H s d); tauto. + apply IHm; auto. Qed. (** The proof that transitions preserve semantics (up to the values of @@ -750,57 +750,57 @@ Proof. induction 1; intro WF; inversion WF as [mu0 sigma0 tau0 A B C D]; subst; simpl. (* nop *) - apply env_equiv_refl'. unfold statemove. - repeat rewrite app_ass. simpl. symmetry. apply exec_par_ident. - rewrite app_ass in A. exact A. + apply env_equiv_refl'. unfold statemove. + repeat rewrite app_ass. simpl. symmetry. apply exec_par_ident. + rewrite app_ass in A. exact A. (* start *) - apply env_equiv_refl'. unfold statemove. - autorewrite with pmov in A. + apply env_equiv_refl'. unfold statemove. + autorewrite with pmov in A. rewrite exec_par_lift. repeat rewrite app_ass. simpl. rewrite exec_par_lift. reflexivity. - tauto. autorewrite with pmov. tauto. + tauto. autorewrite with pmov. tauto. (* push *) - apply env_equiv_refl'. unfold statemove. + apply env_equiv_refl'. unfold statemove. autorewrite with pmov in A. rewrite exec_par_lift. rewrite exec_par_lift. simpl. - rewrite exec_par_lift. repeat rewrite app_ass. simpl. rewrite exec_par_lift. - simpl. apply update_commut. intuition. - tauto. autorewrite with pmov; tauto. - autorewrite with pmov; intuition. + rewrite exec_par_lift. repeat rewrite app_ass. simpl. rewrite exec_par_lift. + simpl. apply update_commut. intuition. + tauto. autorewrite with pmov; tauto. + autorewrite with pmov; intuition. autorewrite with pmov; intuition. (* loop *) - unfold statemove. simpl exec_seq_rev. - set (e1 := exec_seq_rev tau e). + unfold statemove. simpl exec_seq_rev. + set (e1 := exec_seq_rev tau e). autorewrite with pmov in A. - repeat rewrite <- app_ass. - assert (~In d (dests (mu ++ sigma))). autorewrite with pmov. tauto. - repeat rewrite exec_par_lift; auto. simpl. + repeat rewrite <- app_ass. + assert (~In d (dests (mu ++ sigma))). autorewrite with pmov. tauto. + repeat rewrite exec_par_lift; auto. simpl. repeat rewrite <- app_nil_end. assert (move_no_temp (mu ++ sigma)). - red in C. rewrite rev_unit in C. destruct C. + red in C. rewrite rev_unit in C. destruct C. apply move_no_temp_append; auto. apply move_no_temp_rev; auto. set (e2 := update (temp s) (e1 s) e1). set (e3 := exec_par (mu ++ sigma) e1). set (e4 := exec_par (mu ++ sigma) e2). assert (env_equiv e2 e1). - unfold e2; red; intros. apply update_o. apply H1. + unfold e2; red; intros. apply update_o. apply H1. assert (env_equiv e4 e3). unfold e4, e3. apply exec_par_env_equiv; auto. - red; intros. unfold update. destruct (reg_eq r d). + red; intros. unfold update. destruct (reg_eq r d). unfold e2. apply update_s. apply H2. auto. (* pop *) - apply env_equiv_refl'. unfold statemove. simpl exec_seq_rev. + apply env_equiv_refl'. unfold statemove. simpl exec_seq_rev. set (e1 := exec_seq_rev tau e). autorewrite with pmov in A. - apply exec_par_append_eq. simpl. - apply exec_par_update_no_read. - apply no_read_path; auto. eapply is_path_pop; eauto. + apply exec_par_append_eq. simpl. + apply exec_par_update_no_read. + apply no_read_path; auto. eapply is_path_pop; eauto. autorewrite with pmov; tauto. autorewrite with pmov; tauto. - intros. apply update_o. red; intro; subst r. elim (H H1). + intros. apply update_o. red; intro; subst r. elim (H H1). (* last *) apply env_equiv_refl'. unfold statemove. simpl exec_seq_rev. @@ -814,9 +814,9 @@ Lemma transitions_preserve_semantics: transitions st st' -> state_wf st -> env_equiv (statemove st' e) (statemove st e). Proof. - induction 1; intros. + induction 1; intros. eapply transition_preserves_semantics; eauto. - apply env_equiv_refl. + apply env_equiv_refl. apply env_equiv_trans with (statemove y e); auto. apply IHclos_refl_trans2. eapply transitions_preserve_wf; eauto. Qed. @@ -828,10 +828,10 @@ Lemma state_wf_start: state_wf (State mu nil nil). Proof. intros. constructor. rewrite <- app_nil_end. auto. - auto. + auto. red. simpl. auto. constructor. -Qed. +Qed. (** The main correctness result in this section is the following: if we can transition repeatedly from an initial state [mu, nil, nil] @@ -846,10 +846,10 @@ Theorem transitions_correctness: transitions (State mu nil nil) (State nil nil tau) -> forall e, env_equiv (exec_seq (List.rev tau) e) (exec_par mu e). Proof. - intros. + intros. generalize (transitions_preserve_semantics _ _ e H1 (state_wf_start _ H H0)). - unfold statemove. simpl. rewrite <- app_nil_end. + unfold statemove. simpl. rewrite <- app_nil_end. rewrite exec_seq_exec_seq_rev. auto. Qed. @@ -897,23 +897,23 @@ Lemma transition_determ: transitions st st'. Proof. induction 1; intro; unfold transitions. - apply rt_step. exact (tr_nop nil r mu nil tau). - apply rt_step. exact (tr_start nil s d mu tau). - apply rt_step. apply tr_push. + apply rt_step. exact (tr_nop nil r mu nil tau). + apply rt_step. exact (tr_start nil s d mu tau). + apply rt_step. apply tr_push. eapply rt_trans. - apply rt_step. + apply rt_step. change ((s, r0) :: sigma ++ (r0, d) :: nil) with (((s, r0) :: sigma) ++ (r0, d) :: nil). - apply tr_loop. - apply rt_step. simpl. apply tr_pop. auto. - inv H0. generalize H6. + apply tr_loop. + apply rt_step. simpl. apply tr_pop. auto. + inv H0. generalize H6. change ((s, r0) :: sigma ++ (r0, d) :: nil) with (((s, r0) :: sigma) ++ (r0, d) :: nil). unfold temp_last; rewrite List.rev_unit. intros [E F]. - elim (F s r0). unfold is_not_temp. auto. + elim (F s r0). unfold is_not_temp. auto. rewrite <- List.In_rev. apply in_eq. - apply rt_step. apply tr_pop. auto. auto. - apply rt_step. apply tr_last. auto. + apply rt_step. apply tr_pop. auto. auto. + apply rt_step. apply tr_last. auto. Qed. Lemma transitions_determ: @@ -939,9 +939,9 @@ Theorem dtransitions_correctness: dtransitions (State mu nil nil) (State nil nil tau) -> forall e, env_equiv (exec_seq (List.rev tau) e) (exec_par mu e). Proof. - intros. + intros. eapply transitions_correctness; eauto. - apply transitions_determ. auto. apply state_wf_start; auto. + apply transitions_determ. auto. apply state_wf_start; auto. Qed. (** * The compilation function *) @@ -1017,10 +1017,10 @@ Lemma split_move_charact: Proof. unfold no_read. induction m; simpl; intros. - tauto. -- destruct a as [s d]. destruct (reg_eq s r). +- destruct a as [s d]. destruct (reg_eq s r). + subst s. auto. + specialize (IHm r). destruct (split_move m r) as [[[before d'] after] | ]. - * destruct IHm. subst m. simpl. intuition. + * destruct IHm. subst m. simpl. intuition. * simpl; intuition. Qed. @@ -1030,11 +1030,11 @@ Lemma is_last_source_charact: then s = r else s <> r. Proof. - induction m; simpl. + induction m; simpl. destruct (reg_eq s r); congruence. destruct a as [s0 d0]. case_eq (m ++ (s, d) :: nil); intros. generalize (app_cons_not_nil m nil (s, d)). congruence. - rewrite <- H. auto. + rewrite <- H. auto. Qed. Lemma replace_last_source_charact: @@ -1055,24 +1055,24 @@ Lemma parmove_step_compatible: dtransition st (parmove_step st). Proof. intros st NOTFINAL. destruct st as [mu sigma tau]. unfold parmove_step. - case_eq mu; [intros MEQ | intros [ms md] mtl MEQ]. - case_eq sigma; [intros SEQ | intros [ss sd] stl SEQ]. - subst mu sigma. simpl in NOTFINAL. discriminate. - simpl. + case_eq mu; [intros MEQ | intros [ms md] mtl MEQ]. + case_eq sigma; [intros SEQ | intros [ss sd] stl SEQ]. + subst mu sigma. simpl in NOTFINAL. discriminate. + simpl. case_eq stl; [intros STLEQ | intros xx1 xx2 STLEQ]. apply dtr_last. red; simpl; auto. - elim (@exists_last _ stl). 2:congruence. intros sigma1 [[ss1 sd1] SEQ2]. - rewrite <- STLEQ. clear STLEQ xx1 xx2. - generalize (is_last_source_charact sd ss1 sd1 sigma1). + elim (@exists_last _ stl). 2:congruence. intros sigma1 [[ss1 sd1] SEQ2]. + rewrite <- STLEQ. clear STLEQ xx1 xx2. + generalize (is_last_source_charact sd ss1 sd1 sigma1). rewrite SEQ2. destruct (is_last_source sd (sigma1 ++ (ss1, sd1) :: nil)). - intro. subst ss1. - rewrite replace_last_source_charact. apply dtr_loop_pop. + intro. subst ss1. + rewrite replace_last_source_charact. apply dtr_loop_pop. red; simpl; auto. - intro. apply dtr_pop. red; simpl; auto. auto. + intro. apply dtr_pop. red; simpl; auto. auto. - case_eq sigma; [intros SEQ | intros [ss sd] stl SEQ]. - destruct (reg_eq ms md). - subst. apply dtr_nop. + case_eq sigma; [intros SEQ | intros [ss sd] stl SEQ]. + destruct (reg_eq ms md). + subst. apply dtr_nop. apply dtr_start. auto. generalize (split_move_charact ((ms, md) :: mtl) sd). @@ -1082,9 +1082,9 @@ Proof. intro NOREAD. case_eq stl; [intros STLEQ | intros xx1 xx2 STLEQ]. apply dtr_last. auto. - elim (@exists_last _ stl). 2:congruence. intros sigma1 [[ss1 sd1] SEQ2]. - rewrite <- STLEQ. clear STLEQ xx1 xx2. - generalize (is_last_source_charact sd ss1 sd1 sigma1). + elim (@exists_last _ stl). 2:congruence. intros sigma1 [[ss1 sd1] SEQ2]. + rewrite <- STLEQ. clear STLEQ xx1 xx2. + generalize (is_last_source_charact sd ss1 sd1 sigma1). rewrite SEQ2. destruct (is_last_source sd (sigma1 ++ (ss1, sd1) :: nil)). intro. subst ss1. rewrite replace_last_source_charact. apply dtr_loop_pop. auto. @@ -1120,7 +1120,7 @@ Qed. (** Compilation function for parallel moves. *) Function parmove_aux (st: state) {measure measure st} : moves := - if final_state st + if final_state st then match st with State _ _ tau => tau end else parmove_aux (parmove_step st). Proof. @@ -1134,7 +1134,7 @@ Proof. unfold dtransitions. intro st. functional induction (parmove_aux st). destruct _x; destruct _x0; simpl in e; discriminate || apply rt_refl. eapply rt_trans. apply rt_step. apply parmove_step_compatible; eauto. - auto. + auto. Qed. Definition parmove (mu: moves) : moves := @@ -1151,7 +1151,7 @@ Theorem parmove_correctness: env_equiv (exec_seq (parmove mu) e) (exec_par mu e). Proof. intros. unfold parmove. apply dtransitions_correctness; auto. - apply parmove_aux_transitions. + apply parmove_aux_transitions. Qed. (** Here is an alternate formulation of [parmove], where the @@ -1172,7 +1172,7 @@ Theorem parmove2_correctness: List.map e' dl = List.map e sl /\ forall r, ~In r dl -> is_not_temp r -> e' r = e r. Proof. - intros. + intros. destruct (srcs_dests_combine sl dl H) as [A B]. assert (env_equiv e' (exec_par (List.combine sl dl) e)). unfold e', parmove2. apply parmove_correctness. @@ -1182,8 +1182,8 @@ Proof. red. rewrite B. auto. destruct (exec_par_combine e sl dl H H0) as [C D]. set (e1 := exec_par (combine sl dl) e) in *. - split. rewrite <- C. apply list_map_exten; intros. - symmetry. apply H3. auto. + split. rewrite <- C. apply list_map_exten; intros. + symmetry. apply H3. auto. intros. transitivity (e1 r); auto. Qed. @@ -1213,7 +1213,7 @@ Definition wf_moves (m: moves) : Prop := Lemma wf_moves_cons: forall s d m, wf_moves ((s, d) :: m) <-> wf_move s d /\ wf_moves m. Proof. - unfold wf_moves; intros; simpl. firstorder. + unfold wf_moves; intros; simpl. firstorder. inversion H0; subst s0 d0. auto. Qed. @@ -1237,7 +1237,7 @@ Lemma dtransition_preserves_wf_state: dtransition st st' -> wf_state st -> wf_state st'. Proof. induction 1; intro WF; inv WF; constructor; autorewrite with pmov in *; intuition. - apply wf_move_temp_left; auto. + apply wf_move_temp_left; auto. eapply wf_move_temp_right; eauto. Qed. @@ -1245,31 +1245,31 @@ Lemma dtransitions_preserve_wf_state: forall st st', dtransitions st st' -> wf_state st -> wf_state st'. Proof. - induction 1; intros; eauto. + induction 1; intros; eauto. eapply dtransition_preserves_wf_state; eauto. -Qed. +Qed. End PROPERTIES. Lemma parmove_wf_moves: forall mu, wf_moves mu (parmove mu). Proof. - intros. + intros. assert (wf_state mu (State mu nil nil)). constructor. red; intros. apply wf_move_same. auto. red; simpl; tauto. red; simpl; tauto. generalize (dtransitions_preserve_wf_state mu _ _ (parmove_aux_transitions (State mu nil nil)) H). - intro WFS. inv WFS. - unfold parmove. red; intros. apply H5. + intro WFS. inv WFS. + unfold parmove. red; intros. apply H5. rewrite List.In_rev. auto. Qed. Lemma parmove2_wf_moves: forall sl dl, wf_moves (List.combine sl dl) (parmove2 sl dl). Proof. - intros. unfold parmove2. apply parmove_wf_moves. + intros. unfold parmove2. apply parmove_wf_moves. Qed. (** As a corollary, we show that all sources of [parmove mu] @@ -1278,12 +1278,12 @@ Qed. or temporaries. *) Remark wf_move_initial_reg_or_temp: - forall mu s d, + forall mu s d, wf_move mu s d -> (In s (srcs mu) \/ is_temp s) /\ (In d (dests mu) \/ is_temp d). Proof. - induction 1. - split; left. + induction 1. + split; left. change s with (fst (s, d)). unfold srcs. apply List.in_map; auto. change d with (snd (s, d)). unfold dests. apply List.in_map; auto. split. right. exists s; auto. tauto. @@ -1316,7 +1316,7 @@ Lemma parmove_srcs_initial_reg_or_temp: forall mu s, In s (srcs (parmove mu)) -> In s (srcs mu) \/ is_temp s. Proof. - intros. destruct (in_srcs _ _ H) as [d A]. + intros. destruct (in_srcs _ _ H) as [d A]. destruct (parmove_initial_reg_or_temp _ _ _ A). auto. Qed. @@ -1324,7 +1324,7 @@ Lemma parmove_dests_initial_reg_or_temp: forall mu d, In d (dests (parmove mu)) -> In d (dests mu) \/ is_temp d. Proof. - intros. destruct (in_dests _ _ H) as [s A]. + intros. destruct (in_dests _ _ H) as [s A]. destruct (parmove_initial_reg_or_temp _ _ _ A). auto. Qed. @@ -1455,11 +1455,11 @@ Hypothesis temps_no_overlap: Lemma disjoint_list_notin: forall r l, disjoint_list r l -> ~In r l. Proof. - intros. red; intro. - assert (r <> r). apply disjoint_not_equal. apply H; auto. + intros. red; intro. + assert (r <> r). apply disjoint_not_equal. apply H; auto. congruence. Qed. - + Lemma pairwise_disjoint_norepet: forall l, pairwise_disjoint l -> list_norepet l. Proof. @@ -1513,7 +1513,7 @@ Proof. subst. right. apply H. auto. subst. right. apply disjoint_sym. apply H. auto. auto. -Qed. +Qed. Lemma no_adherence_dst: forall d, In d (dests mu) -> no_adherence d. @@ -1547,7 +1547,7 @@ Qed. Definition env_match (e1 e2: env) : Prop := forall r, no_adherence r -> e1 r = e2 r. -(** The following lemmas relate the effect of executing moves +(** The following lemmas relate the effect of executing moves using normal, overlap-unaware update and weak, overlap-aware update. *) Lemma weak_update_match: @@ -1558,9 +1558,9 @@ Lemma weak_update_match: env_match (update d (e1 s) e1) (weak_update d (e2 s) e2). Proof. - intros. red; intros. + intros. red; intros. assert (no_overlap d r). apply H2. auto. - destruct H3. + destruct H3. subst. rewrite update_s. rewrite weak_update_s. apply H1. destruct H. apply no_adherence_src; auto. apply no_adherence_tmp; auto. rewrite update_o. rewrite weak_update_d. apply H1. auto. @@ -1576,8 +1576,8 @@ Lemma weak_exec_seq_match: Proof. induction m; intros; simpl. auto. - destruct a as [s d]. simpl in H. simpl in H0. - apply IHm; auto. + destruct a as [s d]. simpl in H. simpl in H0. + apply IHm; auto. apply weak_update_match; auto. Qed. @@ -1600,7 +1600,7 @@ Theorem parmove2_correctness_with_overlap: forall r, disjoint_list r dl -> disjoint_temps r -> e' r = e r. Proof. intros. - assert (list_norepet dl). + assert (list_norepet dl). apply pairwise_disjoint_norepet; auto. assert (forall r : reg, In r sl -> is_not_temp r). intros. apply disjoint_temps_not_temp; auto. @@ -1608,7 +1608,7 @@ Proof. intros. apply disjoint_temps_not_temp; auto. generalize (parmove2_correctness sl dl H H5 H6 H7 e). set (e1 := exec_seq (parmove2 sl dl) e). intros [A B]. - destruct (srcs_dests_combine sl dl H) as [C D]. + destruct (srcs_dests_combine sl dl H) as [C D]. assert (env_match (combine sl dl) e1 e'). unfold parmove2. unfold e1, e'. apply weak_exec_seq_match; try (rewrite C); try (rewrite D); auto. @@ -1616,11 +1616,11 @@ Proof. intros. rewrite <- D. apply parmove_dests_initial_reg_or_temp. auto. red; auto. split. - rewrite <- A. + rewrite <- A. apply list_map_exten; intros. apply H8. - apply no_adherence_dst. rewrite D; auto. rewrite D; auto. rewrite D; auto. + apply no_adherence_dst. rewrite D; auto. rewrite D; auto. rewrite D; auto. intros. transitivity (e1 r). - symmetry. apply H8. red. rewrite D. intros. destruct H11. + symmetry. apply H8. red. rewrite D. intros. destruct H11. right. apply disjoint_sym. apply H9. auto. right. apply disjoint_sym. apply H10. auto. apply B. apply disjoint_list_notin; auto. apply disjoint_temps_not_temp; auto. -- cgit