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. --- common/Smallstep.v | 350 ++++++++++++++++++++++++++--------------------------- 1 file changed, 175 insertions(+), 175 deletions(-) (limited to 'common/Smallstep.v') diff --git a/common/Smallstep.v b/common/Smallstep.v index ab41d327..71cef35f 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -62,7 +62,7 @@ Inductive star (ge: genv): state -> trace -> state -> Prop := Lemma star_one: forall ge s1 t s2, step ge s1 t s2 -> star ge s1 t s2. Proof. - intros. eapply star_step; eauto. apply star_refl. traceEq. + intros. eapply star_step; eauto. apply star_refl. traceEq. Qed. Lemma star_two: @@ -70,7 +70,7 @@ Lemma star_two: step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> star ge s1 t s3. Proof. - intros. eapply star_step; eauto. apply star_one; auto. + intros. eapply star_step; eauto. apply star_one; auto. Qed. Lemma star_three: @@ -78,7 +78,7 @@ Lemma star_three: step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 -> star ge s1 t s4. Proof. - intros. eapply star_step; eauto. eapply star_two; eauto. + intros. eapply star_step; eauto. eapply star_two; eauto. Qed. Lemma star_four: @@ -87,7 +87,7 @@ Lemma star_four: step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 -> star ge s1 t s5. Proof. - intros. eapply star_step; eauto. eapply star_three; eauto. + intros. eapply star_step; eauto. eapply star_three; eauto. Qed. Lemma star_trans: @@ -119,13 +119,13 @@ Lemma star_E0_ind: (forall s1 s2 s3, step ge s1 E0 s2 -> P s2 s3 -> P s1 s3) -> forall s1 s2, star ge s1 E0 s2 -> P s1 s2. Proof. - intros ge P BASE REC. + intros ge P BASE REC. assert (forall s1 t s2, star ge s1 t s2 -> t = E0 -> P s1 s2). induction 1; intros; subst. auto. destruct (Eapp_E0_inv _ _ H2). subst. eauto. eauto. -Qed. +Qed. (** One or several transitions. Also known as the transitive closure. *) @@ -146,7 +146,7 @@ Lemma plus_two: step ge s1 t1 s2 -> step ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. Proof. - intros. eapply plus_left; eauto. apply star_one; auto. + intros. eapply plus_left; eauto. apply star_one; auto. Qed. Lemma plus_three: @@ -154,7 +154,7 @@ Lemma plus_three: step ge s1 t1 s2 -> step ge s2 t2 s3 -> step ge s3 t3 s4 -> t = t1 ** t2 ** t3 -> plus ge s1 t s4. Proof. - intros. eapply plus_left; eauto. eapply star_two; eauto. + intros. eapply plus_left; eauto. eapply star_two; eauto. Qed. Lemma plus_four: @@ -163,14 +163,14 @@ Lemma plus_four: step ge s3 t3 s4 -> step ge s4 t4 s5 -> t = t1 ** t2 ** t3 ** t4 -> plus ge s1 t s5. Proof. - intros. eapply plus_left; eauto. eapply star_three; eauto. + intros. eapply plus_left; eauto. eapply star_three; eauto. Qed. Lemma plus_star: forall ge s1 t s2, plus ge s1 t s2 -> star ge s1 t s2. Proof. intros. inversion H; subst. - eapply star_step; eauto. + eapply star_step; eauto. Qed. Lemma plus_right: @@ -180,7 +180,7 @@ Lemma plus_right: Proof. intros. inversion H; subst. simpl. apply plus_one. auto. rewrite Eapp_assoc. eapply plus_left; eauto. - eapply star_right; eauto. + eapply star_right; eauto. Qed. Lemma plus_left': @@ -203,7 +203,7 @@ Lemma plus_star_trans: forall ge s1 t1 s2 t2 s3 t, plus ge s1 t1 s2 -> star ge s2 t2 s3 -> t = t1 ** t2 -> plus ge s1 t s3. Proof. - intros. inversion H; subst. + intros. inversion H; subst. econstructor; eauto. eapply star_trans; eauto. traceEq. Qed. @@ -214,8 +214,8 @@ Lemma star_plus_trans: Proof. intros. inversion H; subst. simpl; auto. - rewrite Eapp_assoc. - econstructor. eauto. eapply star_trans. eauto. + rewrite Eapp_assoc. + econstructor. eauto. eapply star_trans. eauto. apply plus_star. eauto. eauto. auto. Qed. @@ -227,7 +227,7 @@ Proof. Qed. Lemma plus_inv: - forall ge s1 t s2, + forall ge s1 t s2, plus ge s1 t s2 -> step ge s1 t s2 \/ exists s', exists t1, exists t2, step ge s1 t1 s' /\ plus ge s' t2 s2 /\ t = t1 ** t2. Proof. @@ -248,7 +248,7 @@ Qed. Lemma plus_ind2: forall ge (P: state -> trace -> state -> Prop), (forall s1 t s2, step ge s1 t s2 -> P s1 t s2) -> - (forall s1 t1 s2 t2 s3 t, + (forall s1 t1 s2 t2 s3 t, step ge s1 t1 s2 -> plus ge s2 t2 s3 -> P s2 t2 s3 -> t = t1 ** t2 -> P s1 t s3) -> forall s1 t s2, plus ge s1 t s2 -> P s1 t s2. @@ -261,7 +261,7 @@ Proof. rewrite E0_right. apply BASE; auto. eapply IND. eauto. econstructor; eauto. subst t. eapply IHstar; eauto. auto. - intros. inv H0. eauto. + intros. inv H0. eauto. Qed. Lemma plus_E0_ind: @@ -290,7 +290,7 @@ Qed. Remark star_starN: forall ge s t s', star ge s t s' -> exists n, starN ge n s t s'. Proof. - induction 1. + induction 1. exists O; constructor. destruct IHstar as [n P]. exists (S n); econstructor; eauto. Qed. @@ -308,9 +308,9 @@ Lemma star_forever: forever ge s1 (t *** T). Proof. induction 1; intros. simpl. auto. - subst t. rewrite Eappinf_assoc. + subst t. rewrite Eappinf_assoc. econstructor; eauto. -Qed. +Qed. (** An alternate, equivalent definition of [forever] that is useful for coinductive reasoning. *) @@ -320,7 +320,7 @@ Variable order: A -> A -> Prop. CoInductive forever_N (ge: genv) : A -> state -> traceinf -> Prop := | forever_N_star: forall s1 t s2 a1 a2 T1 T2, - star ge s1 t s2 -> + star ge s1 t s2 -> order a2 a1 -> forever_N ge a2 s2 T2 -> T1 = t *** T2 -> @@ -344,7 +344,7 @@ Proof. (* star case *) inv H1. (* no transition *) - change (E0 *** T2) with T2. apply H with a2. auto. auto. + change (E0 *** T2) with T2. apply H with a2. auto. auto. (* at least one transition *) exists t1; exists s0; exists x; exists (t2 *** T2). split. auto. split. eapply forever_N_star; eauto. @@ -353,7 +353,7 @@ Proof. inv H1. exists t1; exists s0; exists a2; exists (t2 *** T2). split. auto. - split. inv H3. auto. + split. inv H3. auto. eapply forever_N_plus. econstructor; eauto. eauto. auto. apply Eappinf_assoc. Qed. @@ -363,7 +363,7 @@ Lemma forever_N_forever: Proof. cofix COINDHYP; intros. destruct (forever_N_inv H) as [t [s' [a' [T' [P [Q R]]]]]]. - rewrite R. apply forever_intro with s'. auto. + rewrite R. apply forever_intro with s'. auto. apply COINDHYP with a'; auto. Qed. @@ -371,7 +371,7 @@ Qed. CoInductive forever_plus (ge: genv) : state -> traceinf -> Prop := | forever_plus_intro: forall s1 t s2 T1 T2, - plus ge s1 t s2 -> + plus ge s1 t s2 -> forever_plus ge s2 T2 -> T1 = t *** T2 -> forever_plus ge s1 T1. @@ -384,8 +384,8 @@ Lemma forever_plus_inv: Proof. intros. inv H. inv H0. exists s0; exists t1; exists (t2 *** T2). split. auto. - split. exploit star_inv; eauto. intros [[P Q] | R]. - subst. simpl. auto. econstructor; eauto. + split. exploit star_inv; eauto. intros [[P Q] | R]. + subst. simpl. auto. econstructor; eauto. traceEq. Qed. @@ -408,7 +408,7 @@ CoInductive forever_silent (ge: genv): state -> Prop := CoInductive forever_silent_N (ge: genv) : A -> state -> Prop := | forever_silent_N_star: forall s1 s2 a1 a2, - star ge s1 E0 s2 -> + star ge s1 E0 s2 -> order a2 a1 -> forever_silent_N ge a2 s2 -> forever_silent_N ge a1 s1 @@ -428,15 +428,15 @@ Proof. (* star case *) inv H1. (* no transition *) - apply H with a2. auto. auto. + apply H with a2. auto. auto. (* at least one transition *) - exploit Eapp_E0_inv; eauto. intros [P Q]. subst. + exploit Eapp_E0_inv; eauto. intros [P Q]. subst. exists s0; exists x. split. auto. eapply forever_silent_N_star; eauto. (* plus case *) - inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst. + inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst. exists s0; exists a2. - split. auto. inv H3. auto. + split. auto. inv H3. auto. eapply forever_silent_N_plus. econstructor; eauto. eauto. Qed. @@ -445,7 +445,7 @@ Lemma forever_silent_N_forever: Proof. cofix COINDHYP; intros. destruct (forever_silent_N_inv H) as [s' [a' [P Q]]]. - apply forever_silent_intro with s'. auto. + apply forever_silent_intro with s'. auto. apply COINDHYP with a'; auto. Qed. @@ -461,8 +461,8 @@ Lemma star_forever_reactive: star ge s1 t s2 -> forever_reactive ge s2 T -> forever_reactive ge s1 (t *** T). Proof. - intros. inv H0. rewrite <- Eappinf_assoc. econstructor. - eapply star_trans; eauto. + intros. inv H0. rewrite <- Eappinf_assoc. econstructor. + eapply star_trans; eauto. red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction. auto. Qed. @@ -523,7 +523,7 @@ Record forward_simulation (L1 L2: semantics) : Type := forall s1, initial_state L1 s1 -> exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2; fsim_match_final_states: - forall i s1 s2 r, + forall i s1 s2 r, fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r; fsim_simulation: forall s1 t s1', Step L1 s1 t s1' -> @@ -546,12 +546,12 @@ Lemma fsim_simulation': (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2') \/ (exists i', fsim_order S i' i /\ t = E0 /\ S i' s1' s2). Proof. - intros. exploit fsim_simulation; eauto. - intros [i' [s2' [A B]]]. intuition. + intros. exploit fsim_simulation; eauto. + intros [i' [s2' [A B]]]. intuition. left; exists i'; exists s2'; auto. - inv H2. + inv H2. right; exists i'; auto. - left; exists i'; exists s2'; split; auto. econstructor; eauto. + left; exists i'; exists s2'; split; auto. econstructor; eauto. Qed. (** ** Forward simulation diagrams. *) @@ -618,7 +618,7 @@ End SIMULATION_STAR_WF. Section SIMULATION_STAR. (** We now consider the case where we have a nonnegative integer measure - associated with states of the first semantics. It must decrease when we take + associated with states of the first semantics. It must decrease when we take a stuttering step. *) Variable measure: state L1 -> nat. @@ -670,7 +670,7 @@ Hypothesis simulation: Lemma forward_simulation_step: forward_simulation L1 L2. Proof. - apply forward_simulation_plus. + apply forward_simulation_plus. intros. exploit simulation; eauto. intros [s2' [A B]]. exists s2'; split; auto. apply plus_one; auto. Qed. @@ -723,7 +723,7 @@ Proof. exploit fsim_simulation; eauto. intros [i' [s2' [A B]]]. exploit IHstar; eauto. intros [i'' [s2'' [C D]]]. exists i''; exists s2''; split; auto. eapply star_trans; eauto. - intuition. apply plus_star; auto. + intuition. apply plus_star; auto. Qed. Lemma simulation_plus: @@ -736,10 +736,10 @@ Proof. (* base case *) exploit fsim_simulation'; eauto. intros [A | [i' A]]. left; auto. - right; exists i'; intuition. + right; exists i'; intuition. (* inductive case *) exploit fsim_simulation'; eauto. intros [[i' [s2' [A B]]] | [i' [A [B C]]]]. - exploit simulation_star. apply plus_star; eauto. eauto. + exploit simulation_star. apply plus_star; eauto. eauto. intros [i'' [s2'' [P Q]]]. left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto. exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]]. @@ -770,7 +770,7 @@ Lemma simulation_forever_reactive: Forever_reactive L2 s2 T. Proof. cofix COINDHYP; intros. - inv H. + inv H. destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]]. econstructor; eauto. Qed. @@ -803,7 +803,7 @@ Proof. (* initial states *) intros. exploit (fsim_match_initial_states S12); eauto. intros [i [s2 [A B]]]. exploit (fsim_match_initial_states S23); eauto. intros [i' [s3 [C D]]]. - exists (i', i); exists s3; split; auto. exists s2; auto. + exists (i', i); exists s3; split; auto. exists s2; auto. (* final states *) intros. destruct H as [s3 [A B]]. eapply (fsim_match_final_states S23); eauto. @@ -816,12 +816,12 @@ Proof. (* L3 makes one or several steps *) exists (i2', i1'); exists s2'; split. auto. exists s3'; auto. (* L3 makes no step *) - exists (i2', i1'); exists s2; split. + exists (i2', i1'); exists s2; split. right; split. subst t; apply star_refl. red. left. auto. - exists s3'; auto. + exists s3'; auto. (* L2 makes no step *) exists (i2, i1'); exists s2; split. - right; split. subst t; apply star_refl. red. right. auto. + right; split. subst t; apply star_refl. red. right. auto. exists s3; auto. (* symbols *) intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply fsim_public_preserved; auto. @@ -867,7 +867,7 @@ Lemma sd_determ_1: Step L s t1 s1 -> Step L s t2 s2 -> match_traces (symbolenv L) t1 t2. Proof. intros. eapply sd_determ; eauto. -Qed. +Qed. Lemma sd_determ_2: forall s t s1 s2, @@ -880,7 +880,7 @@ Lemma star_determinacy: forall s t s', Star L s t s' -> forall s'', Star L s t s'' -> Star L s' E0 s'' \/ Star L s'' E0 s'. Proof. - induction 1; intros. + induction 1; intros. auto. inv H2. right. eapply star_step; eauto. @@ -888,12 +888,12 @@ Proof. exploit (sd_traces DET). eexact H. intros L1. exploit (sd_traces DET). eexact H3. intros L2. assert (t1 = t0 /\ t2 = t3). - destruct t1. inv MT. auto. - destruct t1; simpl in L1; try omegaContradiction. + destruct t1. inv MT. auto. + destruct t1; simpl in L1; try omegaContradiction. destruct t0. inv MT. destruct t0; simpl in L2; try omegaContradiction. simpl in H5. split. congruence. congruence. destruct H1; subst. - assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4. + assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4. auto. Qed. @@ -903,7 +903,7 @@ End DETERMINACY. Definition safe (L: semantics) (s: state L) : Prop := forall s', - Star L s E0 s' -> + Star L s E0 s' -> (exists r, final_state L s' r) \/ (exists t, exists s'', Step L s' t s''). @@ -912,7 +912,7 @@ Lemma star_safe: Star L s E0 s' -> safe L s -> safe L s'. Proof. intros; red; intros. apply H0. eapply star_trans; eauto. -Qed. +Qed. (** The general form of a backward simulation. *) @@ -928,11 +928,11 @@ Record backward_simulation (L1 L2: semantics) : Type := forall s1 s2, initial_state L1 s1 -> initial_state L2 s2 -> exists i, exists s1', initial_state L1 s1' /\ bsim_match_states i s1' s2; bsim_match_final_states: - forall i s1 s2 r, - bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r -> + forall i s1 s2 r, + bsim_match_states i s1 s2 -> safe L1 s1 -> final_state L2 s2 r -> exists s1', Star L1 s1 E0 s1' /\ final_state L1 s1' r; bsim_progress: - forall i s1 s2, + forall i s1 s2, bsim_match_states i s1 s2 -> safe L1 s1 -> (exists r, final_state L2 s2 r) \/ (exists t, exists s2', Step L2 s2 t s2'); @@ -955,12 +955,12 @@ Lemma bsim_simulation': (exists i', exists s1', Plus L1 s1 t s1' /\ S i' s1' s2') \/ (exists i', bsim_order S i' i /\ t = E0 /\ S i' s1 s2'). Proof. - intros. exploit bsim_simulation; eauto. - intros [i' [s1' [A B]]]. intuition. + intros. exploit bsim_simulation; eauto. + intros [i' [s1' [A B]]]. intuition. left; exists i'; exists s1'; auto. - inv H3. + inv H3. right; exists i'; auto. - left; exists i'; exists s1'; split; auto. econstructor; eauto. + left; exists i'; exists s1'; split; auto. econstructor; eauto. Qed. (** ** Backward simulation diagrams. *) @@ -985,11 +985,11 @@ Hypothesis match_initial_states: exists s1', initial_state L1 s1' /\ match_states s1' s2. Hypothesis match_final_states: - forall s1 s2 r, + forall s1 s2 r, match_states s1 s2 -> final_state L2 s2 r -> final_state L1 s1 r. Hypothesis progress: - forall s1 s2, + forall s1 s2, match_states s1 s2 -> safe L1 s1 -> (exists r, final_state L2 s2 r) \/ (exists t, exists s2', Step L2 s2 t s2'). @@ -1009,8 +1009,8 @@ Proof. auto. red; intros; constructor; intros. contradiction. intros. exists tt; eauto. - intros. exists s1; split. apply star_refl. eauto. - intros. exploit simulation; eauto. intros [s1' [A B]]. + intros. exists s1; split. apply star_refl. eauto. + intros. exploit simulation; eauto. intros [s1' [A B]]. exists tt; exists s1'; auto. Qed. @@ -1036,7 +1036,7 @@ Proof. intros. exists i; exists s1; split; auto. apply star_refl. (* inductive case *) intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]]. - assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto. + assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto. exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]]. exists i''; exists s1''; split; auto. eapply star_trans; eauto. Qed. @@ -1045,7 +1045,7 @@ Lemma bsim_safe: forall i s1 s2, S i s1 s2 -> safe L1 s1 -> safe L2 s2. Proof. - intros; red; intros. + intros; red; intros. exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]]. eapply bsim_progress; eauto. eapply star_safe; eauto. Qed. @@ -1065,8 +1065,8 @@ Proof. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. exploit bsim_E0_star. apply plus_star; eauto. eauto. eapply star_safe; eauto. apply plus_star; auto. - intros [i'' [s1'' [P Q]]]. - left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto. + intros [i'' [s1'' [P Q]]]. + left; exists i''; exists s1''; intuition. eapply plus_star_trans; eauto. exploit IHplus; eauto. intros [P | [i'' [P Q]]]. left; auto. right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto. @@ -1079,12 +1079,12 @@ Proof. induction 1; intros. simpl in H; discriminate. subst t. - assert (EITHER: t1 = E0 \/ t2 = E0). - unfold Eapp in H2; rewrite app_length in H2. + assert (EITHER: t1 = E0 \/ t2 = E0). + unfold Eapp in H2; rewrite app_length in H2. destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction. - destruct EITHER; subst. - exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]]. - exists s2x; exists s2y; intuition. eapply star_left; eauto. + destruct EITHER; subst. + exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]]. + exists s2x; exists s2y; intuition. eapply star_left; eauto. rewrite E0_right. exists s1; exists s2; intuition. apply star_refl. Qed. @@ -1116,7 +1116,7 @@ Lemma bb_match_at: forall i1 i2 s1 s3 s2, bb_match_states (i1, i2) s1 s3. Proof. intros. econstructor; eauto. apply star_refl. -Qed. +Qed. Lemma bb_simulation_base: forall s3 t s3', Step L3 s3 t s3' -> @@ -1130,29 +1130,29 @@ Proof. intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]]. (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). - exploit L3_single_events; eauto. + exploit L3_single_events; eauto. destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. destruct EITHER. (* 1.1 these are silent transitions *) - subst t. exploit bsim_E0_plus; eauto. + subst t. exploit bsim_E0_plus; eauto. intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]]. (* 1.1.1 L1 makes one or several transitions *) - exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto. + exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto. (* 1.1.2 L1 makes no transitions *) - exists (i1', i2'); exists s1; split. - right; split. apply star_refl. left; auto. - eapply bb_match_at; eauto. + exists (i1', i2'); exists s1; split. + right; split. apply star_refl. left; auto. + eapply bb_match_at; eauto. (* 1.2 non-silent transitions *) - exploit star_non_E0_split. apply plus_star; eauto. auto. + exploit star_non_E0_split. apply plus_star; eauto. auto. intros [s2x [s2y [P [Q R]]]]. exploit bsim_E0_star. eexact P. eauto. auto. intros [i1' [s1x [X Y]]]. - exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto. + exploit bsim_simulation'. eexact Q. eauto. eapply star_safe; eauto. intros [[i1'' [s1y [U V]]] | [i1'' [U [V W]]]]; try (subst t; discriminate). exists (i1'', i2'); exists s1y; split. left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto. (* 2. L2 makes no transitions *) subst. exists (i1, i2'); exists s1; split. - right; split. apply star_refl. right; auto. + right; split. apply star_refl. right; auto. eapply bb_match_at; eauto. Qed. @@ -1163,12 +1163,12 @@ Lemma bb_simulation: (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' i)) /\ bb_match_states i' s1' s3'. Proof. - intros. inv H0. + intros. inv H0. exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS]. (* 1. match at *) subst. eapply bb_simulation_base; eauto. (* 2. match later *) - exploit bsim_E0_plus; eauto. + exploit bsim_E0_plus; eauto. intros [[i1' [s1' [A B]]] | [i1' [A B]]]. (* 2.1 one or several silent transitions *) exploit bb_simulation_base. eauto. auto. eexact B. eauto. @@ -1176,13 +1176,13 @@ Proof. intros [i'' [s1'' [C D]]]. exists i''; exists s1''; split; auto. left. eapply plus_star_trans; eauto. - destruct C as [P | [P Q]]. apply plus_star; eauto. eauto. + destruct C as [P | [P Q]]. apply plus_star; eauto. eauto. traceEq. (* 2.2 no silent transition *) exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto. intros [i'' [s1'' [C D]]]. exists i''; exists s1''; split; auto. - intuition. right; intuition. + intuition. right; intuition. inv H6. left. eapply t_trans; eauto. left; auto. Qed. @@ -1202,17 +1202,17 @@ Proof. exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto. (* match final states *) intros i s1 s3 r MS SAFE FIN. inv MS. - exploit (bsim_match_final_states S23); eauto. - eapply star_safe; eauto. eapply bsim_safe; eauto. + exploit (bsim_match_final_states S23); eauto. + eapply star_safe; eauto. eapply bsim_safe; eauto. intros [s2' [A B]]. exploit bsim_E0_star. eapply star_trans. eexact H0. eexact A. auto. eauto. auto. intros [i1' [s1' [C D]]]. - exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto. - intros [s1'' [P Q]]. + exploit (bsim_match_final_states S12); eauto. eapply star_safe; eauto. + intros [s1'' [P Q]]. exists s1''; split; auto. eapply star_trans; eauto. (* progress *) intros i s1 s3 MS SAFE. inv MS. - eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. + eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. (* simulation *) exact bb_simulation. (* symbols *) @@ -1243,21 +1243,21 @@ Inductive f2b_transitions: state L1 -> state L2 -> Prop := Star L1 s1 E0 s1' -> Step L1 s1' t s1'' -> Plus L2 s2 t s2' -> - FS i' s1' s2 -> + FS i' s1' s2 -> FS i'' s1'' s2' -> f2b_transitions s1 s2. Lemma f2b_progress: forall i s1 s2, FS i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2. Proof. - intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS). + intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS). apply fsim_order_wf. intros i REC s1 s2 MATCH SAFE. destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl. (* final state reached *) - eapply f2b_trans_final; eauto. + eapply f2b_trans_final; eauto. apply star_refl. - eapply fsim_match_final_states; eauto. + eapply fsim_match_final_states; eauto. (* L1 can make one step *) exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]]. assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ fsim_order FS i' i)). @@ -1267,7 +1267,7 @@ Proof. eapply f2b_trans_step; eauto. apply star_refl. subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto. intros TRANS; inv TRANS. - eapply f2b_trans_final; eauto. eapply star_left; eauto. + eapply f2b_trans_final; eauto. eapply star_left; eauto. eapply f2b_trans_step; eauto. eapply star_left; eauto. Qed. @@ -1293,7 +1293,7 @@ Qed. Remark not_silent_length: forall t1 t2, (length (t1 ** t2) <= 1)%nat -> t1 = E0 \/ t2 = E0. Proof. - unfold Eapp, E0; intros. rewrite app_length in H. + unfold Eapp, E0; intros. rewrite app_length in H. destruct t1; destruct t2; auto. simpl in H. omegaContradiction. Qed. @@ -1303,21 +1303,21 @@ Lemma f2b_determinacy_inv: (t' = E0 /\ t'' = E0 /\ s2' = s2'') \/ (t' <> E0 /\ t'' <> E0 /\ match_traces (symbolenv L1) t' t''). Proof. - intros. + intros. assert (match_traces (symbolenv L2) t' t''). - eapply sd_determ_1; eauto. + eapply sd_determ_1; eauto. destruct (silent_or_not_silent t'). - subst. inv H1. + subst. inv H1. left; intuition. eapply sd_determ_2; eauto. destruct (silent_or_not_silent t''). - subst. inv H1. elim H2; auto. - right; intuition. - eapply match_traces_preserved with (ge1 := (symbolenv L2)); auto. - intros; symmetry; apply (fsim_public_preserved FS). + subst. inv H1. elim H2; auto. + right; intuition. + eapply match_traces_preserved with (ge1 := (symbolenv L2)); auto. + intros; symmetry; apply (fsim_public_preserved FS). Qed. Lemma f2b_determinacy_star: - forall s s1, Star L2 s E0 s1 -> + forall s s1, Star L2 s E0 s1 -> forall t s2 s3, Step L2 s1 t s2 -> t <> E0 -> Star L2 s t s3 -> @@ -1327,7 +1327,7 @@ Proof. intros. inv H3. congruence. exploit f2b_determinacy_inv. eexact H. eexact H4. intros [[EQ1 [EQ2 EQ3]] | [NEQ1 [NEQ2 MT]]]. - subst. simpl in *. eauto. + subst. simpl in *. eauto. congruence. Qed. @@ -1352,10 +1352,10 @@ Lemma wf_f2b_order: Proof. assert (ACC1: forall n, Acc f2b_order (F2BI_before n)). intros n0; pattern n0; apply lt_wf_ind; intros. - constructor; intros. inv H0. auto. + constructor; intros. inv H0. auto. assert (ACC2: forall n, Acc f2b_order (F2BI_after n)). intros n0; pattern n0; apply lt_wf_ind; intros. - constructor; intros. inv H0. auto. auto. + constructor; intros. inv H0. auto. auto. red; intros. destruct a; auto. Qed. @@ -1382,7 +1382,7 @@ Remark f2b_match_after': FS i s1 s2a -> f2b_match_states (F2BI_after n) s1 s2. Proof. - intros. inv H. + intros. inv H. econstructor; eauto. econstructor; eauto. econstructor; eauto. Qed. @@ -1403,7 +1403,7 @@ Proof. (* 1.1 L1 can reach final state and L2 is at final state: impossible! *) exploit (sd_final_nostep L2_determinate); eauto. contradiction. (* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *) - inv H2. + inv H2. exploit f2b_determinacy_inv. eexact H5. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. (* 1.2.1 L2 makes a silent transition *) @@ -1417,24 +1417,24 @@ Proof. subst. simpl in *. destruct (star_starN H6) as [n STEPS2]. exists (F2BI_before n); exists s1'; split. right; split. auto. constructor. - econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. + econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. (* 1.2.2 L2 makes a non-silent transition, and so does L1 *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. - subst t2. rewrite E0_right in H1. + subst t2. rewrite E0_right in H1. (* Use receptiveness to equate the traces *) exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1]. - exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. + exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. intros [i''' [s2''' [P Q]]]. inv P. (* Exploit determinacy *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. - subst t0. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. + subst t0. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. intros. elim NOT2. inv H8. auto. - subst t2. rewrite E0_right in *. - assert (s4 = s2'). eapply sd_determ_2; eauto. subst s4. + subst t2. rewrite E0_right in *. + assert (s4 = s2'). eapply sd_determ_2; eauto. subst s4. (* Perform transition now and go to "after" state *) destruct (star_starN H7) as [n STEPS2]. exists (F2BI_after n); exists s1'''; split. - left. eapply plus_right; eauto. + left. eapply plus_right; eauto. eapply f2b_match_after'; eauto. (* 2. Before *) @@ -1444,22 +1444,22 @@ Proof. (* 2.1 L2 makes a silent transition: remain in "before" state *) subst. simpl in *. exists (F2BI_before n0); exists s1; split. right; split. apply star_refl. constructor. omega. - econstructor; eauto. eapply star_right; eauto. + econstructor; eauto. eapply star_right; eauto. (* 2.2 L2 make a non-silent transition *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. congruence. subst. rewrite E0_right in *. (* Use receptiveness to equate the traces *) exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1]. - exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. + exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto. intros [i''' [s2''' [P Q]]]. (* Exploit determinacy *) - exploit f2b_determinacy_star. eauto. eexact STEP2. auto. apply plus_star; eauto. - intro R. inv R. congruence. + exploit f2b_determinacy_star. eauto. eexact STEP2. auto. apply plus_star; eauto. + intro R. inv R. congruence. exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. - subst. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. - intros. elim NOT2. inv H7; auto. - subst. rewrite E0_right in *. + subst. simpl in *. exploit sd_determ_1. eauto. eexact STEP2. eexact H2. + intros. elim NOT2. inv H7; auto. + subst. rewrite E0_right in *. assert (s3 = s2'). eapply sd_determ_2; eauto. subst s3. (* Perform transition now and go to "after" state *) destruct (star_starN H6) as [n STEPS2]. exists (F2BI_after n); exists s1'''; split. @@ -1467,7 +1467,7 @@ Proof. eapply f2b_match_after'; eauto. (* 3. After *) - inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. + inv H. exploit Eapp_E0_inv; eauto. intros [EQ1 EQ2]; subst. exploit f2b_determinacy_inv. eexact H2. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. subst. exists (F2BI_after n); exists s1; split. @@ -1498,9 +1498,9 @@ Proof. inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction. inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction. (* progress *) - intros. inv H. - exploit f2b_progress; eauto. intros TRANS; inv TRANS. - left; exists r; auto. + intros. inv H. + exploit f2b_progress; eauto. intros TRANS; inv TRANS. + left; exists r; auto. inv H3. right; econstructor; econstructor; eauto. inv H4. congruence. right; econstructor; econstructor; eauto. inv H1. right; econstructor; econstructor; eauto. @@ -1566,20 +1566,20 @@ Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop := ffs_match i (ev :: t, s1) s2. Lemma star_non_E0_split': - forall s2 t s2', Star L2 s2 t s2' -> + forall s2 t s2', Star L2 s2 t s2' -> match t with | nil => True | ev :: t' => exists s2x, Plus L2 s2 (ev :: nil) s2x /\ Star L2 s2x t' s2' end. Proof. induction 1. simpl. auto. - exploit L2single; eauto. intros LEN. - destruct t1. simpl in *. subst. destruct t2. auto. + exploit L2single; eauto. intros LEN. + destruct t1. simpl in *. subst. destruct t2. auto. destruct IHstar as [s2x [A B]]. exists s2x; split; auto. - eapply plus_left. eauto. apply plus_star; eauto. auto. + eapply plus_left. eauto. apply plus_star; eauto. auto. destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto. simpl in LEN. omegaContradiction. -Qed. +Qed. Lemma ffs_simulation: forall s1 t s1', Step (atomic L1) s1 t s1' -> @@ -1590,27 +1590,27 @@ Lemma ffs_simulation: Proof. induction 1; intros. (* silent step *) - inv H0. - exploit (fsim_simulation sim); eauto. - intros [i' [s2' [A B]]]. + inv H0. + exploit (fsim_simulation sim); eauto. + intros [i' [s2' [A B]]]. exists i'; exists s2'; split. auto. constructor; auto. (* start step *) - inv H0. - exploit (fsim_simulation sim); eauto. + inv H0. + exploit (fsim_simulation sim); eauto. intros [i' [s2' [A B]]]. - destruct t as [ | ev' t]. + destruct t as [ | ev' t]. (* single event *) exists i'; exists s2'; split. auto. constructor; auto. (* multiple events *) - assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto. - exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. + assert (C: Star L2 s2 (ev :: ev' :: t) s2'). intuition. apply plus_star; auto. + exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. exists i'; exists s2x; split. auto. econstructor; eauto. (* continue step *) - inv H0. - exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. - destruct t. - exists i; exists s2'; split. left. eapply plus_star_trans; eauto. constructor; auto. - exists i; exists s2x; split. auto. econstructor; eauto. + inv H0. + exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. + destruct t. + exists i; exists s2'; split. left. eapply plus_star_trans; eauto. constructor; auto. + exists i; exists s2x; split. auto. econstructor; eauto. Qed. Theorem factor_forward_simulation: @@ -1620,11 +1620,11 @@ Proof. (* wf *) apply fsim_order_wf. (* initial states *) - intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst. - exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]]. + intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst. + exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]]. exists i; exists s2; split; auto. constructor; auto. (* final states *) - intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H. + intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H. eapply (fsim_match_final_states sim); eauto. (* simulation *) exact ffs_simulation. @@ -1661,47 +1661,47 @@ Proof. induction 1; intros. (* silent step *) inv H0. - exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. + exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. intros [i' [s1'' [A B]]]. exists i'; exists s1''; split. - destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto. + destruct A as [P | [P Q]]. left. eapply star_plus_trans; eauto. right; split; auto. eapply star_trans; eauto. econstructor. apply star_refl. auto. auto. (* start step *) inv H0. - exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. + exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. intros [i' [s1'' [A B]]]. assert (C: Star L1 s1 (ev :: t) s1''). - eapply star_trans. eauto. destruct A as [P | [P Q]]. apply plus_star; eauto. eauto. auto. + eapply star_trans. eauto. destruct A as [P | [P Q]]. apply plus_star; eauto. eauto. auto. exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]]. exists i'; exists s1x; split. left; auto. econstructor; eauto. - exploit L2wb; eauto. + exploit L2wb; eauto. (* continue step *) inv H0. unfold E0 in H8; destruct H8; try congruence. exploit star_non_E0_split'; eauto. simpl. intros [s1x [P Q]]. - exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto. + exists i; exists s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto. Qed. Lemma fbs_progress: - forall i s1 s2, + forall i s1 s2, fbs_match i s1 s2 -> safe L1 s1 -> (exists r, final_state (atomic L2) s2 r) \/ (exists t, exists s2', Step (atomic L2) s2 t s2'). Proof. - intros. inv H. destruct t. + intros. inv H. destruct t. (* 1. no buffered events *) exploit (bsim_progress sim); eauto. eapply star_safe; eauto. - intros [[r A] | [t [s2' A]]]. + intros [[r A] | [t [s2' A]]]. (* final state *) left; exists r; simpl; auto. -(* L2 can step *) - destruct t. +(* L2 can step *) + destruct t. right; exists E0; exists (nil, s2'). constructor. auto. right; exists (e :: nil); exists (t, s2'). constructor. auto. (* 2. some buffered events *) - unfold E0 in H3; destruct H3. congruence. - right; exists (e :: nil); exists (t, s3). constructor. auto. + unfold E0 in H3; destruct H3. congruence. + right; exists (e :: nil); exists (t, s3). constructor. auto. Qed. Theorem factor_backward_simulation: @@ -1712,14 +1712,14 @@ Proof. apply bsim_order_wf. (* initial states exist *) intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A]. - exists (E0, s2). simpl; auto. + exists (E0, s2). simpl; auto. (* initial states match *) intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst. - exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]]. + exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]]. exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto. (* final states match *) intros. destruct s2 as [t s2]; simpl in H1; destruct H1; subst. - inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto. + inv H. exploit (bsim_match_final_states sim); eauto. eapply star_safe; eauto. intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto. (* progress *) exact fbs_progress. @@ -1748,19 +1748,19 @@ Theorem atomic_receptive: Proof. intros. constructor; intros. (* receptive *) - inv H0. + inv H0. (* silent step *) inv H1. exists (E0, s'). constructor; auto. (* start step *) - assert (exists ev2, t2 = ev2 :: nil). inv H1; econstructor; eauto. + assert (exists ev2, t2 = ev2 :: nil). inv H1; econstructor; eauto. destruct H0 as [ev2 EQ]; subst t2. exploit ssr_receptive; eauto. intros [s2 [t2 P]]. - exploit ssr_well_behaved. eauto. eexact P. simpl; intros Q. + exploit ssr_well_behaved. eauto. eexact P. simpl; intros Q. exists (t2, s2). constructor; auto. (* continue step *) - simpl in H2; destruct H2. + simpl in H2; destruct H2. assert (t2 = ev :: nil). inv H1; simpl in H0; tauto. - subst t2. exists (t, s0). constructor; auto. simpl; auto. + subst t2. exists (t, s0). constructor; auto. simpl; auto. (* single-event *) red. intros. inv H0; simpl; omega. Qed. -- cgit