diff options
| -rw-r--r-- | common/Behaviors.v | 96 | ||||
| -rw-r--r-- | common/Smallstep.v | 530 |
2 files changed, 323 insertions, 303 deletions
diff --git a/common/Behaviors.v b/common/Behaviors.v index 1a6b8bd6..ef99b205 100644 --- a/common/Behaviors.v +++ b/common/Behaviors.v @@ -281,31 +281,29 @@ End PROGRAM_BEHAVIORS. Section FORWARD_SIMULATIONS. -Variable L1: semantics. -Variable L2: semantics. -Variable S: forward_simulation L1 L2. +Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states). Lemma forward_simulation_state_behaves: forall i s1 s2 beh1, - S i s1 s2 -> state_behaves L1 s1 beh1 -> + match_states i s1 s2 -> state_behaves L1 s1 beh1 -> exists beh2, state_behaves L2 s2 beh2 /\ behavior_improves beh1 beh2. Proof. intros. inv H0. -(* termination *) +- (* termination *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. exists (Terminates t r); split. econstructor; eauto. eapply fsim_match_final_states; eauto. apply behavior_improves_refl. -(* silent divergence *) +- (* silent divergence *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. exists (Diverges t); split. econstructor; eauto. eapply simulation_forever_silent; eauto. apply behavior_improves_refl. -(* reactive divergence *) +- (* reactive divergence *) exists (Reacts T); split. econstructor. eapply simulation_forever_reactive; eauto. apply behavior_improves_refl. -(* going wrong *) +- (* going wrong *) exploit simulation_star; eauto. intros [i' [s2' [A B]]]. destruct (state_behaves_exists L2 s2') as [beh' SB]. exists (behavior_app t beh'); split. @@ -315,16 +313,19 @@ Proof. simpl. decEq. traceEq. Qed. +End FORWARD_SIMULATIONS. + Theorem forward_simulation_behavior_improves: + forall L1 L2, forward_simulation L1 L2 -> forall beh1, program_behaves L1 beh1 -> exists beh2, program_behaves L2 beh2 /\ behavior_improves beh1 beh2. Proof. - intros. inv H. -(* initial state defined *) + intros L1 L2 FS. destruct FS as [init order match_states S]. intros. inv H. +- (* initial state defined *) exploit (fsim_match_initial_states S); eauto. intros [i [s' [INIT MATCH]]]. exploit forward_simulation_state_behaves; eauto. intros [beh2 [A B]]. exists beh2; split; auto. econstructor; eauto. -(* initial state undefined *) +- (* initial state undefined *) destruct (classic (exists s', initial_state L2 s')). destruct H as [s' INIT]. destruct (state_behaves_exists L2 s') as [beh' SB]. @@ -336,6 +337,7 @@ Proof. Qed. Corollary forward_simulation_same_safe_behavior: + forall L1 L2, forward_simulation L1 L2 -> forall beh, program_behaves L1 beh -> not_wrong beh -> program_behaves L2 beh. @@ -343,18 +345,14 @@ Proof. intros. exploit forward_simulation_behavior_improves; eauto. intros [beh' [A B]]. destruct B. congruence. - destruct H1 as [t [C D]]. subst. contradiction. + destruct H2 as [t [C D]]. subst. contradiction. Qed. -End FORWARD_SIMULATIONS. - (** * Backward simulations and program behaviors *) Section BACKWARD_SIMULATIONS. -Variable L1: semantics. -Variable L2: semantics. -Variable S: backward_simulation L1 L2. +Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states). Definition safe_along_behavior (s: state L1) (b: program_behavior) : Prop := forall t1 s' b2, Star L1 s t1 s' -> b = behavior_app t1 b2 -> @@ -402,8 +400,8 @@ Qed. Lemma backward_simulation_star: forall s2 t s2', Star L2 s2 t s2' -> - forall i s1 b, S i s1 s2 -> safe_along_behavior s1 (behavior_app t b) -> - exists i', exists s1', Star L1 s1 t s1' /\ S i' s1' s2'. + forall i s1 b, match_states i s1 s2 -> safe_along_behavior s1 (behavior_app t b) -> + exists i', exists s1', Star L1 s1 t s1' /\ match_states i' s1' s2'. Proof. induction 1; intros. exists i; exists s1; split; auto. apply star_refl. @@ -418,12 +416,12 @@ Qed. Lemma backward_simulation_forever_silent: forall i s1 s2, - Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> + Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 -> Forever_silent L1 s1. Proof. assert (forall i s1 s2, - Forever_silent L2 s2 -> S i s1 s2 -> safe L1 s1 -> - forever_silent_N (step L1) (bsim_order S) (globalenv L1) i s1). + Forever_silent L2 s2 -> match_states i s1 s2 -> safe L1 s1 -> + forever_silent_N (step L1) order (globalenv L1) i s1). cofix COINDHYP; intros. inv H. destruct (bsim_simulation S _ _ _ H2 _ H0 H1) as [i' [s2' [A B]]]. destruct A as [C | [C D]]. @@ -431,29 +429,29 @@ Proof. eapply star_safe; eauto. apply plus_star; auto. eapply forever_silent_N_star; eauto. eapply COINDHYP; eauto. eapply star_safe; eauto. - intros. eapply forever_silent_N_forever; eauto. apply bsim_order_wf. + intros. eapply forever_silent_N_forever; eauto. eapply bsim_order_wf; eauto. Qed. Lemma backward_simulation_forever_reactive: forall i s1 s2 T, - Forever_reactive L2 s2 T -> S i s1 s2 -> safe_along_behavior s1 (Reacts T) -> + Forever_reactive L2 s2 T -> match_states i s1 s2 -> safe_along_behavior s1 (Reacts T) -> Forever_reactive L1 s1 T. Proof. cofix COINDHYP; intros. inv H. - destruct (backward_simulation_star H2 _ (Reacts T0) H0) as [i' [s1' [A B]]]; eauto. + destruct (backward_simulation_star H2 (Reacts T0) H0) as [i' [s1' [A B]]]; eauto. econstructor; eauto. eapply COINDHYP; eauto. eapply star_safe_along; eauto. Qed. Lemma backward_simulation_state_behaves: forall i s1 s2 beh2, - S i s1 s2 -> state_behaves L2 s2 beh2 -> + match_states i s1 s2 -> state_behaves L2 s2 beh2 -> exists beh1, state_behaves L1 s1 beh1 /\ behavior_improves beh1 beh2. Proof. intros. destruct (classic (safe_along_behavior s1 beh2)). -(* 1. Safe along *) +- (* 1. Safe along *) exists beh2; split; [idtac|apply behavior_improves_refl]. inv H0. -(* termination *) ++ (* termination *) assert (Terminates t r = behavior_app t (Terminates E0 r)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -463,7 +461,7 @@ Proof. eapply safe_along_safe. eapply star_safe_along; eauto. intros [s1'' [C D]]. econstructor. eapply star_trans; eauto. traceEq. auto. -(* silent divergence *) ++ (* silent divergence *) assert (Diverges t = behavior_app t (Diverges E0)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -471,9 +469,9 @@ Proof. intros [i' [s1' [A B]]]. econstructor. eauto. eapply backward_simulation_forever_silent; eauto. eapply safe_along_safe. eapply star_safe_along; eauto. -(* reactive divergence *) ++ (* reactive divergence *) econstructor. eapply backward_simulation_forever_reactive; eauto. -(* goes wrong *) ++ (* goes wrong *) assert (Goes_wrong t = behavior_app t (Goes_wrong E0)). simpl. rewrite E0_right; auto. rewrite H0 in H1. @@ -484,7 +482,7 @@ Proof. elim (H4 _ FIN). elim (H3 _ _ STEP2). -(* 2. Not safe along *) +- (* 2. Not safe along *) exploit not_safe_along_behavior; eauto. intros [t [s1' [PREF [STEPS [NOSTEP NOFIN]]]]]. exists (Goes_wrong t); split. @@ -492,23 +490,26 @@ Proof. right. exists t; auto. Qed. +End BACKWARD_SIMULATIONS. + Theorem backward_simulation_behavior_improves: + forall L1 L2, backward_simulation L1 L2 -> forall beh2, program_behaves L2 beh2 -> exists beh1, program_behaves L1 beh1 /\ behavior_improves beh1 beh2. Proof. - intros. inv H. -(* L2's initial state is defined. *) + intros L1 L2 S beh2 H. destruct S as [index order match_states S]. inv H. +- (* L2's initial state is defined. *) destruct (classic (exists s1, initial_state L1 s1)) as [[s1 INIT] | NOINIT]. -(* L1's initial state is defined too. *) ++ (* L1's initial state is defined too. *) exploit (bsim_match_initial_states S); eauto. intros [i [s1' [INIT1' MATCH]]]. exploit backward_simulation_state_behaves; eauto. intros [beh1 [A B]]. exists beh1; split; auto. econstructor; eauto. -(* L1 has no initial state *) ++ (* L1 has no initial state *) exists (Goes_wrong E0); split. apply program_goes_initially_wrong. intros; red; intros. elim NOINIT; exists s0; auto. apply behavior_improves_bot. -(* L2 has no initial state *) +- (* L2 has no initial state *) exists (Goes_wrong E0); split. apply program_goes_initially_wrong. intros; red; intros. @@ -518,17 +519,16 @@ Proof. Qed. Corollary backward_simulation_same_safe_behavior: + forall L1 L2, backward_simulation L1 L2 -> (forall beh, program_behaves L1 beh -> not_wrong beh) -> (forall beh, program_behaves L2 beh -> program_behaves L1 beh). Proof. intros. exploit backward_simulation_behavior_improves; eauto. intros [beh' [A B]]. destruct B. congruence. - destruct H1 as [t [C D]]. subst. elim (H (Goes_wrong t)). auto. + destruct H2 as [t [C D]]. subst. elim (H0 (Goes_wrong t)). auto. Qed. -End BACKWARD_SIMULATIONS. - (** * Program behaviors for the "atomic" construction *) Section ATOMIC. @@ -635,7 +635,7 @@ Theorem atomic_behaviors: forall beh, program_behaves L beh <-> program_behaves (atomic L) beh. Proof. intros; split; intros. - (* L -> atomic L *) +- (* L -> atomic L *) exploit forward_simulation_behavior_improves. eapply atomic_forward_simulation. eauto. intros [beh2 [A B]]. red in B. destruct B as [EQ | [t [C D]]]. congruence. @@ -646,23 +646,23 @@ Proof. intros; red; intros. simpl in H. destruct H. eelim H4; eauto. apply program_goes_initially_wrong. intros; red; intros. simpl in H; destruct H. eelim H1; eauto. - (* atomic L -> L *) +- (* atomic L -> L *) inv H. - (* initial state defined *) ++ (* initial state defined *) destruct s as [t s]. simpl in H0. destruct H0; subst t. apply program_runs with s; auto. inv H1. - (* termination *) +* (* termination *) destruct s' as [t' s']. simpl in H2; destruct H2; subst t'. econstructor. eapply atomic_star_star; eauto. auto. - (* silent divergence *) +* (* silent divergence *) destruct s' as [t' s']. assert (t' = E0). inv H2. inv H1; auto. subst t'. econstructor. eapply atomic_star_star; eauto. change s' with (snd (E0,s')). apply atomic_forever_silent_forever_silent. auto. - (* reactive divergence *) +* (* reactive divergence *) econstructor. apply atomic_forever_reactive_forever_reactive. auto. - (* going wrong *) +* (* going wrong *) destruct s' as [t' s']. assert (t' = E0). destruct t'; auto. eelim H2. simpl. apply atomic_step_continue. @@ -672,7 +672,7 @@ Proof. elim (H2 E0 (E0,s'0)). constructor; auto. elim (H2 (e::nil) (t0,s'0)). constructor; auto. intros; red; intros. elim (H3 r). simpl; auto. - (* initial state undefined *) ++ (* initial state undefined *) apply program_goes_initially_wrong. intros; red; intros. elim (H0 (E0,s)); simpl; auto. Qed. diff --git a/common/Smallstep.v b/common/Smallstep.v index 71cef35f..9c91243a 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -513,43 +513,49 @@ Open Scope smallstep_scope. (** The general form of a forward simulation. *) -Record forward_simulation (L1 L2: semantics) : Type := - Forward_simulation { - fsim_index: Type; - fsim_order: fsim_index -> fsim_index -> Prop; - fsim_order_wf: well_founded fsim_order; - fsim_match_states :> fsim_index -> state L1 -> state L2 -> Prop; +Record fsim_properties (L1 L2: semantics) (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) : Prop := { + fsim_order_wf: well_founded order; fsim_match_initial_states: forall s1, initial_state L1 s1 -> - exists i, exists s2, initial_state L2 s2 /\ fsim_match_states i s1 s2; + exists i, exists s2, initial_state L2 s2 /\ match_states i s1 s2; fsim_match_final_states: forall i s1 s2 r, - fsim_match_states i s1 s2 -> final_state L1 s1 r -> final_state L2 s2 r; + 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' -> - forall i s2, fsim_match_states i s1 s2 -> + forall i s2, match_states i s1 s2 -> exists i', exists s2', - (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ fsim_order i' i)) - /\ fsim_match_states i' s1' s2'; + (Plus L2 s2 t s2' \/ (Star L2 s2 t s2' /\ order i' i)) + /\ match_states i' s1' s2'; fsim_public_preserved: forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id }. -Implicit Arguments forward_simulation []. +Arguments fsim_properties: clear implicits. + +Inductive forward_simulation (L1 L2: semantics) : Prop := + Forward_simulation (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) + (props: fsim_properties L1 L2 index order match_states). + +Arguments Forward_simulation {L1 L2 index} order match_states props. (** An alternate form of the simulation diagram *) Lemma fsim_simulation': - forall L1 L2 (S: forward_simulation L1 L2), + forall L1 L2 index order match_states, fsim_properties L1 L2 index order match_states -> forall i s1 t s1', Step L1 s1 t s1' -> - forall s2, S i s1 s2 -> - (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). + forall s2, match_states i s1 s2 -> + (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2') + \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1' s2). Proof. intros. exploit fsim_simulation; eauto. intros [i' [s2' [A B]]]. intuition. left; exists i'; exists s2'; auto. - inv H2. + inv H3. right; exists i'; auto. left; exists i'; exists s2'; split; auto. econstructor; eauto. Qed. @@ -602,15 +608,15 @@ Hypothesis simulation: Lemma forward_simulation_star_wf: forward_simulation L1 L2. Proof. - apply Forward_simulation with - (fsim_order := order) - (fsim_match_states := fun idx s1 s2 => idx = s1 /\ match_states s1 s2); - auto. - intros. exploit match_initial_states; eauto. intros [s2 [A B]]. + apply Forward_simulation with order (fun idx s1 s2 => idx = s1 /\ match_states s1 s2); + constructor. +- auto. +- intros. exploit match_initial_states; eauto. intros [s2 [A B]]. exists s1; exists s2; auto. - intros. destruct H. eapply match_final_states; eauto. - intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]]. - exists s1'; exists s2'; intuition. +- intros. destruct H. eapply match_final_states; eauto. +- intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]]. + exists s1'; exists s2'; intuition auto. +- auto. Qed. End SIMULATION_STAR_WF. @@ -709,28 +715,26 @@ End FORWARD_SIMU_DIAGRAMS. Section SIMULATION_SEQUENCES. -Variable L1: semantics. -Variable L2: semantics. -Variable S: forward_simulation L1 L2. +Context L1 L2 index order match_states (S: fsim_properties L1 L2 index order match_states). Lemma simulation_star: forall s1 t s1', Star L1 s1 t s1' -> - forall i s2, S i s1 s2 -> - exists i', exists s2', Star L2 s2 t s2' /\ S i' s1' s2'. + forall i s2, match_states i s1 s2 -> + exists i', exists s2', Star L2 s2 t s2' /\ match_states i' s1' s2'. Proof. induction 1; intros. exists i; exists s2; split; auto. apply star_refl. 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 auto. apply plus_star; auto. Qed. Lemma simulation_plus: forall s1 t s1', Plus L1 s1 t s1' -> - forall i s2, S i s1 s2 -> - (exists i', exists s2', Plus L2 s2 t s2' /\ S i' s1' s2') - \/ (exists i', clos_trans _ (fsim_order S) i' i /\ t = E0 /\ S i' s1' s2). + forall i s2, match_states i s1 s2 -> + (exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2') + \/ (exists i', clos_trans _ order i' i /\ t = E0 /\ match_states i' s1' s2). Proof. induction 1 using plus_ind2; intros. (* base case *) @@ -744,34 +748,34 @@ Proof. left; exists i''; exists s2''; split; auto. eapply plus_star_trans; eauto. exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]]. subst. simpl. left; exists i''; exists s2''; auto. - subst. simpl. right; exists i''; intuition. + subst. simpl. right; exists i''; intuition auto. eapply t_trans; eauto. eapply t_step; eauto. Qed. Lemma simulation_forever_silent: forall i s1 s2, - Forever_silent L1 s1 -> S i s1 s2 -> + Forever_silent L1 s1 -> match_states i s1 s2 -> Forever_silent L2 s2. Proof. assert (forall i s1 s2, - Forever_silent L1 s1 -> S i s1 s2 -> - forever_silent_N (step L2) (fsim_order S) (globalenv L2) i s2). + Forever_silent L1 s1 -> match_states i s1 s2 -> + forever_silent_N (step L2) order (globalenv L2) i s2). cofix COINDHYP; intros. inv H. destruct (fsim_simulation S _ _ _ H1 _ _ H0) as [i' [s2' [A B]]]. destruct A as [C | [C D]]. eapply forever_silent_N_plus; eauto. eapply forever_silent_N_star; eauto. - intros. eapply forever_silent_N_forever; eauto. apply fsim_order_wf. + intros. eapply forever_silent_N_forever; eauto. eapply fsim_order_wf; eauto. Qed. Lemma simulation_forever_reactive: forall i s1 s2 T, - Forever_reactive L1 s1 T -> S i s1 s2 -> + Forever_reactive L1 s1 T -> match_states i s1 s2 -> Forever_reactive L2 s2 T. Proof. cofix COINDHYP; intros. inv H. - destruct (simulation_star H1 i _ H0) as [i' [st2' [A B]]]. + edestruct simulation_star as [i' [st2' [A B]]]; eauto. econstructor; eauto. Qed. @@ -779,56 +783,48 @@ End SIMULATION_SEQUENCES. (** ** Composing two forward simulations *) -Section COMPOSE_SIMULATIONS. - -Variable L1: semantics. -Variable L2: semantics. -Variable L3: semantics. -Variable S12: forward_simulation L1 L2. -Variable S23: forward_simulation L2 L3. - -Let ff_index : Type := (fsim_index S23 * fsim_index S12)%type. - -Let ff_order : ff_index -> ff_index -> Prop := - lex_ord (clos_trans _ (fsim_order S23)) (fsim_order S12). - -Let ff_match_states (i: ff_index) (s1: state L1) (s3: state L3) : Prop := - exists s2, S12 (snd i) s1 s2 /\ S23 (fst i) s2 s3. - -Lemma compose_forward_simulation: forward_simulation L1 L3. -Proof. - apply Forward_simulation with (fsim_order := ff_order) (fsim_match_states := ff_match_states). -(* well founded *) - unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. apply fsim_order_wf. apply fsim_order_wf. -(* 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]]]. +Lemma compose_forward_simulations: + forall L1 L2 L3, forward_simulation L1 L2 -> forward_simulation L2 L3 -> forward_simulation L1 L3. +Proof. + intros L1 L2 L3 S12 S23. + destruct S12 as [index order match_states props]. + destruct S23 as [index' order' match_states' props']. + + set (ff_index := (index' * index)%type). + set (ff_order := lex_ord (clos_trans _ order') order). + set (ff_match_states := fun (i: ff_index) (s1: state L1) (s3: state L3) => + exists s2, match_states (snd i) s1 s2 /\ match_states' (fst i) s2 s3). + apply Forward_simulation with ff_order ff_match_states; constructor. +- (* well founded *) + unfold ff_order. apply wf_lex_ord. apply wf_clos_trans. + eapply fsim_order_wf; eauto. eapply fsim_order_wf; eauto. +- (* initial states *) + intros. exploit (fsim_match_initial_states props); eauto. intros [i [s2 [A B]]]. + exploit (fsim_match_initial_states props'); eauto. intros [i' [s3 [C D]]]. exists (i', i); exists s3; split; auto. exists s2; auto. -(* final states *) +- (* final states *) intros. destruct H as [s3 [A B]]. - eapply (fsim_match_final_states S23); eauto. - eapply (fsim_match_final_states S12); eauto. -(* simulation *) + eapply (fsim_match_final_states props'); eauto. + eapply (fsim_match_final_states props); eauto. +- (* simulation *) intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in *. - exploit (fsim_simulation' S12); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]]. - (* L2 makes one or several steps. *) + exploit (fsim_simulation' props); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]]. ++ (* L2 makes one or several steps. *) exploit simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]]. - (* L3 makes one or several steps *) +* (* L3 makes one or several steps *) exists (i2', i1'); exists s2'; split. auto. exists s3'; auto. - (* L3 makes no step *) +* (* L3 makes no step *) exists (i2', i1'); exists s2; split. right; split. subst t; apply star_refl. red. left. auto. exists s3'; auto. - (* L2 makes no step *) ++ (* L2 makes no step *) exists (i2, i1'); exists s2; split. 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. +- (* symbols *) + intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply fsim_public_preserved; eauto. Qed. -End COMPOSE_SIMULATIONS. - (** * Receptiveness and determinacy *) Definition single_events (L: semantics) : Prop := @@ -916,49 +912,57 @@ Qed. (** The general form of a backward simulation. *) -Record backward_simulation (L1 L2: semantics) : Type := - Backward_simulation { - bsim_index: Type; - bsim_order: bsim_index -> bsim_index -> Prop; - bsim_order_wf: well_founded bsim_order; - bsim_match_states :> bsim_index -> state L1 -> state L2 -> Prop; +Record bsim_properties (L1 L2: semantics) (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) : Prop := { + bsim_order_wf: well_founded order; bsim_initial_states_exist: forall s1, initial_state L1 s1 -> exists s2, initial_state L2 s2; bsim_match_initial_states: 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; + exists i, exists s1', initial_state L1 s1' /\ 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 -> + 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, - bsim_match_states i s1 s2 -> safe L1 s1 -> + match_states i s1 s2 -> safe L1 s1 -> (exists r, final_state L2 s2 r) \/ (exists t, exists s2', Step L2 s2 t s2'); bsim_simulation: forall s2 t s2', Step L2 s2 t s2' -> - forall i s1, bsim_match_states i s1 s2 -> safe L1 s1 -> + forall i s1, match_states i s1 s2 -> safe L1 s1 -> exists i', exists s1', - (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order i' i)) - /\ bsim_match_states i' s1' s2'; + (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i)) + /\ match_states i' s1' s2'; bsim_public_preserved: forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id }. +Arguments bsim_properties: clear implicits. + +Inductive backward_simulation (L1 L2: semantics) : Prop := + Backward_simulation (index: Type) + (order: index -> index -> Prop) + (match_states: index -> state L1 -> state L2 -> Prop) + (props: bsim_properties L1 L2 index order match_states). + +Arguments Backward_simulation {L1 L2 index} order match_states props. + (** An alternate form of the simulation diagram *) Lemma bsim_simulation': - forall L1 L2 (S: backward_simulation L1 L2), + forall L1 L2 index order match_states, bsim_properties L1 L2 index order match_states -> forall i s2 t s2', Step L2 s2 t s2' -> - forall s1, S i s1 s2 -> safe L1 s1 -> - (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'). + forall s1, match_states i s1 s2 -> safe L1 s1 -> + (exists i', exists s1', Plus L1 s1 t s1' /\ match_states i' s1' s2') + \/ (exists i', order i' i /\ t = E0 /\ match_states i' s1 s2'). Proof. intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]]. intuition. left; exists i'; exists s1'; auto. - inv H3. + inv H4. right; exists i'; auto. left; exists i'; exists s1'; split; auto. econstructor; eauto. Qed. @@ -1004,13 +1008,13 @@ Hypothesis simulation: Lemma backward_simulation_plus: backward_simulation L1 L2. Proof. apply Backward_simulation with - (bsim_order := fun (x y: unit) => False) - (bsim_match_states := fun (i: unit) s1 s2 => match_states s1 s2); - 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]]. + (fun (x y: unit) => False) + (fun (i: unit) s1 s2 => match_states s1 s2); + constructor; 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]]. exists tt; exists s1'; auto. Qed. @@ -1022,19 +1026,17 @@ End BACKWARD_SIMU_DIAGRAMS. Section BACKWARD_SIMULATION_SEQUENCES. -Variable L1: semantics. -Variable L2: semantics. -Variable S: backward_simulation L1 L2. +Context L1 L2 index order match_states (S: bsim_properties L1 L2 index order match_states). Lemma bsim_E0_star: forall s2 s2', Star L2 s2 E0 s2' -> - forall i s1, S i s1 s2 -> safe L1 s1 -> - exists i', exists s1', Star L1 s1 E0 s1' /\ S i' s1' s2'. + forall i s1, match_states i s1 s2 -> safe L1 s1 -> + exists i', exists s1', Star L1 s1 E0 s1' /\ match_states i' s1' s2'. Proof. intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto. -(* base case *) +- (* base case *) intros. exists i; exists s1; split; auto. apply star_refl. -(* inductive case *) +- (* inductive case *) intros. exploit bsim_simulation; eauto. intros [i' [s1' [A B]]]. assert (Star L1 s0 E0 s1'). intuition. apply plus_star; auto. exploit H0. eauto. eapply star_safe; eauto. intros [i'' [s1'' [C D]]]. @@ -1043,7 +1045,7 @@ Qed. Lemma bsim_safe: forall i s1 s2, - S i s1 s2 -> safe L1 s1 -> safe L2 s2. + match_states i s1 s2 -> safe L1 s1 -> safe L2 s2. Proof. intros; red; intros. exploit bsim_E0_star; eauto. intros [i' [s1' [A B]]]. @@ -1052,22 +1054,22 @@ Qed. Lemma bsim_E0_plus: forall s2 t s2', Plus L2 s2 t s2' -> t = E0 -> - forall i s1, S i s1 s2 -> safe L1 s1 -> - (exists i', exists s1', Plus L1 s1 E0 s1' /\ S i' s1' s2') - \/ (exists i', clos_trans _ (bsim_order S) i' i /\ S i' s1 s2'). + forall i s1, match_states i s1 s2 -> safe L1 s1 -> + (exists i', exists s1', Plus L1 s1 E0 s1' /\ match_states i' s1' s2') + \/ (exists i', clos_trans _ order i' i /\ match_states i' s1 s2'). Proof. induction 1 using plus_ind2; intros; subst t. -(* base case *) +- (* base case *) exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]]. - left; exists i'; exists s1'; auto. - right; exists i'; intuition. -(* inductive case *) ++ left; exists i'; exists s1'; auto. ++ right; exists i'; intuition. +- (* inductive case *) 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. ++ 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. - exploit IHplus; eauto. intros [P | [i'' [P Q]]]. ++ exploit IHplus; eauto. intros [P | [i'' [P Q]]]. left; auto. right; exists i''; intuition. eapply t_trans; eauto. apply t_step; auto. Qed. @@ -1098,21 +1100,20 @@ Variable L1: semantics. Variable L2: semantics. Variable L3: semantics. Hypothesis L3_single_events: single_events L3. -Variable S12: backward_simulation L1 L2. -Variable S23: backward_simulation L2 L3. +Context index order match_states (S12: bsim_properties L1 L2 index order match_states). +Context index' order' match_states' (S23: bsim_properties L2 L3 index' order' match_states'). -Let bb_index : Type := (bsim_index S12 * bsim_index S23)%type. +Let bb_index : Type := (index * index')%type. -Let bb_order : bb_index -> bb_index -> Prop := - lex_ord (clos_trans _ (bsim_order S12)) (bsim_order S23). +Definition bb_order : bb_index -> bb_index -> Prop := lex_ord (clos_trans _ order) order'. Inductive bb_match_states: bb_index -> state L1 -> state L3 -> Prop := | bb_match_later: forall i1 i2 s1 s3 s2x s2y, - S12 i1 s1 s2x -> Star L2 s2x E0 s2y -> S23 i2 s2y s3 -> + match_states i1 s1 s2x -> Star L2 s2x E0 s2y -> match_states' i2 s2y s3 -> bb_match_states (i1, i2) s1 s3. Lemma bb_match_at: forall i1 i2 s1 s3 s2, - S12 i1 s1 s2 -> S23 i2 s2 s3 -> + match_states i1 s1 s2 -> match_states' i2 s2 s3 -> bb_match_states (i1, i2) s1 s3. Proof. intros. econstructor; eauto. apply star_refl. @@ -1120,7 +1121,7 @@ Qed. Lemma bb_simulation_base: forall s3 t s3', Step L3 s3 t s3' -> - forall i1 s1 i2 s2, S12 i1 s1 s2 -> S23 i2 s2 s3 -> safe L1 s1 -> + forall i1 s1 i2 s2, match_states i1 s1 s2 -> match_states' i2 s2 s3 -> safe L1 s1 -> exists i', exists s1', (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bb_order i' (i1, i2))) /\ bb_match_states i' s1' s3'. @@ -1128,29 +1129,29 @@ Proof. intros. exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto. intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]]. - (* 1 L2 makes one or several transitions *) +- (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). - exploit L3_single_events; eauto. - destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. + { 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. ++ (* 1.1 these are silent transitions *) + subst t. exploit (bsim_E0_plus S12); eauto. intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]]. - (* 1.1.1 L1 makes one or several transitions *) +* (* 1.1.1 L1 makes one or several transitions *) exists (i1', i2'); exists s1'; split. auto. eapply bb_match_at; eauto. - (* 1.1.2 L1 makes no transitions *) +* (* 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. - (* 1.2 non-silent transitions *) ++ (* 1.2 non-silent transitions *) 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_E0_star S12). eexact P. eauto. auto. intros [i1' [s1x [X Y]]]. + exploit (bsim_simulation' S12). 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 *) +- (* 2. L2 makes no transitions *) subst. exists (i1, i2'); exists s1; split. right; split. apply star_refl. right; auto. eapply bb_match_at; eauto. @@ -1165,12 +1166,12 @@ Lemma bb_simulation: Proof. intros. inv H0. exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS]. - (* 1. match at *) +- (* 1. match at *) subst. eapply bb_simulation_base; eauto. - (* 2. match later *) - exploit bsim_E0_plus; eauto. +- (* 2. match later *) + exploit (bsim_E0_plus S12); eauto. intros [[i1' [s1' [A B]]] | [i1' [A B]]]. - (* 2.1 one or several silent transitions *) ++ (* 2.1 one or several silent transitions *) exploit bb_simulation_base. eauto. auto. eexact B. eauto. eapply star_safe; eauto. eapply plus_star; eauto. intros [i'' [s1'' [C D]]]. @@ -1178,7 +1179,7 @@ Proof. left. eapply plus_star_trans; eauto. destruct C as [P | [P Q]]. apply plus_star; eauto. eauto. traceEq. - (* 2.2 no silent transition *) ++ (* 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. @@ -1186,48 +1187,53 @@ Proof. inv H6. left. eapply t_trans; eauto. left; auto. Qed. -Lemma compose_backward_simulation: backward_simulation L1 L3. -Proof. - apply Backward_simulation with (bsim_order := bb_order) (bsim_match_states := bb_match_states). -(* well founded *) - unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. apply bsim_order_wf. apply bsim_order_wf. -(* initial states exist *) - intros. exploit (bsim_initial_states_exist S12); eauto. intros [s2 A]. - eapply (bsim_initial_states_exist S23); eauto. -(* match initial states *) +End COMPOSE_BACKWARD_SIMULATIONS. + +Lemma compose_backward_simulation: + forall L1 L2 L3, + single_events L3 -> backward_simulation L1 L2 -> backward_simulation L2 L3 -> + backward_simulation L1 L3. +Proof. + intros L1 L2 L3 L3single S12 S23. + destruct S12 as [index order match_states props]. + destruct S23 as [index' order' match_states' props']. + apply Backward_simulation with (bb_order order order') (bb_match_states L1 L2 L3 match_states match_states'); + constructor. +- (* well founded *) + unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. eapply bsim_order_wf; eauto. eapply bsim_order_wf; eauto. +- (* initial states exist *) + intros. exploit (bsim_initial_states_exist props); eauto. intros [s2 A]. + eapply (bsim_initial_states_exist props'); eauto. +- (* match initial states *) intros s1 s3 INIT1 INIT3. - exploit (bsim_initial_states_exist S12); eauto. intros [s2 INIT2]. - exploit (bsim_match_initial_states S23); eauto. intros [i2 [s2' [INIT2' M2]]]. - exploit (bsim_match_initial_states S12); eauto. intros [i1 [s1' [INIT1' M1]]]. - exists (i1, i2); exists s1'; intuition. eapply bb_match_at; eauto. -(* match final states *) + exploit (bsim_initial_states_exist props); eauto. intros [s2 INIT2]. + exploit (bsim_match_initial_states props'); eauto. intros [i2 [s2' [INIT2' M2]]]. + exploit (bsim_match_initial_states props); eauto. intros [i1 [s1' [INIT1' M1]]]. + exists (i1, i2); exists s1'; intuition auto. 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. + exploit (bsim_match_final_states props'); 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. + exploit (bsim_E0_star props). 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. + exploit (bsim_match_final_states props); eauto. eapply star_safe; eauto. intros [s1'' [P Q]]. exists s1''; split; auto. eapply star_trans; eauto. -(* progress *) +- (* progress *) intros i s1 s3 MS SAFE. inv MS. - eapply (bsim_progress S23). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. -(* simulation *) - exact bb_simulation. -(* symbols *) - intros. transitivity (Senv.public_symbol (symbolenv L2) id); apply bsim_public_preserved; auto. + eapply (bsim_progress props'). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto. +- (* simulation *) + apply bb_simulation; auto. +- (* symbols *) + intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply bsim_public_preserved; eauto. Qed. -End COMPOSE_BACKWARD_SIMULATIONS. - (** ** Converting a forward simulation to a backward simulation *) Section FORWARD_TO_BACKWARD. -Variable L1: semantics. -Variable L2: semantics. -Variable FS: forward_simulation L1 L2. +Context L1 L2 index order match_states (FS: fsim_properties L1 L2 index order match_states). Hypothesis L1_receptive: receptive L1. Hypothesis L2_determinate: determinate L2. @@ -1243,38 +1249,38 @@ 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' -> + match_states i' s1' s2 -> + match_states 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. + forall i s1 s2, match_states i s1 s2 -> safe L1 s1 -> f2b_transitions s1 s2. Proof. - intros i0; pattern i0. apply well_founded_ind with (R := fsim_order FS). - apply fsim_order_wf. + intros i0; pattern i0. apply well_founded_ind with (R := order). + eapply fsim_order_wf; eauto. intros i REC s1 s2 MATCH SAFE. destruct (SAFE s1) as [[r FINAL] | [t [s1' STEP1]]]. apply star_refl. - (* final state reached *) +- (* final state reached *) eapply f2b_trans_final; eauto. apply star_refl. eapply fsim_match_final_states; eauto. - (* L1 can make one step *) +- (* 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)). - intuition. - destruct (star_inv H0); intuition. + assert (B: Plus L2 s2 t s2' \/ (s2' = s2 /\ t = E0 /\ order i' i)). + intuition auto. + destruct (star_inv H0); intuition auto. clear A. destruct B as [PLUS2 | [EQ1 [EQ2 ORDER]]]. - eapply f2b_trans_step; eauto. apply star_refl. - subst. exploit REC; eauto. eapply star_safe; eauto. apply star_one; auto. ++ 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_step; eauto. eapply star_left; eauto. +* eapply f2b_trans_final; eauto. eapply star_left; eauto. +* eapply f2b_trans_step; eauto. eapply star_left; eauto. Qed. Lemma fsim_simulation_not_E0: forall s1 t s1', Step L1 s1 t s1' -> t <> E0 -> - forall i s2, FS i s1 s2 -> - exists i', exists s2', Plus L2 s2 t s2' /\ FS i' s1' s2'. + forall i s2, match_states i s1 s2 -> + exists i', exists s2', Plus L2 s2 t s2' /\ match_states i' s1' s2'. Proof. intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]]. exists i'; exists s2'; split; auto. @@ -1363,23 +1369,23 @@ Qed. Inductive f2b_match_states: f2b_index -> state L1 -> state L2 -> Prop := | f2b_match_at: forall i s1 s2, - FS i s1 s2 -> + match_states i s1 s2 -> f2b_match_states (F2BI_after O) s1 s2 | f2b_match_before: forall s1 t s1' s2b s2 n s2a i, Step L1 s1 t s1' -> t <> E0 -> Star L2 s2b E0 s2 -> starN (step L2) (globalenv L2) n s2 t s2a -> - FS i s1 s2b -> + match_states i s1 s2b -> f2b_match_states (F2BI_before n) s1 s2 | f2b_match_after: forall n s2 s2a s1 i, starN (step L2) (globalenv L2) (S n) s2 E0 s2a -> - FS i s1 s2a -> + match_states i s1 s2a -> f2b_match_states (F2BI_after (S n)) s1 s2. Remark f2b_match_after': forall n s2 s2a s1 i, starN (step L2) (globalenv L2) n s2 E0 s2a -> - FS i s1 s2a -> + match_states i s1 s2a -> f2b_match_states (F2BI_after n) s1 s2. Proof. intros. inv H. @@ -1398,15 +1404,15 @@ Lemma f2b_simulation_step: Proof. intros s2 t s2' STEP2 i s1 MATCH SAFE. inv MATCH. -(* 1. At matching states *) +- (* 1. At matching states *) exploit f2b_progress; eauto. intros TRANS; inv TRANS. - (* 1.1 L1 can reach final state and L2 is at final state: impossible! *) ++ (* 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. *) ++ (* 1.2 L1 can make 0 or several steps; L2 can make 1 or several matching steps. *) 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 *) +* (* 1.2.1 L2 makes a silent transition *) destruct (silent_or_not_silent t2). (* 1.2.1.1 L1 makes a silent transition too: perform transition now and go to "after" state *) subst. simpl in *. destruct (star_starN H6) as [n STEPS2]. @@ -1418,7 +1424,7 @@ Proof. exists (F2BI_before n); exists s1'; split. right; split. auto. constructor. econstructor. eauto. auto. apply star_one; eauto. eauto. eauto. - (* 1.2.2 L2 makes a non-silent transition, and so does L1 *) +* (* 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. @@ -1437,15 +1443,15 @@ Proof. left. eapply plus_right; eauto. eapply f2b_match_after'; eauto. -(* 2. Before *) +- (* 2. Before *) inv H2. congruence. exploit f2b_determinacy_inv. eexact H4. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. - (* 2.1 L2 makes a silent transition: remain in "before" state *) ++ (* 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. - (* 2.2 L2 make a non-silent transition *) ++ (* 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 *. @@ -1466,7 +1472,7 @@ Proof. left. apply plus_one; auto. eapply f2b_match_after'; eauto. -(* 3. After *) +- (* 3. After *) 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]]]. @@ -1476,20 +1482,28 @@ Proof. congruence. Qed. +End FORWARD_TO_BACKWARD. + (** The backward simulation *) -Lemma forward_to_backward_simulation: backward_simulation L1 L2. +Lemma forward_to_backward_simulation: + forall L1 L2, + forward_simulation L1 L2 -> receptive L1 -> determinate L2 -> + backward_simulation L1 L2. Proof. - apply Backward_simulation with (bsim_order := f2b_order) (bsim_match_states := f2b_match_states). + intros L1 L2 FS L1_receptive L2_determinate. + destruct FS as [index order match_states FS]. + apply Backward_simulation with f2b_order (f2b_match_states L1 L2 match_states); constructor. +- (* well founded *) apply wf_f2b_order. -(* initial states exist *) +- (* initial states exist *) intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]]. exists s2; auto. -(* initial states *) +- (* initial states *) intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]]. assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'. exists (F2BI_after O); exists s1; split; auto. econstructor; eauto. -(* final states *) +- (* final states *) intros. inv H. exploit f2b_progress; eauto. intros TRANS; inv TRANS. assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0. @@ -1497,21 +1511,19 @@ Proof. inv H4. exploit (sd_final_nostep L2_determinate); eauto. contradiction. inv H5. congruence. exploit (sd_final_nostep L2_determinate); eauto. contradiction. inv H2. exploit (sd_final_nostep L2_determinate); eauto. contradiction. -(* progress *) +- (* progress *) 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. -(* simulation *) - exact f2b_simulation_step. -(* symbols preserved *) +- (* simulation *) + eapply f2b_simulation_step; eauto. +- (* symbols preserved *) exact (fsim_public_preserved FS). Qed. -End FORWARD_TO_BACKWARD. - (** * Transforming a semantics into a single-event, equivalent semantics *) Definition well_behaved_traces (L: semantics) : Prop := @@ -1554,15 +1566,15 @@ Section FACTOR_FORWARD_SIMULATION. Variable L1: semantics. Variable L2: semantics. -Variable sim: forward_simulation L1 L2. +Context index order match_states (sim: fsim_properties L1 L2 index order match_states). Hypothesis L2single: single_events L2. -Inductive ffs_match: fsim_index sim -> (trace * state L1) -> state L2 -> Prop := +Inductive ffs_match: index -> (trace * state L1) -> state L2 -> Prop := | ffs_match_at: forall i s1 s2, - sim i s1 s2 -> + match_states i s1 s2 -> ffs_match i (E0, s1) s2 | ffs_match_buffer: forall i ev t s1 s2 s2', - Star L2 s2 (ev :: t) s2' -> sim i s1 s2' -> + Star L2 s2 (ev :: t) s2' -> match_states i s1 s2' -> ffs_match i (ev :: t, s1) s2. Lemma star_non_E0_split': @@ -1585,27 +1597,27 @@ Lemma ffs_simulation: forall s1 t s1', Step (atomic L1) s1 t s1' -> forall i s2, ffs_match i s1 s2 -> exists i', exists s2', - (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ fsim_order sim i' i) + (Plus L2 s2 t s2' \/ (Star L2 s2 t s2') /\ order i' i) /\ ffs_match i' s1' s2'. Proof. induction 1; intros. -(* silent step *) +- (* silent step *) inv H0. exploit (fsim_simulation sim); eauto. intros [i' [s2' [A B]]]. exists i'; exists s2'; split. auto. constructor; auto. -(* start step *) +- (* start step *) inv H0. exploit (fsim_simulation sim); eauto. intros [i' [s2' [A B]]]. destruct t as [ | ev' t]. - (* single event *) ++ (* single event *) exists i'; exists s2'; split. auto. constructor; auto. - (* multiple events *) ++ (* 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]]. exists i'; exists s2x; split. auto. econstructor; eauto. -(* continue step *) +- (* continue step *) inv H0. exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]]. destruct t. @@ -1613,27 +1625,31 @@ Proof. exists i; exists s2x; split. auto. econstructor; eauto. Qed. +End FACTOR_FORWARD_SIMULATION. + Theorem factor_forward_simulation: + forall L1 L2, + forward_simulation L1 L2 -> single_events L2 -> forward_simulation (atomic L1) L2. Proof. - apply Forward_simulation with (fsim_match_states := ffs_match) (fsim_order := fsim_order sim). -(* wf *) - apply fsim_order_wf. -(* initial states *) + intros L1 L2 FS L2single. + destruct FS as [index order match_states sim]. + apply Forward_simulation with order (ffs_match L1 L2 match_states); constructor. +- (* wf *) + eapply fsim_order_wf; eauto. +- (* 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]]]. exists i; exists s2; split; auto. constructor; auto. -(* final states *) +- (* final states *) 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. -(* symbols preserved *) +- (* simulation *) + eapply ffs_simulation; eauto. +- (* symbols preserved *) simpl. exact (fsim_public_preserved sim). Qed. -End FACTOR_FORWARD_SIMULATION. - (** Likewise, a backward simulation from a single-event semantics [L1] to a semantics [L2] can be "factored" as a backward simulation from [L1] to [atomic L2]. *) @@ -1641,13 +1657,13 @@ Section FACTOR_BACKWARD_SIMULATION. Variable L1: semantics. Variable L2: semantics. -Variable sim: backward_simulation L1 L2. +Context index order match_states (sim: bsim_properties L1 L2 index order match_states). Hypothesis L1single: single_events L1. Hypothesis L2wb: well_behaved_traces L2. -Inductive fbs_match: bsim_index sim -> state L1 -> (trace * state L2) -> Prop := +Inductive fbs_match: index -> state L1 -> (trace * state L2) -> Prop := | fbs_match_intro: forall i s1 t s2 s1', - Star L1 s1 t s1' -> sim i s1' s2 -> + Star L1 s1 t s1' -> match_states i s1' s2 -> t = E0 \/ output_trace t -> fbs_match i s1 (t, s2). @@ -1655,18 +1671,18 @@ Lemma fbs_simulation: forall s2 t s2', Step (atomic L2) s2 t s2' -> forall i s1, fbs_match i s1 s2 -> safe L1 s1 -> exists i', exists s1', - (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ bsim_order sim i' i)) + (Plus L1 s1 t s1' \/ (Star L1 s1 t s1' /\ order i' i)) /\ fbs_match i' s1' s2'. Proof. induction 1; intros. -(* silent step *) +- (* silent step *) inv H0. 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. econstructor. apply star_refl. auto. auto. -(* start step *) +- (* start step *) inv H0. exploit (bsim_simulation sim); eauto. eapply star_safe; eauto. intros [i' [s1'' [A B]]]. @@ -1677,7 +1693,7 @@ Proof. left; auto. econstructor; eauto. exploit L2wb; eauto. -(* continue step *) +- (* 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. @@ -1690,47 +1706,51 @@ Lemma fbs_progress: (exists t, exists s2', Step (atomic L2) s2 t s2'). Proof. intros. inv H. destruct t. -(* 1. no buffered events *) +- (* 1. no buffered events *) exploit (bsim_progress sim); eauto. eapply star_safe; eauto. intros [[r A] | [t [s2' A]]]. -(* final state *) ++ (* final state *) left; exists r; simpl; auto. -(* L2 can step *) ++ (* 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 *) +- (* 2. some buffered events *) unfold E0 in H3; destruct H3. congruence. right; exists (e :: nil); exists (t, s3). constructor. auto. Qed. +End FACTOR_BACKWARD_SIMULATION. + Theorem factor_backward_simulation: + forall L1 L2, + backward_simulation L1 L2 -> single_events L1 -> well_behaved_traces L2 -> backward_simulation L1 (atomic L2). Proof. - apply Backward_simulation with (bsim_match_states := fbs_match) (bsim_order := bsim_order sim). -(* wf *) - apply bsim_order_wf. -(* initial states exist *) + intros L1 L2 BS L1single L2wb. + destruct BS as [index order match_states sim]. + apply Backward_simulation with order (fbs_match L1 L2 match_states); constructor. +- (* wf *) + eapply bsim_order_wf; eauto. +- (* initial states exist *) intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A]. exists (E0, s2). simpl; auto. -(* initial states match *) +- (* 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]]]. exists i; exists s1'; split. auto. econstructor. apply star_refl. auto. auto. -(* final states match *) +- (* 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. intros [s1'' [A B]]. exists s1''; split; auto. eapply star_trans; eauto. -(* progress *) - exact fbs_progress. -(* simulation *) - exact fbs_simulation. -(* symbols *) +- (* progress *) + eapply fbs_progress; eauto. +- (* simulation *) + eapply fbs_simulation; eauto. +- (* symbols *) simpl. exact (bsim_public_preserved sim). Qed. -End FACTOR_BACKWARD_SIMULATION. - (** Receptiveness of [atomic L]. *) Record strongly_receptive (L: semantics) : Prop := |