Library compcert.common.Smallstep
Tools for small-step operational semantics
This module defines generic operations and theorems over
the one-step transition relations that are used to specify
operational semantics in small-step style.
Require Import Relations.
Require Import Wellfounded.
Require Import Coqlib.
Require Import Events.
Require Import Globalenvs.
Require Import Integers.
Set Implicit Arguments.
A one-step transition relation has the following signature.
It is parameterized by a global environment, which does not
change during the transition. It relates the initial state
of the transition with its final state. The trace parameter
captures the observable events possibly generated during the
transition.
No transitions: stuck state
Zero, one or several transitions. Also known as Kleene closure,
or reflexive transitive closure.
Inductive star (ge: genv): state → trace → state → Prop :=
| star_refl: ∀ s,
star ge s E0 s
| star_step: ∀ s1 t1 s2 t2 s3 t,
step ge s1 t1 s2 → star ge s2 t2 s3 → t = t1 ** t2 →
star ge s1 t s3.
Lemma star_one:
∀ ge s1 t s2, step ge s1 t s2 → star ge s1 t s2.
Proof.
intros. eapply star_step; eauto. apply star_refl. traceEq.
Qed.
Lemma star_two:
∀ ge s1 t1 s2 t2 s3 t,
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.
Qed.
Lemma star_three:
∀ ge s1 t1 s2 t2 s3 t3 s4 t,
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.
Qed.
Lemma star_four:
∀ ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
step ge s1 t1 s2 → step ge s2 t2 s3 →
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.
Qed.
Lemma star_trans:
∀ ge s1 t1 s2, star ge s1 t1 s2 →
∀ t2 s3 t, star ge s2 t2 s3 → t = t1 ** t2 → star ge s1 t s3.
Proof.
induction 1; intros.
rewrite H0. simpl. auto.
eapply star_step; eauto. traceEq.
Qed.
Lemma star_left:
∀ ge s1 t1 s2 t2 s3 t,
step ge s1 t1 s2 → star ge s2 t2 s3 → t = t1 ** t2 →
star ge s1 t s3.
Proof star_step.
Lemma star_right:
∀ ge s1 t1 s2 t2 s3 t,
star ge s1 t1 s2 → step ge s2 t2 s3 → t = t1 ** t2 →
star ge s1 t s3.
Proof.
intros. eapply star_trans. eauto. apply star_one. eauto. auto.
Qed.
Lemma star_E0_ind:
∀ ge (P: state → state → Prop),
(∀ s, P s s) →
(∀ s1 s2 s3, step ge s1 E0 s2 → P s2 s3 → P s1 s3) →
∀ s1 s2, star ge s1 E0 s2 → P s1 s2.
Proof.
intros ge P BASE REC.
assert (∀ 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.
One or several transitions. Also known as the transitive closure.
Inductive plus (ge: genv): state → trace → state → Prop :=
| plus_left: ∀ s1 t1 s2 t2 s3 t,
step ge s1 t1 s2 → star ge s2 t2 s3 → t = t1 ** t2 →
plus ge s1 t s3.
Lemma plus_one:
∀ ge s1 t s2,
step ge s1 t s2 → plus ge s1 t s2.
Proof.
intros. econstructor; eauto. apply star_refl. traceEq.
Qed.
Lemma plus_two:
∀ ge s1 t1 s2 t2 s3 t,
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.
Qed.
Lemma plus_three:
∀ ge s1 t1 s2 t2 s3 t3 s4 t,
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.
Qed.
Lemma plus_four:
∀ ge s1 t1 s2 t2 s3 t3 s4 t4 s5 t,
step ge s1 t1 s2 → step ge s2 t2 s3 →
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.
Qed.
Lemma plus_star:
∀ ge s1 t s2, plus ge s1 t s2 → star ge s1 t s2.
Proof.
intros. inversion H; subst.
eapply star_step; eauto.
Qed.
Lemma plus_right:
∀ ge s1 t1 s2 t2 s3 t,
star ge s1 t1 s2 → step ge s2 t2 s3 → t = t1 ** t2 →
plus ge s1 t s3.
Proof.
intros. inversion H; subst. simpl. apply plus_one. auto.
rewrite Eapp_assoc. eapply plus_left; eauto.
eapply star_right; eauto.
Qed.
Lemma plus_left':
∀ ge s1 t1 s2 t2 s3 t,
step ge s1 t1 s2 → plus ge s2 t2 s3 → t = t1 ** t2 →
plus ge s1 t s3.
Proof.
intros. eapply plus_left; eauto. apply plus_star; auto.
Qed.
Lemma plus_right':
∀ ge s1 t1 s2 t2 s3 t,
plus ge s1 t1 s2 → step ge s2 t2 s3 → t = t1 ** t2 →
plus ge s1 t s3.
Proof.
intros. eapply plus_right; eauto. apply plus_star; auto.
Qed.
Lemma plus_star_trans:
∀ 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.
econstructor; eauto. eapply star_trans; eauto.
traceEq.
Qed.
Lemma star_plus_trans:
∀ ge s1 t1 s2 t2 s3 t,
star ge s1 t1 s2 → plus ge s2 t2 s3 → t = t1 ** t2 → plus ge s1 t s3.
Proof.
intros. inversion H; subst.
simpl; auto.
rewrite Eapp_assoc.
econstructor. eauto. eapply star_trans. eauto.
apply plus_star. eauto. eauto. auto.
Qed.
Lemma plus_trans:
∀ ge s1 t1 s2 t2 s3 t,
plus ge s1 t1 s2 → plus ge s2 t2 s3 → t = t1 ** t2 → plus ge s1 t s3.
Proof.
intros. eapply plus_star_trans. eauto. apply plus_star. eauto. auto.
Qed.
Lemma plus_inv:
∀ ge s1 t s2,
plus ge s1 t s2 →
step ge s1 t s2 ∨ ∃ s', ∃ t1, ∃ t2, step ge s1 t1 s' ∧ plus ge s' t2 s2 ∧ t = t1 ** t2.
Proof.
intros. inversion H; subst. inversion H1; subst.
left. rewrite E0_right. auto.
right. ∃ s3; ∃ t1; ∃ (t0 ** t3); split. auto.
split. econstructor; eauto. auto.
Qed.
Lemma star_inv:
∀ ge s1 t s2,
star ge s1 t s2 →
(s2 = s1 ∧ t = E0) ∨ plus ge s1 t s2.
Proof.
intros. inv H. left; auto. right; econstructor; eauto.
Qed.
Lemma plus_ind2:
∀ ge (P: state → trace → state → Prop),
(∀ s1 t s2, step ge s1 t s2 → P s1 t s2) →
(∀ 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) →
∀ s1 t s2, plus ge s1 t s2 → P s1 t s2.
Proof.
intros ge P BASE IND.
assert (∀ s1 t s2, star ge s1 t s2 →
∀ s0 t0, step ge s0 t0 s1 →
P s0 (t0 ** t) s2).
induction 1; intros.
rewrite E0_right. apply BASE; auto.
eapply IND. eauto. econstructor; eauto. subst t. eapply IHstar; eauto. auto.
intros. inv H0. eauto.
Qed.
Lemma plus_E0_ind:
∀ ge (P: state → state → Prop),
(∀ s1 s2 s3, step ge s1 E0 s2 → star ge s2 E0 s3 → P s1 s3) →
∀ s1 s2, plus ge s1 E0 s2 → P s1 s2.
Proof.
intros. inv H0. exploit Eapp_E0_inv; eauto. intros [A B]; subst. eauto.
Qed.
Counted sequences of transitions
Inductive starN (ge: genv): nat → state → trace → state → Prop :=
| starN_refl: ∀ s,
starN ge O s E0 s
| starN_step: ∀ n s t t1 s' t2 s'',
step ge s t1 s' → starN ge n s' t2 s'' → t = t1 ** t2 →
starN ge (S n) s t s''.
Remark starN_star:
∀ ge n s t s', starN ge n s t s' → star ge s t s'.
Proof.
induction 1; econstructor; eauto.
Qed.
Remark star_starN:
∀ ge s t s', star ge s t s' → ∃ n, starN ge n s t s'.
Proof.
induction 1.
∃ O; constructor.
destruct IHstar as [n P]. ∃ (S n); econstructor; eauto.
Qed.
Infinitely many transitions
CoInductive forever (ge: genv): state → traceinf → Prop :=
| forever_intro: ∀ s1 t s2 T,
step ge s1 t s2 → forever ge s2 T →
forever ge s1 (t *** T).
Lemma star_forever:
∀ ge s1 t s2, star ge s1 t s2 →
∀ T, forever ge s2 T →
forever ge s1 (t *** T).
Proof.
induction 1; intros. simpl. auto.
subst t. rewrite Eappinf_assoc.
econstructor; eauto.
Qed.
An alternate, equivalent definition of forever that is useful
for coinductive reasoning.
Variable A: Type.
Variable order: A → A → Prop.
CoInductive forever_N (ge: genv) : A → state → traceinf → Prop :=
| forever_N_star: ∀ s1 t s2 a1 a2 T1 T2,
star ge s1 t s2 →
order a2 a1 →
forever_N ge a2 s2 T2 →
T1 = t *** T2 →
forever_N ge a1 s1 T1
| forever_N_plus: ∀ s1 t s2 a1 a2 T1 T2,
plus ge s1 t s2 →
forever_N ge a2 s2 T2 →
T1 = t *** T2 →
forever_N ge a1 s1 T1.
Hypothesis order_wf: well_founded order.
Lemma forever_N_inv:
∀ ge a s T,
forever_N ge a s T →
∃ t, ∃ s', ∃ a', ∃ T',
step ge s t s' ∧ forever_N ge a' s' T' ∧ T = t *** T'.
Proof.
intros ge a0. pattern a0. apply (well_founded_ind order_wf).
intros. inv H0.
inv H1.
change (E0 *** T2) with T2. apply H with a2. auto. auto.
∃ t1; ∃ s0; ∃ x; ∃ (t2 *** T2).
split. auto. split. eapply forever_N_star; eauto.
apply Eappinf_assoc.
inv H1.
∃ t1; ∃ s0; ∃ a2; ∃ (t2 *** T2).
split. auto.
split. inv H3. auto.
eapply forever_N_plus. econstructor; eauto. eauto. auto.
apply Eappinf_assoc.
Qed.
Lemma forever_N_forever:
∀ ge a s T, forever_N ge a s T → forever ge s T.
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.
apply COINDHYP with a'; auto.
Qed.
Yet another alternative definition of forever.
CoInductive forever_plus (ge: genv) : state → traceinf → Prop :=
| forever_plus_intro: ∀ s1 t s2 T1 T2,
plus ge s1 t s2 →
forever_plus ge s2 T2 →
T1 = t *** T2 →
forever_plus ge s1 T1.
Lemma forever_plus_inv:
∀ ge s T,
forever_plus ge s T →
∃ s', ∃ t, ∃ T',
step ge s t s' ∧ forever_plus ge s' T' ∧ T = t *** T'.
Proof.
intros. inv H. inv H0. ∃ s0; ∃ t1; ∃ (t2 *** T2).
split. auto.
split. exploit star_inv; eauto. intros [[P Q] | R].
subst. simpl. auto. econstructor; eauto.
traceEq.
Qed.
Lemma forever_plus_forever:
∀ ge s T, forever_plus ge s T → forever ge s T.
Proof.
cofix COINDHYP; intros.
destruct (forever_plus_inv H) as [s' [t [T' [P [Q R]]]]].
subst. econstructor; eauto.
Qed.
Infinitely many silent transitions
CoInductive forever_silent (ge: genv): state → Prop :=
| forever_silent_intro: ∀ s1 s2,
step ge s1 E0 s2 → forever_silent ge s2 →
forever_silent ge s1.
An alternate definition.
CoInductive forever_silent_N (ge: genv) : A → state → Prop :=
| forever_silent_N_star: ∀ s1 s2 a1 a2,
star ge s1 E0 s2 →
order a2 a1 →
forever_silent_N ge a2 s2 →
forever_silent_N ge a1 s1
| forever_silent_N_plus: ∀ s1 s2 a1 a2,
plus ge s1 E0 s2 →
forever_silent_N ge a2 s2 →
forever_silent_N ge a1 s1.
Lemma forever_silent_N_inv:
∀ ge a s,
forever_silent_N ge a s →
∃ s', ∃ a',
step ge s E0 s' ∧ forever_silent_N ge a' s'.
Proof.
intros ge a0. pattern a0. apply (well_founded_ind order_wf).
intros. inv H0.
inv H1.
apply H with a2. auto. auto.
exploit Eapp_E0_inv; eauto. intros [P Q]. subst.
∃ s0; ∃ x.
split. auto. eapply forever_silent_N_star; eauto.
inv H1. exploit Eapp_E0_inv; eauto. intros [P Q]. subst.
∃ s0; ∃ a2.
split. auto. inv H3. auto.
eapply forever_silent_N_plus. econstructor; eauto. eauto.
Qed.
Lemma forever_silent_N_forever:
∀ ge a s, forever_silent_N ge a s → forever_silent ge s.
Proof.
cofix COINDHYP; intros.
destruct (forever_silent_N_inv H) as [s' [a' [P Q]]].
apply forever_silent_intro with s'. auto.
apply COINDHYP with a'; auto.
Qed.
Infinitely many non-silent transitions
CoInductive forever_reactive (ge: genv): state → traceinf → Prop :=
| forever_reactive_intro: ∀ s1 s2 t T,
star ge s1 t s2 → t ≠ E0 → forever_reactive ge s2 T →
forever_reactive ge s1 (t *** T).
Lemma star_forever_reactive:
∀ ge s1 t s2 T,
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.
red; intro. exploit Eapp_E0_inv; eauto. intros [P Q]. contradiction.
auto.
Qed.
End CLOSURES.
Transition semantics
Record semantics (RETVAL: Type) : Type := Semantics_gen {
state: Type;
genvtype: Type;
step : genvtype → state → trace → state → Prop;
initial_state: state → Prop;
final_state: state → RETVAL → Prop;
globalenv: genvtype;
symbolenv: Senv.t
}.
The form used in earlier CompCert versions, for backward compatibility.
Definition Semantics {state funtype vartype: Type}
{RETVAL: Type}
(step: Genv.t funtype vartype → state → trace → state → Prop)
(initial_state: state → Prop)
(final_state: state → RETVAL → Prop)
(globalenv: Genv.t funtype vartype) :=
{| state := state;
genvtype := Genv.t funtype vartype;
step := step;
initial_state := initial_state;
final_state := final_state;
globalenv := globalenv;
symbolenv := Genv.to_senv globalenv |}.
Handy notations.
Notation " 'Step' L " := (step L (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Star' L " := (star (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Plus' L " := (plus (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Forever_silent' L " := (forever_silent (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Forever_reactive' L " := (forever_reactive (step L) (globalenv L)) (at level 1) : smallstep_scope.
Notation " 'Nostep' L " := (nostep (step L) (globalenv L)) (at level 1) : smallstep_scope.
Open Scope smallstep_scope.
Record fsim_properties {RETVAL: Type} (L1 L2: semantics RETVAL) (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:
∀ s1, initial_state L1 s1 →
∃ i, ∃ s2, initial_state L2 s2 ∧ match_states i s1 s2;
fsim_match_final_states:
∀ i s1 s2 r,
match_states i s1 s2 → final_state L1 s1 r → final_state L2 s2 r;
fsim_simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ i s2, match_states i s1 s2 →
∃ i', ∃ s2',
(Plus L2 s2 t s2' ∨ (Star L2 s2 t s2' ∧ order i' i))
∧ match_states i' s1' s2';
fsim_public_preserved:
∀ id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
}.
Arguments fsim_properties {_} _ _ _ _ _.
Inductive forward_simulation {RETVAL: Type} (L1 L2: semantics RETVAL) : 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 {RETVAL L1 L2 index} order match_states props.
An alternate form of the simulation diagram
Lemma fsim_simulation':
∀ RETVAL: Type,
∀ L1 L2: _ RETVAL,
∀ index order match_states, fsim_properties L1 L2 index order match_states →
∀ i s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states i s1 s2 →
(∃ i', ∃ s2', Plus L2 s2 t s2' ∧ match_states i' s1' s2')
∨ (∃ i', order i' i ∧ t = E0 ∧ match_states i' s1' s2).
Proof.
intros. exploit @fsim_simulation; eauto.
intros [i' [s2' [A B]]]. intuition.
left; ∃ i'; ∃ s2'; auto.
inv H3.
right; ∃ i'; auto.
left; ∃ i'; ∃ s2'; split; auto. econstructor; eauto.
Qed.
Section FORWARD_SIMU_DIAGRAMS.
Context {RETVAL: Type}.
Variable L1: semantics RETVAL.
Variable L2: semantics RETVAL.
Hypothesis public_preserved:
∀ id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
Variable match_states: state L1 → state L2 → Prop.
Hypothesis match_initial_states:
∀ s1, initial_state L1 s1 →
∃ s2, initial_state L2 s2 ∧ match_states s1 s2.
Hypothesis match_final_states:
∀ s1 s2 r,
match_states s1 s2 →
final_state L1 s1 r →
final_state L2 s2 r.
Simulation when one transition in the first program
corresponds to zero, one or several transitions in the second program.
However, there is no stuttering: infinitely many transitions
in the source program must correspond to infinitely many
transitions in the second program.
order is a well-founded ordering associated with states
of the first semantics. Stuttering steps must correspond
to states that decrease w.r.t. order.
Variable order: state L1 → state L1 → Prop.
Hypothesis order_wf: well_founded order.
Hypothesis simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states s1 s2 →
∃ s2',
(Plus L2 s2 t s2' ∨ (Star L2 s2 t s2' ∧ order s1' s1))
∧ match_states s1' s2'.
Lemma forward_simulation_star_wf: forward_simulation L1 L2.
Proof.
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]].
∃ s1; ∃ s2; auto.
- intros. destruct H. eapply match_final_states; eauto.
- intros. destruct H0. subst i. exploit simulation; eauto. intros [s2' [A B]].
∃ s1'; ∃ s2'; intuition auto.
- auto.
Qed.
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
a stuttering step.
Variable measure: state L1 → nat.
Hypothesis simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states s1 s2 →
(∃ s2', Plus L2 s2 t s2' ∧ match_states s1' s2')
∨ (measure s1' < measure s1 ∧ t = E0 ∧ match_states s1' s2)%nat.
Lemma forward_simulation_star: forward_simulation L1 L2.
Proof.
apply forward_simulation_star_wf with (ltof _ measure).
apply well_founded_ltof.
intros. exploit simulation; eauto. intros [[s2' [A B]] | [A [B C]]].
∃ s2'; auto.
∃ s2; split. right; split. rewrite B. apply star_refl. auto. auto.
Qed.
End SIMULATION_STAR.
Simulation when one transition in the first program corresponds
to one or several transitions in the second program.
Section SIMULATION_PLUS.
Hypothesis simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states s1 s2 →
∃ s2', Plus L2 s2 t s2' ∧ match_states s1' s2'.
Lemma forward_simulation_plus: forward_simulation L1 L2.
Proof.
apply forward_simulation_star with (measure := fun _ ⇒ O).
intros. exploit simulation; eauto.
Qed.
End SIMULATION_PLUS.
Lock-step simulation: each transition in the first semantics
corresponds to exactly one transition in the second semantics.
Section SIMULATION_STEP.
Hypothesis simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states s1 s2 →
∃ s2', Step L2 s2 t s2' ∧ match_states s1' s2'.
Lemma forward_simulation_step: forward_simulation L1 L2.
Proof.
apply forward_simulation_plus.
intros. exploit simulation; eauto. intros [s2' [A B]].
∃ s2'; split; auto. apply plus_one; auto.
Qed.
End SIMULATION_STEP.
Simulation when one transition in the first program
corresponds to zero or one transitions in the second program.
However, there is no stuttering: infinitely many transitions
in the source program must correspond to infinitely many
transitions in the second program.
Section SIMULATION_OPT.
Variable measure: state L1 → nat.
Hypothesis simulation:
∀ s1 t s1', Step L1 s1 t s1' →
∀ s2, match_states s1 s2 →
(∃ s2', Step L2 s2 t s2' ∧ match_states s1' s2')
∨ (measure s1' < measure s1 ∧ t = E0 ∧ match_states s1' s2)%nat.
Lemma forward_simulation_opt: forward_simulation L1 L2.
Proof.
apply forward_simulation_star with measure.
intros. exploit simulation; eauto. intros [[s2' [A B]] | [A [B C]]].
left; ∃ s2'; split; auto. apply plus_one; auto.
right; auto.
Qed.
End SIMULATION_OPT.
End FORWARD_SIMU_DIAGRAMS.
Section SIMULATION_SEQUENCES.
Context {RETVAL: Type}.
Context (L1 L2: semantics RETVAL).
Context index order match_states (S: fsim_properties L1 L2 index order match_states).
Lemma simulation_star:
∀ s1 t s1', Star L1 s1 t s1' →
∀ i s2, match_states i s1 s2 →
∃ i', ∃ s2', Star L2 s2 t s2' ∧ match_states i' s1' s2'.
Proof.
induction 1; intros.
∃ i; ∃ s2; split; auto. apply star_refl.
exploit @fsim_simulation; eauto. intros [i' [s2' [A B]]].
exploit IHstar; eauto. intros [i'' [s2'' [C D]]].
∃ i''; ∃ s2''; split; auto. eapply star_trans; eauto.
intuition auto. apply plus_star; auto.
Qed.
Lemma simulation_plus:
∀ s1 t s1', Plus L1 s1 t s1' →
∀ i s2, match_states i s1 s2 →
(∃ i', ∃ s2', Plus L2 s2 t s2' ∧ match_states i' s1' s2')
∨ (∃ i', clos_trans _ order i' i ∧ t = E0 ∧ match_states i' s1' s2).
Proof.
induction 1 using plus_ind2; intros.
exploit fsim_simulation'; eauto. intros [A | [i' A]].
left; auto.
right; ∃ i'; intuition.
exploit fsim_simulation'; eauto. intros [[i' [s2' [A B]]] | [i' [A [B C]]]].
exploit simulation_star. apply plus_star; eauto. eauto.
intros [i'' [s2'' [P Q]]].
left; ∃ i''; ∃ s2''; split; auto. eapply plus_star_trans; eauto.
exploit IHplus; eauto. intros [[i'' [s2'' [P Q]]] | [i'' [P [Q R]]]].
subst. simpl. left; ∃ i''; ∃ s2''; auto.
subst. simpl. right; ∃ i''; intuition auto.
eapply t_trans; eauto. eapply t_step; eauto.
Qed.
Lemma simulation_forever_silent:
∀ i s1 s2,
Forever_silent L1 s1 → match_states i s1 s2 →
Forever_silent L2 s2.
Proof.
assert (∀ i s1 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. eapply fsim_order_wf; eauto.
Qed.
Lemma simulation_forever_reactive:
∀ i s1 s2 T,
Forever_reactive L1 s1 T → match_states i s1 s2 →
Forever_reactive L2 s2 T.
Proof.
cofix COINDHYP; intros.
inv H.
edestruct simulation_star as [i' [st2' [A B]]]; eauto.
econstructor; eauto.
Qed.
End SIMULATION_SEQUENCES.
Lemma compose_forward_simulations:
∀ {RETVAL: Type},
∀ L1 L2 L3, forward_simulation (RETVAL := RETVAL) L1 L2 → forward_simulation L2 L3 → forward_simulation L1 L3.
Proof.
intro RETVAL.
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) ⇒
∃ s2, match_states (snd i) s1 s2 ∧ match_states' (fst i) s2 s3).
apply Forward_simulation with ff_order ff_match_states; constructor.
-
unfold ff_order. apply wf_lex_ord. apply wf_clos_trans.
eapply fsim_order_wf; eauto. eapply fsim_order_wf; eauto.
-
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]]].
∃ (i', i); ∃ s3; split; auto. ∃ s2; auto.
-
intros. destruct H as [s3 [A B]].
eapply (fsim_match_final_states props'); eauto.
eapply (fsim_match_final_states props); eauto.
-
intros. destruct H0 as [s3 [A B]]. destruct i as [i2 i1]; simpl in ×.
exploit (fsim_simulation' props); eauto. intros [[i1' [s3' [C D]]] | [i1' [C [D E]]]].
+
exploit @simulation_plus; eauto. intros [[i2' [s2' [P Q]]] | [i2' [P [Q R]]]].
×
∃ (i2', i1'); ∃ s2'; split. auto. ∃ s3'; auto.
×
∃ (i2', i1'); ∃ s2; split.
right; split. subst t; apply star_refl. red. left. auto.
∃ s3'; auto.
+
∃ (i2, i1'); ∃ s2; split.
right; split. subst t; apply star_refl. red. right. auto.
∃ s3; auto.
-
intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply fsim_public_preserved; eauto.
Qed.
Definition single_events {RETVAL: Type} (L: semantics RETVAL) : Prop :=
∀ s t s', Step L s t s' → (length t ≤ 1)%nat.
Record receptive {RETVAL: Type} (L: semantics RETVAL) : Prop :=
Receptive {
sr_receptive: ∀ s t1 s1 t2,
Step L s t1 s1 → match_traces (symbolenv L) t1 t2 → ∃ s2, Step L s t2 s2;
sr_traces:
single_events L
}.
Record determinate {RETVAL: Type} (L: semantics RETVAL) : Prop :=
Determinate {
sd_determ: ∀ s t1 s1 t2 s2,
Step L s t1 s1 → Step L s t2 s2 →
match_traces (symbolenv L) t1 t2 ∧ (t1 = t2 → s1 = s2);
sd_traces:
single_events L;
sd_initial_determ: ∀ s1 s2,
initial_state L s1 → initial_state L s2 → s1 = s2;
sd_final_nostep: ∀ s r,
final_state L s r → Nostep L s;
sd_final_determ: ∀ s r1 r2,
final_state L s r1 → final_state L s r2 → r1 = r2
}.
Section DETERMINACY.
Context {RETVAL: Type}.
Variable L: semantics RETVAL.
Hypothesis DET: determinate L.
Lemma sd_determ_1:
∀ s t1 s1 t2 s2,
Step L s t1 s1 → Step L s t2 s2 → match_traces (symbolenv L) t1 t2.
Proof.
intros. eapply sd_determ; eauto.
Qed.
Lemma sd_determ_2:
∀ s t s1 s2,
Step L s t s1 → Step L s t s2 → s1 = s2.
Proof.
intros. eapply sd_determ; eauto.
Qed.
Lemma star_determinacy:
∀ s t s', Star L s t s' →
∀ s'', Star L s t s'' → Star L s' E0 s'' ∨ Star L s'' E0 s'.
Proof.
induction 1; intros.
auto.
inv H2.
right. eapply star_step; eauto.
exploit sd_determ_1. eexact H. eexact H3. intros MT.
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 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.
auto.
Qed.
End DETERMINACY.
Definition safe {RETVAL: Type} (L: semantics RETVAL) (s: state L) : Prop :=
∀ s',
Star L s E0 s' →
(∃ r, final_state L s' r)
∨ (∃ t, ∃ s'', Step L s' t s'').
Lemma star_safe:
∀ {RETVAL: Type},
∀ (L: semantics RETVAL) s s',
Star L s E0 s' → safe L s → safe L s'.
Proof.
intros; red; intros. apply H0. eapply star_trans; eauto.
Qed.
The general form of a backward simulation.
Record bsim_properties {RETVAL: Type}
(L1 L2: semantics RETVAL) (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:
∀ s1, initial_state L1 s1 → ∃ s2, initial_state L2 s2;
bsim_match_initial_states:
∀ s1 s2, initial_state L1 s1 → initial_state L2 s2 →
∃ i, ∃ s1', initial_state L1 s1' ∧ match_states i s1' s2;
bsim_match_final_states:
∀ i s1 s2 r,
match_states i s1 s2 → safe L1 s1 → final_state L2 s2 r →
∃ s1', Star L1 s1 E0 s1' ∧ final_state L1 s1' r;
bsim_progress:
∀ i s1 s2,
match_states i s1 s2 → safe L1 s1 →
(∃ r, final_state L2 s2 r) ∨
(∃ t, ∃ s2', Step L2 s2 t s2');
bsim_simulation:
∀ s2 t s2', Step L2 s2 t s2' →
∀ i s1, match_states i s1 s2 → safe L1 s1 →
∃ i', ∃ s1',
(Plus L1 s1 t s1' ∨ (Star L1 s1 t s1' ∧ order i' i))
∧ match_states i' s1' s2';
bsim_public_preserved:
∀ id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id
}.
Arguments bsim_properties {_} _ _ _ _ _.
Inductive backward_simulation {RETVAL: Type} (L1 L2: semantics RETVAL) : 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 {RETVAL L1 L2 index} order match_states props.
An alternate form of the simulation diagram
Lemma bsim_simulation':
∀ RETVAL: Type,
∀ (L1 L2: _ RETVAL) index order match_states, bsim_properties L1 L2 index order match_states →
∀ i s2 t s2', Step L2 s2 t s2' →
∀ s1, match_states i s1 s2 → safe L1 s1 →
(∃ i', ∃ s1', Plus L1 s1 t s1' ∧ match_states i' s1' s2')
∨ (∃ i', order i' i ∧ t = E0 ∧ match_states i' s1 s2').
Proof.
intros. exploit @bsim_simulation; eauto.
intros [i' [s1' [A B]]]. intuition.
left; ∃ i'; ∃ s1'; auto.
inv H4.
right; ∃ i'; auto.
left; ∃ i'; ∃ s1'; split; auto. econstructor; eauto.
Qed.
Section BACKWARD_SIMU_DIAGRAMS.
Context {RETVAL: Type}.
Variable L1: semantics RETVAL.
Variable L2: semantics RETVAL.
Hypothesis public_preserved:
∀ id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id.
Variable match_states: state L1 → state L2 → Prop.
Hypothesis initial_states_exist:
∀ s1, initial_state L1 s1 → ∃ s2, initial_state L2 s2.
Hypothesis match_initial_states:
∀ s1 s2, initial_state L1 s1 → initial_state L2 s2 →
∃ s1', initial_state L1 s1' ∧ match_states s1' s2.
Hypothesis match_final_states:
∀ s1 s2 r,
match_states s1 s2 → final_state L2 s2 r → final_state L1 s1 r.
Hypothesis progress:
∀ s1 s2,
match_states s1 s2 → safe L1 s1 →
(∃ r, final_state L2 s2 r) ∨
(∃ t, ∃ s2', Step L2 s2 t s2').
Section BACKWARD_SIMULATION_PLUS.
Hypothesis simulation:
∀ s2 t s2', Step L2 s2 t s2' →
∀ s1, match_states s1 s2 → safe L1 s1 →
∃ s1', Plus L1 s1 t s1' ∧ match_states s1' s2'.
Lemma backward_simulation_plus: backward_simulation L1 L2.
Proof.
apply Backward_simulation with
(fun (x y: unit) ⇒ False)
(fun (i: unit) s1 s2 ⇒ match_states s1 s2);
constructor; auto.
- red; intros; constructor; intros. contradiction.
- intros. ∃ tt; eauto.
- intros. ∃ s1; split. apply star_refl. eauto.
- intros. exploit simulation; eauto. intros [s1' [A B]].
∃ tt; ∃ s1'; auto.
Qed.
End BACKWARD_SIMULATION_PLUS.
End BACKWARD_SIMU_DIAGRAMS.
Section BACKWARD_SIMULATION_SEQUENCES.
Context {RETVAL: Type}.
Context (L1 L2: _ RETVAL) index order match_states (S: bsim_properties L1 L2 index order match_states).
Lemma bsim_E0_star:
∀ s2 s2', Star L2 s2 E0 s2' →
∀ i s1, match_states i s1 s2 → safe L1 s1 →
∃ i', ∃ s1', Star L1 s1 E0 s1' ∧ match_states i' s1' s2'.
Proof.
intros s20 s20' STAR0. pattern s20, s20'. eapply star_E0_ind; eauto.
-
intros. ∃ i; ∃ s1; split; auto. apply star_refl.
-
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]]].
∃ i''; ∃ s1''; split; auto. eapply star_trans; eauto.
Qed.
Lemma bsim_safe:
∀ i s1 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]]].
eapply bsim_progress; eauto. eapply star_safe; eauto.
Qed.
Lemma bsim_E0_plus:
∀ s2 t s2', Plus L2 s2 t s2' → t = E0 →
∀ i s1, match_states i s1 s2 → safe L1 s1 →
(∃ i', ∃ s1', Plus L1 s1 E0 s1' ∧ match_states i' s1' s2')
∨ (∃ i', clos_trans _ order i' i ∧ match_states i' s1 s2').
Proof.
induction 1 using plus_ind2; intros; subst t.
-
exploit bsim_simulation'; eauto. intros [[i' [s1' [A B]]] | [i' [A [B C]]]].
+ left; ∃ i'; ∃ s1'; auto.
+ right; ∃ i'; intuition.
-
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; ∃ i''; ∃ s1''; intuition. eapply plus_star_trans; eauto.
+ exploit IHplus; eauto. intros [P | [i'' [P Q]]].
left; auto.
right; ∃ i''; intuition. eapply t_trans; eauto. apply t_step; auto.
Qed.
Lemma star_non_E0_split:
∀ s2 t s2', Star L2 s2 t s2' → (length t = 1)%nat →
∃ s2x, ∃ s2y, Star L2 s2 E0 s2x ∧ Step L2 s2x t s2y ∧ Star L2 s2y E0 s2'.
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.
destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction.
destruct EITHER; subst.
exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]].
∃ s2x; ∃ s2y; intuition. eapply star_left; eauto.
rewrite E0_right. ∃ s1; ∃ s2; intuition. apply star_refl.
Qed.
End BACKWARD_SIMULATION_SEQUENCES.
Section COMPOSE_BACKWARD_SIMULATIONS.
Context {RETVAL: Type}.
Variable L1: semantics RETVAL.
Variable L2: semantics RETVAL.
Variable L3: semantics RETVAL.
Hypothesis L3_single_events: single_events 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 := (index × index')%type.
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: ∀ i1 i2 s1 s3 s2x s2y,
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: ∀ i1 i2 s1 s3 s2,
match_states i1 s1 s2 → match_states' i2 s2 s3 →
bb_match_states (i1, i2) s1 s3.
Proof.
intros. econstructor; eauto. apply star_refl.
Qed.
Lemma bb_simulation_base:
∀ s3 t s3', Step L3 s3 t s3' →
∀ i1 s1 i2 s2, match_states i1 s1 s2 → match_states' i2 s2 s3 → safe L1 s1 →
∃ i', ∃ s1',
(Plus L1 s1 t s1' ∨ (Star L1 s1 t s1' ∧ bb_order i' (i1, i2)))
∧ bb_match_states i' s1' s3'.
Proof.
intros.
exploit (bsim_simulation' S23); eauto. eapply bsim_safe; eauto.
intros [ [i2' [s2' [PLUS2 MATCH2]]] | [i2' [ORD2 [EQ MATCH2]]]].
-
assert (EITHER: t = E0 ∨ (length t = 1)%nat).
{ exploit L3_single_events; eauto.
destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. }
destruct EITHER.
+
subst t. exploit (bsim_E0_plus S12); eauto.
intros [ [i1' [s1' [PLUS1 MATCH1]]] | [i1' [ORD1 MATCH1]]].
×
∃ (i1', i2'); ∃ s1'; split. auto. eapply bb_match_at; eauto.
×
∃ (i1', i2'); ∃ s1; split.
right; split. apply star_refl. left; auto.
eapply bb_match_at; eauto.
+
exploit @star_non_E0_split. apply plus_star; eauto. auto.
intros [s2x [s2y [P [Q R]]]].
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).
∃ (i1'', i2'); ∃ s1y; split.
left. eapply star_plus_trans; eauto. eapply bb_match_later; eauto.
-
subst. ∃ (i1, i2'); ∃ s1; split.
right; split. apply star_refl. right; auto.
eapply bb_match_at; eauto.
Qed.
Lemma bb_simulation:
∀ s3 t s3', Step L3 s3 t s3' →
∀ i s1, bb_match_states i s1 s3 → safe L1 s1 →
∃ i', ∃ s1',
(Plus L1 s1 t s1' ∨ (Star L1 s1 t s1' ∧ bb_order i' i))
∧ bb_match_states i' s1' s3'.
Proof.
intros. inv H0.
exploit star_inv; eauto. intros [[EQ1 EQ2] | PLUS].
-
subst. eapply bb_simulation_base; eauto.
-
exploit (bsim_E0_plus S12); eauto.
intros [[i1' [s1' [A B]]] | [i1' [A B]]].
+
exploit bb_simulation_base. eauto. auto. eexact B. eauto.
eapply star_safe; eauto. eapply plus_star; eauto.
intros [i'' [s1'' [C D]]].
∃ i''; ∃ s1''; split; auto.
left. eapply plus_star_trans; eauto.
destruct C as [P | [P Q]]. apply plus_star; eauto. eauto.
traceEq.
+
exploit bb_simulation_base. eauto. auto. eexact B. eauto. auto.
intros [i'' [s1'' [C D]]].
∃ i''; ∃ s1''; split; auto.
intuition. right; intuition.
inv H6. left. eapply t_trans; eauto. left; auto.
Qed.
End COMPOSE_BACKWARD_SIMULATIONS.
Lemma compose_backward_simulation:
∀ RETVAL: Type,
∀ L1 L2 L3: _ RETVAL,
single_events L3 → backward_simulation L1 L2 → backward_simulation L2 L3 →
backward_simulation L1 L3.
Proof.
intro RETVAL.
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.
-
unfold bb_order. apply wf_lex_ord. apply wf_clos_trans. eapply bsim_order_wf; eauto. eapply bsim_order_wf; eauto.
-
intros. exploit (bsim_initial_states_exist props); eauto. intros [s2 A].
eapply (bsim_initial_states_exist props'); eauto.
-
intros s1 s3 INIT1 INIT3.
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]]].
∃ (i1, i2); ∃ s1'; intuition auto. eapply bb_match_at; eauto.
-
intros i s1 s3 r MS SAFE FIN. inv MS.
exploit (bsim_match_final_states props'); eauto.
eapply star_safe; eauto. eapply bsim_safe; eauto.
intros [s2' [A B]].
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 props); eauto. eapply star_safe; eauto.
intros [s1'' [P Q]].
∃ s1''; split; auto. eapply star_trans; eauto.
-
intros i s1 s3 MS SAFE. inv MS.
eapply (bsim_progress props'). eauto. eapply star_safe; eauto. eapply bsim_safe; eauto.
-
apply bb_simulation; auto.
-
intros. transitivity (Senv.public_symbol (symbolenv L2) id); eapply bsim_public_preserved; eauto.
Qed.
Section FORWARD_TO_BACKWARD.
Context {RETVAL} (L1 L2: _ RETVAL) index order match_states (FS: fsim_properties L1 L2 index order match_states).
Hypothesis L1_receptive: receptive L1.
Hypothesis L2_determinate: determinate L2.
Exploiting forward simulation
Inductive f2b_transitions: state L1 → state L2 → Prop :=
| f2b_trans_final: ∀ s1 s2 s1' r,
Star L1 s1 E0 s1' →
final_state L1 s1' r →
final_state L2 s2 r →
f2b_transitions s1 s2
| f2b_trans_step: ∀ s1 s2 s1' t s1'' s2' i' i'',
Star L1 s1 E0 s1' →
Step L1 s1' t s1'' →
Plus L2 s2 t s2' →
match_states i' s1' s2 →
match_states i'' s1'' s2' →
f2b_transitions s1 s2.
Lemma f2b_progress:
∀ 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 := 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.
-
eapply f2b_trans_final; eauto.
apply star_refl.
eapply fsim_match_final_states; eauto.
-
exploit (fsim_simulation FS); eauto. intros [i' [s2' [A MATCH']]].
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.
intros TRANS; inv TRANS.
× eapply f2b_trans_final; eauto. eapply star_left; eauto.
× eapply f2b_trans_step; eauto. eapply star_left; eauto.
Qed.
Lemma fsim_simulation_not_E0:
∀ s1 t s1', Step L1 s1 t s1' → t ≠ E0 →
∀ i s2, match_states i s1 s2 →
∃ i', ∃ s2', Plus L2 s2 t s2' ∧ match_states i' s1' s2'.
Proof.
intros. exploit (fsim_simulation FS); eauto. intros [i' [s2' [A B]]].
∃ i'; ∃ s2'; split; auto.
destruct A. auto. destruct H2. exploit star_inv; eauto. intros [[EQ1 EQ2] | P]; auto.
congruence.
Qed.
Exploiting determinacy
Remark silent_or_not_silent:
∀ t, t = E0 ∨ t ≠ E0.
Proof.
intros; unfold E0; destruct t; auto; right; congruence.
Qed.
Remark not_silent_length:
∀ t1 t2, (length (t1 ** t2) ≤ 1)%nat → t1 = E0 ∨ t2 = E0.
Proof.
unfold Eapp, E0; intros. rewrite app_length in H.
destruct t1; destruct t2; auto. simpl in H. omegaContradiction.
Qed.
Lemma f2b_determinacy_inv:
∀ s2 t' s2' t'' s2'',
Step L2 s2 t' s2' → Step L2 s2 t'' s2'' →
(t' = E0 ∧ t'' = E0 ∧ s2' = s2'')
∨ (t' ≠ E0 ∧ t'' ≠ E0 ∧ match_traces (symbolenv L1) t' t'').
Proof.
intros.
assert (match_traces (symbolenv L2) t' t'').
eapply sd_determ_1; eauto.
destruct (silent_or_not_silent t').
subst. inv H1.
left; intuition. eapply sd_determ; 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).
Qed.
Lemma f2b_determinacy_star:
∀ s s1, Star L2 s E0 s1 →
∀ t s2 s3,
Step L2 s1 t s2 → t ≠ E0 →
Star L2 s t s3 →
Star L2 s1 t s3.
Proof.
intros s0 s01 ST0. pattern s0, s01. eapply star_E0_ind; eauto.
intros. inv H3. congruence.
exploit f2b_determinacy_inv. eexact H. eexact H4.
intros [[EQ1 [EQ2 EQ3]] | [NEQ1 [NEQ2 MT]]].
subst. simpl in ×. eauto.
congruence.
Qed.
Orders
Inductive f2b_index : Type :=
| F2BI_before (n: nat)
| F2BI_after (n: nat).
Inductive f2b_order: f2b_index → f2b_index → Prop :=
| f2b_order_before: ∀ n n',
(n' < n)%nat →
f2b_order (F2BI_before n') (F2BI_before n)
| f2b_order_after: ∀ n n',
(n' < n)%nat →
f2b_order (F2BI_after n') (F2BI_after n)
| f2b_order_switch: ∀ n n',
f2b_order (F2BI_before n') (F2BI_after n).
Lemma wf_f2b_order:
well_founded f2b_order.
Proof.
assert (ACC1: ∀ n, Acc f2b_order (F2BI_before n)).
intros n0; pattern n0; apply lt_wf_ind; intros.
constructor; intros. inv H0. auto.
assert (ACC2: ∀ n, Acc f2b_order (F2BI_after n)).
intros n0; pattern n0; apply lt_wf_ind; intros.
constructor; intros. inv H0. auto. auto.
red; intros. destruct a; auto.
Qed.
Constructing the backward simulation
Inductive f2b_match_states: f2b_index → state L1 → state L2 → Prop :=
| f2b_match_at: ∀ i s1 s2,
match_states i s1 s2 →
f2b_match_states (F2BI_after O) s1 s2
| f2b_match_before: ∀ 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 →
match_states i s1 s2b →
f2b_match_states (F2BI_before n) s1 s2
| f2b_match_after: ∀ n s2 s2a s1 i,
starN (step L2) (globalenv L2) (S n) s2 E0 s2a →
match_states i s1 s2a →
f2b_match_states (F2BI_after (S n)) s1 s2.
Remark f2b_match_after':
∀ n s2 s2a s1 i,
starN (step L2) (globalenv L2) n s2 E0 s2a →
match_states i s1 s2a →
f2b_match_states (F2BI_after n) s1 s2.
Proof.
intros. inv H.
econstructor; eauto.
econstructor; eauto. econstructor; eauto.
Qed.
Backward simulation of L2 steps
Lemma f2b_simulation_step:
∀ s2 t s2', Step L2 s2 t s2' →
∀ i s1, f2b_match_states i s1 s2 → safe L1 s1 →
∃ i', ∃ s1',
(Plus L1 s1 t s1' ∨ (Star L1 s1 t s1' ∧ f2b_order i' i))
∧ f2b_match_states i' s1' s2'.
Proof.
intros s2 t s2' STEP2 i s1 MATCH SAFE.
inv MATCH.
-
exploit f2b_progress; eauto. intros TRANS; inv TRANS.
+
exploit (sd_final_nostep L2_determinate); eauto. contradiction.
+
inv H2.
exploit f2b_determinacy_inv. eexact H5. eexact STEP2.
intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
×
destruct (silent_or_not_silent t2).
subst. simpl in ×. destruct (star_starN H6) as [n STEPS2].
∃ (F2BI_after n); ∃ s1''; split.
left. eapply plus_right; eauto.
eapply f2b_match_after'; eauto.
subst. simpl in ×. destruct (star_starN H6) as [n STEPS2].
∃ (F2BI_before n); ∃ s1'; split.
right; split. auto. constructor.
econstructor. eauto. auto. apply star_one; eauto. eauto. eauto.
×
exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
congruence.
subst t2. rewrite E0_right in H1.
exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1].
exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto.
intros [i''' [s2''' [P Q]]]. inv P.
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.
intros. elim NOT2. inv H8. auto.
subst t2. rewrite E0_right in ×.
assert (s4 = s2'). eapply sd_determ_2; eauto. subst s4.
destruct (star_starN H7) as [n STEPS2]. ∃ (F2BI_after n); ∃ s1'''; split.
left. eapply plus_right; eauto.
eapply f2b_match_after'; eauto.
-
inv H2. congruence.
exploit f2b_determinacy_inv. eexact H4. eexact STEP2.
intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]].
+
subst. simpl in ×. ∃ (F2BI_before n0); ∃ s1; split.
right; split. apply star_refl. constructor. omega.
econstructor; eauto. eapply star_right; eauto.
+
exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ].
congruence.
subst. rewrite E0_right in ×.
exploit (sr_receptive L1_receptive); eauto. intros [s1''' STEP1].
exploit fsim_simulation_not_E0. eexact STEP1. auto. eauto.
intros [i''' [s2''' [P Q]]].
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 ×.
assert (s3 = s2'). eapply sd_determ_2; eauto. subst s3.
destruct (star_starN H6) as [n STEPS2]. ∃ (F2BI_after n); ∃ s1'''; split.
left. apply plus_one; auto.
eapply f2b_match_after'; eauto.
-
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. ∃ (F2BI_after n); ∃ s1; split.
right; split. apply star_refl. constructor; omega.
eapply f2b_match_after'; eauto.
congruence.
Qed.
End FORWARD_TO_BACKWARD.
The backward simulation
Lemma forward_to_backward_simulation:
∀ {RETVAL: Type},
∀ L1 L2: _ RETVAL,
forward_simulation L1 L2 → receptive L1 → determinate L2 →
backward_simulation L1 L2.
Proof.
intro RETVAL.
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.
-
apply wf_f2b_order.
-
intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2 [A B]]].
∃ s2; auto.
-
intros. exploit (fsim_match_initial_states FS); eauto. intros [i [s2' [A B]]].
assert (s2 = s2') by (eapply sd_initial_determ; eauto). subst s2'.
∃ (F2BI_after O); ∃ s1; split; auto. econstructor; eauto.
-
intros. inv H.
exploit @f2b_progress; eauto. intros TRANS; inv TRANS.
assert (r0 = r) by (eapply (sd_final_determ L2_determinate); eauto). subst r0.
∃ s1'; auto.
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.
-
intros. inv H.
exploit @f2b_progress; eauto. intros TRANS; inv TRANS.
left; ∃ r; auto.
inv H3. right; econstructor; econstructor; eauto.
inv H4. congruence. right; econstructor; econstructor; eauto.
inv H1. right; econstructor; econstructor; eauto.
-
eapply f2b_simulation_step; eauto.
-
exact (fsim_public_preserved FS).
Qed.
Definition well_behaved_traces {RETVAL: Type} (L: semantics RETVAL) : Prop :=
∀ s t s', Step L s t s' →
match t with nil ⇒ True | ev :: t' ⇒ output_trace t' end.
Section ATOMIC.
Context {RETVAL: Type}.
Variable L: semantics RETVAL.
Hypothesis Lwb: well_behaved_traces L.
Inductive atomic_step (ge: genvtype L): (trace × state L) → trace → (trace × state L) → Prop :=
| atomic_step_silent: ∀ s s',
Step L s E0 s' →
atomic_step ge (E0, s) E0 (E0, s')
| atomic_step_start: ∀ s ev t s',
Step L s (ev :: t) s' →
atomic_step ge (E0, s) (ev :: nil) (t, s')
| atomic_step_continue: ∀ ev t s,
output_trace (ev :: t) →
atomic_step ge (ev :: t, s) (ev :: nil) (t, s).
Definition atomic : semantics RETVAL := {|
state := (trace × state L)%type;
genvtype := genvtype L;
step := atomic_step;
initial_state := fun s ⇒ initial_state L (snd s) ∧ fst s = E0;
final_state := fun s r ⇒ final_state L (snd s) r ∧ fst s = E0;
globalenv := globalenv L;
symbolenv := symbolenv L
|}.
End ATOMIC.
A forward simulation from a semantics L1 to a single-event semantics L2
can be "factored" into a forward simulation from atomic L1 to L2.
Section FACTOR_FORWARD_SIMULATION.
Context {RETVAL: Type}.
Variable L1: semantics RETVAL.
Variable L2: semantics RETVAL.
Context index order match_states (sim: fsim_properties L1 L2 index order match_states).
Hypothesis L2single: single_events L2.
Inductive ffs_match: index → (trace × state L1) → state L2 → Prop :=
| ffs_match_at: ∀ i s1 s2,
match_states i s1 s2 →
ffs_match i (E0, s1) s2
| ffs_match_buffer: ∀ i ev t s1 s2 s2',
Star L2 s2 (ev :: t) s2' → match_states i s1 s2' →
ffs_match i (ev :: t, s1) s2.
Lemma star_non_E0_split':
∀ s2 t s2', Star L2 s2 t s2' →
match t with
| nil ⇒ True
| ev :: t' ⇒ ∃ 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.
destruct IHstar as [s2x [A B]]. ∃ s2x; split; auto.
eapply plus_left. eauto. apply plus_star; eauto. auto.
destruct t1. simpl in ×. subst t. ∃ s2; split; auto. apply plus_one; auto.
simpl in LEN. omegaContradiction.
Qed.
Lemma ffs_simulation:
∀ s1 t s1', Step (atomic L1) s1 t s1' →
∀ i s2, ffs_match i s1 s2 →
∃ i', ∃ s2',
(Plus L2 s2 t s2' ∨ (Star L2 s2 t s2') ∧ order i' i)
∧ ffs_match i' s1' s2'.
Proof.
induction 1; intros.
-
inv H0.
exploit (fsim_simulation sim); eauto.
intros [i' [s2' [A B]]].
∃ i'; ∃ s2'; split. auto. constructor; auto.
-
inv H0.
exploit (fsim_simulation sim); eauto.
intros [i' [s2' [A B]]].
destruct t as [ | ev' t].
+
∃ i'; ∃ s2'; split. auto. constructor; auto.
+
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]].
∃ i'; ∃ s2x; split. auto. econstructor; eauto.
-
inv H0.
exploit star_non_E0_split'. eauto. simpl. intros [s2x [P Q]].
destruct t.
∃ i; ∃ s2'; split. left. eapply plus_star_trans; eauto. constructor; auto.
∃ i; ∃ s2x; split. auto. econstructor; eauto.
Qed.
End FACTOR_FORWARD_SIMULATION.
Theorem factor_forward_simulation:
∀ {RETVAL: Type},
∀ L1 L2: _ RETVAL,
forward_simulation L1 L2 → single_events L2 →
forward_simulation (atomic L1) L2.
Proof.
intro RETVAL.
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.
-
eapply fsim_order_wf; eauto.
-
intros. destruct s1 as [t1 s1]. simpl in H. destruct H. subst.
exploit (fsim_match_initial_states sim); eauto. intros [i [s2 [A B]]].
∃ i; ∃ s2; split; auto. constructor; auto.
-
intros. destruct s1 as [t1 s1]. simpl in H0; destruct H0; subst. inv H.
eapply (fsim_match_final_states sim); eauto.
-
eapply ffs_simulation; eauto.
-
simpl. exact (fsim_public_preserved sim).
Qed.
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.
Section FACTOR_BACKWARD_SIMULATION.
Context {RETVAL: Type}.
Variable L1: semantics RETVAL.
Variable L2: semantics RETVAL.
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: index → state L1 → (trace × state L2) → Prop :=
| fbs_match_intro: ∀ i s1 t s2 s1',
Star L1 s1 t s1' → match_states i s1' s2 →
t = E0 ∨ output_trace t →
fbs_match i s1 (t, s2).
Lemma fbs_simulation:
∀ s2 t s2', Step (atomic L2) s2 t s2' →
∀ i s1, fbs_match i s1 s2 → safe L1 s1 →
∃ i', ∃ s1',
(Plus L1 s1 t s1' ∨ (Star L1 s1 t s1' ∧ order i' i))
∧ fbs_match i' s1' s2'.
Proof.
induction 1; intros.
-
inv H0.
exploit (bsim_simulation sim); eauto. eapply star_safe; eauto.
intros [i' [s1'' [A B]]].
∃ i'; ∃ 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.
-
inv H0.
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.
exploit @star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
∃ i'; ∃ s1x; split.
left; auto.
econstructor; eauto.
exploit L2wb; eauto.
-
inv H0. unfold E0 in H8; destruct H8; try congruence.
exploit @star_non_E0_split'; eauto. simpl. intros [s1x [P Q]].
∃ i; ∃ s1x; split. left; auto. econstructor; eauto. simpl in H0; tauto.
Qed.
Lemma fbs_progress:
∀ i s1 s2,
fbs_match i s1 s2 → safe L1 s1 →
(∃ r, final_state (atomic L2) s2 r) ∨
(∃ t, ∃ s2', Step (atomic L2) s2 t s2').
Proof.
intros. inv H. destruct t.
-
exploit (bsim_progress sim); eauto. eapply star_safe; eauto.
intros [[r A] | [t [s2' A]]].
+
left; ∃ r; simpl; auto.
+
destruct t.
right; ∃ E0; ∃ (nil, s2'). constructor. auto.
right; ∃ (e :: nil); ∃ (t, s2'). constructor. auto.
-
unfold E0 in H3; destruct H3. congruence.
right; ∃ (e :: nil); ∃ (t, s3). constructor. auto.
Qed.
End FACTOR_BACKWARD_SIMULATION.
Theorem factor_backward_simulation:
∀ {RETVAL: Type},
∀ L1 L2: _ RETVAL,
backward_simulation L1 L2 → single_events L1 → well_behaved_traces L2 →
backward_simulation L1 (atomic L2).
Proof.
intro RETVAL.
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.
-
eapply bsim_order_wf; eauto.
-
intros. exploit (bsim_initial_states_exist sim); eauto. intros [s2 A].
∃ (E0, s2). simpl; auto.
-
intros. destruct s2 as [t s2]; simpl in H0; destruct H0; subst.
exploit (bsim_match_initial_states sim); eauto. intros [i [s1' [A B]]].
∃ i; ∃ s1'; split. auto. econstructor. apply star_refl. auto. auto.
-
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]]. ∃ s1''; split; auto. eapply star_trans; eauto.
-
eapply fbs_progress; eauto.
-
eapply fbs_simulation; eauto.
-
simpl. exact (bsim_public_preserved sim).
Qed.
Record strongly_receptive {RETVAL: Type} (L: semantics RETVAL) : Prop :=
Strongly_receptive {
ssr_receptive: ∀ s ev1 t1 s1 ev2,
Step L s (ev1 :: t1) s1 →
match_traces (symbolenv L) (ev1 :: nil) (ev2 :: nil) →
∃ s2, ∃ t2, Step L s (ev2 :: t2) s2;
ssr_well_behaved:
well_behaved_traces L
}.
Theorem atomic_receptive:
∀ {RETVAL: Type},
∀ (L: _ RETVAL), strongly_receptive L → receptive (atomic L).
Proof.
intros. constructor; intros.
inv H0.
inv H1. ∃ (E0, s'). constructor; auto.
assert (∃ 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.
∃ (t2, s2). constructor; auto.
simpl in H2; destruct H2.
assert (t2 = ev :: nil). inv H1; simpl in H0; tauto.
subst t2. ∃ (t, s0). constructor; auto. simpl; auto.
red. intros. inv H0; simpl; omega.
Qed.
Record bigstep_semantics (RETVAL: Type) : Type :=
Bigstep_semantics {
bigstep_terminates: trace → RETVAL → Prop;
bigstep_diverges: traceinf → Prop
}.
Soundness with respect to a small-step semantics
Record bigstep_sound {RETVAL: Type} (B: bigstep_semantics RETVAL) (L: semantics RETVAL) : Prop :=
Bigstep_sound {
bigstep_terminates_sound:
∀ t r,
bigstep_terminates B t r →
∃ s1, ∃ s2, initial_state L s1 ∧ Star L s1 t s2 ∧ final_state L s2 r;
bigstep_diverges_sound:
∀ T,
bigstep_diverges B T →
∃ s1, initial_state L s1 ∧ forever (step L) (globalenv L) s1 T
}.