Lvc.Equiv.Bisim
Require Import List.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL AllInRel.
Require Export EventsActivated StateType paco Equiv.
Set Implicit Arguments.
Unset Printing Records.
Require Export Util Var Val Exp Env Map CSet AutoIndTac IL AllInRel.
Require Export EventsActivated StateType paco Equiv.
Set Implicit Arguments.
Unset Printing Records.
Simulation
A characterization of simulation equivalence on states; works only for deterministic semanticsCoInductive bisim {S} `{StateType S} {S´} `{StateType S´} : S → S´ → Prop :=
| bisimSilent (σ1 σ1´:S) (σ2 σ2´:S´) :
plus2 step σ1 nil σ1´
→ plus2 step σ2 nil σ2´
→ bisim σ1´ σ2´
→ bisim σ1 σ2
| bisimExtern (pσ1 σ1:S) (pσ2 σ2:S´) :
star2 step pσ1 nil σ1
→ star2 step pσ2 nil σ2
→ activated σ1
→ activated σ2
→ (∀ evt σ1´, step σ1 evt σ1´ → ∃ σ2´, step σ2 evt σ2´ ∧ bisim σ1´ σ2´)
→ (∀ evt σ2´, step σ2 evt σ2´ → ∃ σ1´, step σ1 evt σ1´ ∧ bisim σ1´ σ2´)
→ bisim pσ1 pσ2
| bisimTerm (σ1 σ1´:S) (σ2 σ2´:S´)
: result σ1´ = result σ2´
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ normal2 step σ1´
→ normal2 step σ2´
→ bisim σ1 σ2.
Arguments bisim [S] {H} [S´] {H0} _ _.
Simulation is an equivalence relation
Lemma bisim_refl {S} `{StateType S} (σ:S)
: bisim σ σ.
Proof.
revert σ. cofix.
intros. destruct (step_dec σ) as [[[] []]|].
- eapply bisimExtern; intros; eauto using star2_refl; eexists; eauto.
- eapply bisimSilent; eauto using plus2O.
- eapply bisimTerm; eauto using star2_refl.
Qed.
Lemma bisim_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
: bisim σ σ´ → bisim σ´ σ.
Proof.
revert σ σ´. cofix; intros.
inv H1.
- eapply bisimSilent; eauto.
- eapply bisimExtern; eauto; intros.
edestruct H7; eauto; dcr. eexists; eauto.
edestruct H6; eauto; dcr. eexists; eauto.
- eapply bisimTerm; eauto using star2_refl.
Qed.
Inductive bisim_gen
{S} `{StateType S} {S´} `{StateType S´} (r: S → S´ → Prop) : S → S´ → Prop :=
| bisim´Silent (σ1 σ1´:S) (σ2 σ2´:S´) :
plus2 step σ1 nil σ1´
→ plus2 step σ2 nil σ2´
→ r σ1´ σ2´
→ bisim_gen r σ1 σ2
| bisim´Extern (pσ1 σ1:S) (pσ2 σ2:S´) :
star2 step pσ1 nil σ1
→ star2 step pσ2 nil σ2
→ activated σ1
→ activated σ2
→ (∀ evt σ1´, step σ1 evt σ1´ → ∃ σ2´, step σ2 evt σ2´ ∧ r σ1´ σ2´)
→ (∀ evt σ2´, step σ2 evt σ2´ → ∃ σ1´, step σ1 evt σ1´ ∧ r σ1´ σ2´)
→ bisim_gen r pσ1 pσ2
| bisim´Term (σ1 σ1´:S) (σ2 σ2´:S´)
: result σ1´ = result σ2´
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ normal2 step σ1´
→ normal2 step σ2´
→ bisim_gen r σ1 σ2.
Arguments bisim_gen [S] {H} [S´] {H0} r _ _.
Hint Constructors bisim_gen.
Definition bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
:= paco2 (@bisim_gen S _ S´ _) bot2 σ1 σ2.
Hint Unfold bisim´.
Definition bisim´r {S} `{StateType S} {S´} `{StateType S´} r (σ1:S) (σ2:S´)
:= paco2 (@bisim_gen S _ S´ _) r σ1 σ2.
Hint Unfold bisim´.
Lemma bisim_gen_mon {S} `{StateType S} {S´} `{StateType S´}
: monotone2 (@bisim_gen S _ S´ _).
Proof.
hnf; intros. inv IN.
- econstructor 1; eauto.
- econstructor 2; eauto; intros.
edestruct H5; eauto; dcr. eexists; eauto.
edestruct H6; eauto; dcr. eexists; eauto.
- econstructor 3; eauto.
Qed.
Arguments bisim_gen_mon [S] {H} [S´] {H0} [x0] [x1] r r´ IN LE.
Hint Resolve bisim_gen_mon : paco.
Lemma bisim_bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim σ1 σ2 → bisim´ σ1 σ2.
Proof.
revert σ1 σ2. pcofix CIH.
intros. pfold.
inv H2.
- econstructor; eauto.
- econstructor 2; eauto; intros.
+ edestruct H6; eauto; dcr. eexists; eauto.
+ edestruct H7; eauto; dcr. eexists; eauto.
- econstructor 3; eauto.
Qed.
Lemma bisim´_bisim {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim´ σ1 σ2 → bisim σ1 σ2.
Proof.
revert σ1 σ2. cofix CIH.
intros.
(assert (bisim_gen (paco2 (bisim_gen (S´:=S´)) bot2 \2/ bot2) σ1 σ2)).
punfold H1.
destruct H2. destruct H4.
- econstructor; eauto.
- exfalso; intuition.
- econstructor 2; eauto; intros.
+ edestruct H6; eauto; dcr. destruct H11. eexists; eauto. exfalso; intuition.
+ edestruct H7; eauto; dcr. destruct H11. eexists; eauto. exfalso; intuition.
- econstructor 3; eauto.
Qed.
Lemma bisim´_refl {S} `{StateType S} (σ:S)
: bisim´ σ σ.
Proof.
eapply bisim_bisim´. eapply bisim_refl.
Qed.
Lemma bisim´_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
: bisim´ σ σ´ → bisim´ σ´ σ.
Proof.
intros. eapply bisim_bisim´. eapply bisim_sym. eapply bisim´_bisim; eauto.
Qed.
Lemma bisim´_expansion_closed {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´) r
: bisim´r r σ1´ σ2´
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ bisim´r r σ1 σ2.
Proof.
intros. pinversion H1; subst; pfold.
- econstructor; eauto.
+ eapply (star2_plus2_plus2 H2 H4).
+ eapply (star2_plus2_plus2 H3 H5).
- econstructor 2.
+ eapply (star2_trans H2 H4).
+ eapply (star2_trans H3 H5).
+ eauto.
+ eauto.
+ intros. edestruct H6; eauto.
+ intros. edestruct H7; eauto.
- econstructor 3; eauto using star2_trans.
+ eapply (star2_trans H2 H5).
+ eapply (star2_trans H3 H6).
Qed.
Lemma bisim´_reduction_closed_1 {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2:S´)
: bisim´ σ1 σ2
→ star2 step σ1 nil σ1´
→ bisim´ σ1´ σ2.
Proof.
intros. eapply star2_star2n in H2. destruct H2 as [n ?].
revert σ1 σ1´ σ2 H1 H2.
pattern n.
eapply size_induction with (f:=id); intros; unfold id in *; simpl in ×.
pinversion H2; subst.
- inv H3; eauto.
eapply plus2_plus2n in H4. destruct H4. eapply plus2n_star2n in H4.
edestruct (star2n_reach H3 H4); eauto. eapply H.
+ eapply bisim´_expansion_closed. eapply H6.
eauto using star2n_star2. eauto using plus2_star2.
+ eapply H1; try eapply H9. omega.
eapply bisim´_expansion_closed. eapply H6. eapply star2_refl.
eauto using plus2_star2.
- eapply star2n_star2 in H3. eapply activated_star_reach in H3; eauto.
- pfold. eapply star2n_star2 in H3.
eapply star2_reach_normal in H3; eauto. eapply H.
Qed.
Lemma bisim´_terminate {S1} `{StateType S1} (σ1 σ1´:S1)
{S2} `{StateType S2} (σ2:S2)
: star2 step σ1 nil σ1´
→ normal2 step σ1´
→ bisim´ σ1 σ2
→ ∃ σ2´, star2 step σ2 nil σ2´ ∧ normal2 step σ2´ ∧ result σ1´ = result σ2´.
Proof.
intros. general induction H1.
- pinversion H3; subst.
+ exfalso. eapply H2. inv H1; do 2 eexists; eauto.
+ exfalso. eapply star2_normal in H1; eauto. subst.
eapply (activated_normal _ H5); eauto.
+ eapply star2_normal in H4; eauto; subst.
eexists; split; eauto.
- destruct y; isabsurd. simpl.
eapply IHstar2; eauto.
eapply bisim´_reduction_closed_1; eauto using star2.
eapply (S_star2 _ _ H); eauto using star2_refl.
Qed.
Lemma bisim´_activated {S1} `{StateType S1} (σ1:S1)
{S2} `{StateType S2} (σ2:S2)
: activated σ1
→ bisim´ σ1 σ2
→ ∃ σ2´, star2 step σ2 nil σ2´ ∧ activated σ2´ ∧
( ∀ (evt : event) (σ1´´ : S1),
step σ1 evt σ1´´ →
∃ σ2´´ : S2,
step σ2´ evt σ2´´ ∧
(paco2 (bisim_gen (S´:=S2)) bot2 σ1´´ σ2´´))
∧
( ∀ (evt : event) (σ2´´ : S2),
step σ2´ evt σ2´´ →
∃ σ1´ : S1,
step σ1 evt σ1´ ∧
(paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´´)).
Proof.
intros.
pinversion H2; subst.
- exfalso. edestruct (plus2_destr_nil H3); dcr.
destruct H1 as [? []].
exploit (step_internally_deterministic _ _ _ _ H7 H1); dcr; congruence.
- assert (σ1 = σ0). eapply activated_star_eq; eauto. subst σ1.
eexists σ3; split; eauto. split; eauto. split.
intros. edestruct H7; eauto; dcr. destruct H12; isabsurd.
eexists; split; eauto.
intros. edestruct H8; eauto; dcr. destruct H12; isabsurd.
eexists; split; eauto.
- exfalso. refine (activated_normal_star _ H1 _ _); eauto using star2.
Qed.
Lemma plus_step_activated {S1} `{StateType S1} (σ1 σ1´:S1)
{S2} `{StateType S2} (σ2a σ2´ σ2b σ4:S2)
{S3} `{StateType S3} (σ3 σ5:S3) (r : S1 → S3 → Prop)
(H6:plus2 step σ2a nil σ2´)
(H2:star2 step σ2a nil σ2b)
(H10:star2 step σ2b nil σ4)
(H11 : star2 step σ3 nil σ5)
(H4 : plus2 step σ1 nil σ1´)
(H13 : activated σ5)
(H12 : activated σ4)
(H7 : paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´)
(H14 : ∀ (evt : event) (σ1´ : S2),
step σ4 evt σ1´ →
∃ σ2´ : S3,
step σ5 evt σ2´ ∧
(paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
(H15 : ∀ (evt : event) (σ2´ : S3),
step σ5 evt σ2´ →
∃ σ1´ : S2,
step σ4 evt σ1´ ∧
(paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
(CIH : ∀ (σ1 : S1) (σ2a σ2b : S2) (σ3 : S3),
bisim´ σ1 σ2a →
star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a →
bisim´ σ2b σ3 → r σ1 σ3)
: paco2 (bisim_gen (S´:=S3)) r σ1 σ3.
Proof.
pfold.
eapply star2_trans in H10; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H6.
exploit (activated_star_reach H12 H10 H6); eauto.
eapply bisim´_sym in H7.
eapply bisim´_reduction_closed_1 in H7; eauto.
destruct (bisim´_activated H12 H7); dcr.
econstructor 2.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H3). eapply H11.
eauto. eauto.
+ intros. edestruct H16; eauto. destruct H9.
edestruct H14; eauto. dcr.
eexists; split; eauto. destruct H20; isabsurd.
right. eapply CIH. eapply bisim´_sym in H17. eauto.
left. eapply star2_refl. eauto.
+ intros. edestruct H15; eauto; dcr.
edestruct H5; eauto; dcr. destruct H9.
eexists; split; eauto. destruct H18; isabsurd.
right. eapply CIH. eapply bisim´_sym. eapply H19.
left; eapply star2_refl.
eauto.
Qed.
Lemma bisim´_zigzag {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2a σ2b:S2) {S3} `{StateType S3} (σ3:S3)
: bisim´ σ1 σ2a
→ (star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a)
→ bisim´ σ2b σ3
→ bisim´ σ1 σ3.
Proof.
revert σ1 σ2a σ2b σ3. pcofix CIH; intros.
destruct H4.
- {
pinversion H3; pinversion H5; subst.
- pfold. eapply star2_plus2_plus2 in H10; eauto. clear H2; simpl in ×.
edestruct (plus2_reach H6 H10); eauto.
eapply H0.
-
eapply (@plus_step_activated S1 _ _ _ S2 _ _ _ _ _ S3); eauto.
-
eapply star2_trans in H11; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H6.
exploit (star2_reach_normal H11 H6); eauto. eapply H0.
edestruct (bisim´_terminate X H13 (bisim´_sym H7)); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H10. eapply H10.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8); eauto.
eauto. eauto. eauto.
-
pfold.
eapply plus2_star2 in H13.
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
exploit (activated_star_reach H8 H6 H13); eauto.
eapply bisim´_reduction_closed_1 in H15; eauto.
destruct (bisim´_activated H8 H15); dcr.
econstructor 2. eauto.
eapply plus2_star2 in H14.
eapply (star2_trans H14 H11). eauto.
eauto.
+ intros.
edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H12 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto.
left; eapply star2_refl.
-
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
exploit (both_activated H6 H13); eauto. subst.
pfold. econstructor 2; eauto; intros.
+ edestruct H9; eauto. dcr.
edestruct H17; eauto; dcr.
eexists. split; eauto.
destruct H19, H21; isabsurd.
right. eapply CIH; try eapply H11; try eapply H19.
left. eapply star2_refl.
+ edestruct H18; eauto. dcr.
edestruct H10; eauto; dcr.
eexists. split; eauto.
destruct H19, H21; isabsurd.
right. eapply CIH; try eapply H11; try eapply H19.
left. eapply star2_refl.
-
eapply star2_trans in H14; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H6); eauto.
-
eapply plus2_star2 in H12.
eapply star2_trans in H12; eauto. clear H2; simpl in ×.
exploit (star2_reach_normal H7 H12); eauto. eapply H0.
edestruct (bisim´_terminate X H9 H14); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H4. eapply H4.
eauto.
eapply plus2_star2 in H13.
eapply (star2_trans H13 H10); eauto.
eauto. eauto.
- eapply star2_trans in H12; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H12 H14 H7); eauto.
-
pfold.
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
edestruct (star2_reach H7 H13); eauto. eapply H0.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H9. do 2 eexists; eauto.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H15. do 2 eexists; eauto.
}
-{
pinversion H3; pinversion H5; subst.
- pfold. eapply star2_plus2_plus2 in H6; eauto. clear H2; simpl in ×.
edestruct (plus2_reach H6 H10); eauto.
eapply H0.
-
pfold.
eapply plus2_star2 in H6.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (activated_star_reach H12 H10 H6); eauto.
eapply bisim´_sym in H7.
eapply bisim´_reduction_closed_1 in H7; eauto.
destruct (bisim´_activated H12 H7); dcr.
econstructor 2.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8). eapply H11.
eauto. eauto.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H14 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH. eapply bisim´_sym in H19; eauto.
left. eapply star2_refl. eauto.
+ intros.
edestruct H15 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H9 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH. eapply bisim´_sym in H21; eauto.
left; eapply star2_refl. eauto.
-
eapply plus2_star2 in H6.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (star2_reach_normal H11 H6); eauto. eapply H0.
edestruct (bisim´_terminate X H13 (bisim´_sym H7)); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H10. eapply H10.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8); eauto.
eauto. eauto. eauto.
-
pfold.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H13.
exploit (activated_star_reach H8 H6 H13); eauto.
eapply bisim´_reduction_closed_1 in H15; eauto.
destruct (bisim´_activated H8 H15); dcr.
econstructor 2. eauto.
eapply plus2_star2 in H14.
eapply (star2_trans H14 H11). eauto.
eauto.
+ intros.
edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H12 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto.
left; eapply star2_refl.
-
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (both_activated H6 H13); eauto. subst.
pfold. econstructor 2; eauto; intros.
+ edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H17 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ edestruct H18 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
-
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H6 H8 H14); eauto.
-
eapply star2_trans in H7; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H12.
exploit (star2_reach_normal H7 H12); eauto. eapply H0.
edestruct (bisim´_terminate X H9 H14); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H4. eapply H4.
eauto.
eapply plus2_star2 in H13.
eapply (star2_trans H13 H10); eauto.
eauto. eauto.
- eapply star2_trans in H7; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H12 H14 H7); eauto.
-
pfold.
eapply star2_trans in H7; eauto. clear H2; simpl in ×.
edestruct (star2_reach H7 H13); eauto. eapply H0.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H9. do 2 eexists; eauto.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H15. do 2 eexists; eauto.
}
Qed.
Lemma bisim´_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: bisim´ σ1 σ2
→ bisim´ σ2 σ3
→ bisim´ σ1 σ3.
Proof.
intros. eauto using (bisim´_zigzag (S1:=S1) (S2:=S2) (S3:=S3)), star2_refl.
Qed.
Lemma bisim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: bisim σ1 σ2
→ bisim σ2 σ3
→ bisim σ1 σ3.
Proof.
intros. eapply bisim´_bisim.
eapply bisim_bisim´ in H2.
eapply bisim_bisim´ in H3.
eapply (bisim´_trans H2 H3).
Qed.
Lemma bisim´_reduction_closed {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´)
: bisim´ σ1 σ2
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ bisim´ σ1´ σ2´.
Proof.
intros. eapply bisim´_trans.
eapply bisim´_reduction_closed_1; eauto.
eapply bisim´_sym.
eapply bisim´_sym in H1.
eapply bisim´_reduction_closed_1; eauto.
eapply bisim´_refl.
Qed.
Instance bisim_progeq : ProgramEquivalence F.state F.state.
constructor. eapply (paco2 (@bisim_gen F.state _ F.state _)).
Defined.
Lemma simL_mon (r r0:rel2 F.state (fun _ : F.state ⇒ F.state)) A AR L1 L2 (AL:list A) L1´ L2´
: AIR5 (simB bisim_progeq r AR) L1 L2 AL L1´ L2´
→ (∀ x0 x1 : F.state, r x0 x1 → r0 x0 x1)
→ L1 = L1´
→ L2 = L2´
→ AIR5 (simB bisim_progeq r0 AR) L1 L2 AL L1´ L2´.
Proof.
intros. general induction H; eauto using AIR5.
econstructor; eauto.
inv pf. econstructor; eauto.
intros. eapply paco2_mon; eauto. eapply H3; eauto.
Qed.
Lemma subst_lemma A AR (a:A) AL s s´ V V´ E E´ Z Z´ L1 L2 t t´
: fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ ParamRel a Z Z´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ simL´ bisim_progeq bot2 AR AL L1 L2
→ (∀ r (L L´ : list F.block),
simL´ bisim_progeq r AR (a :: AL) L L´ →
paco2 (@bisim_gen F.state _ F.state _) r (L, V, t) (L´, V´, t´))
→ paco2 (@bisim_gen F.state _ F.state _) bot2 (F.blockI E Z s :: L1, V, t)
(F.blockI E´ Z´ s´ :: L2, V´, t´).
Proof.
revert_all; pcofix CIH; intros.
eapply H4.
econstructor. econstructor; eauto.
intros. pfold.
econstructor; try eapply plus2O.
econstructor; eauto using get; simpl.
edestruct RelsOK; eauto.
eapply omap_length in H. congruence. reflexivity.
econstructor; eauto using get; simpl. edestruct RelsOK; eauto.
eapply omap_length in H5. congruence. reflexivity.
simpl.
right. eapply CIH; eauto.
intros. eapply H0; eauto.
eapply simL_mon; eauto. intros; isabsurd.
Qed.
Lemma fix_compatible r A AR (a:A) AL s s´ E E´ Z Z´ L L´ Yv Y´v
: simL´ bisim_progeq r AR AL L L´
→ fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ ParamRel a Z Z´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ ArgRel E E´ a Yv Y´v
→ bisim´r r
(F.blockI E Z s :: L, E [Z <-- List.map Some Yv], s)
(F.blockI E´ Z´ s´ :: L´, E´ [Z´ <-- List.map Some Y´v], s´).
Proof.
revert_all; pcofix CIH; intros.
eapply H1; eauto.
hnf; intros. econstructor; eauto. econstructor; eauto; intros.
pfold. econstructor; try eapply plus2O.
- econstructor; eauto using get.
+ simpl. edestruct RelsOK; eauto.
exploit omap_length; try eapply H; eauto.
congruence.
- reflexivity.
- econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H6; eauto.
congruence.
- reflexivity.
- simpl. right. eapply CIH; eauto.
- eapply simL_mon; eauto.
Qed.
Lemma simL_extension´ r A AR (a:A) AL s s´ E E´ Z Z´ L L´
: simL´ bisim_progeq r AR AL L L´
→ fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ simL´ bisim_progeq r AR (a::AL) (F.blockI E Z s :: L) (F.blockI E´ Z´ s´ :: L´).
Proof.
intros. destruct H0.
hnf; intros. econstructor; eauto. econstructor; eauto; intros.
+ pfold. econstructor; try eapply plus2O.
econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H3; eauto.
congruence. reflexivity.
econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H4; eauto.
congruence. reflexivity.
simpl. left.
eapply fix_compatible; eauto. split; eauto.
Qed.
Lemma get_drop_lab0 (L:F.labenv) l blk
: get L (counted l) blk
→ get (drop (labN l) L) (counted (LabI 0)) blk.
Proof.
intros. eapply drop_get; simpl. orewrite (labN l + 0 = labN l); eauto.
Qed.
Lemma drop_get_lab0 (L:F.labenv) l blk
: get (drop (labN l) L) (counted (LabI 0)) blk
→ get L (counted l) blk.
Proof.
intros. eapply get_drop in H; simpl in ×. orewrite (labN l + 0 = labN l) in H; eauto.
Qed.
Lemma bisim_drop_shift r l L E Y L´ E´ Y´
: paco2 (@bisim_gen F.state _ F.state _) r (drop (labN l) L, E, stmtApp (LabI 0) Y)
(drop (labN l) L´, E´, stmtApp (LabI 0) Y´)
→ paco2 (@bisim_gen F.state _ F.state _) r (L, E, stmtApp l Y)
(L´, E´, stmtApp l Y´).
Proof.
intros. pinversion H; subst.
- eapply plus2_destr_nil in H0.
eapply plus2_destr_nil in H1.
destruct H0; destruct H1; dcr. inv H3.
simpl in ×. inv H1; simpl in ×.
pfold. econstructor; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
eauto.
- inv H0.
+ exfalso. destruct H2 as [? [? ?]]. inv H2.
+ inv H1.
× exfalso. destruct H3 as [? [? ?]]. inv H3.
× inv H7; inv H10; simpl in ×.
pfold. subst yl yl0.
econstructor; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H9.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H12.
left. pfold. econstructor 2; try eapply star2_refl; eauto.
- inv H1; inv H2; simpl in ×.
+ pfold. econstructor 3; try eapply star2_refl. reflexivity.
× stuck2. eapply H3. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
× stuck2. eapply H4. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
+ inv H6.
pfold. econstructor 3; [
| eapply star2_refl
|
|
|].
Focus 2. rewrite <- H5. eapply S_star2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
simpl; eauto.
stuck2. eapply H3. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
+ inv H6.
pfold. econstructor 3; [
|
|eapply star2_refl
|
|].
Focus 2. rewrite <- H5. eapply S_star2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
simpl; eauto. eauto.
stuck2. eapply H4. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
+ inv H6; inv H9. pfold. simpl in ×. subst yl yl0.
econstructor 1; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H8.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H11.
left. pfold. econstructor 3; try eapply star2_refl; eauto.
Qed.
Ltac single_step :=
match goal with
| [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = true |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
econstructor; eauto; rewrite <- H; eauto; cset_tac; intuition
| [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = false |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
econstructor 3; eauto; rewrite <- H; eauto; cset_tac; intuition
| [ H : val2bool _ = false |- _ ] ⇒ econstructor 3 ; try eassumption; try reflexivity
| [ H : step (?L, _ , stmtApp ?l _) _, H´: get ?L (counted ?l) _ |- _] ⇒
econstructor; try eapply H´; eauto
| [ H´: get ?L (counted ?l) _ |- step (?L, _ , stmtApp ?l _) _] ⇒
econstructor; try eapply H´; eauto
| _ ⇒ econstructor; eauto
end.
Ltac one_step := eapply bisimSilent; [ eapply plus2O; single_step
| eapply plus2O; single_step
| ].
Ltac no_step := eapply bisimTerm;
try eapply star2_refl; try get_functional; try subst;
[ try reflexivity
| stuck2
| stuck2 ].
Ltac step_activated :=
match goal with
| [ H : omap (exp_eval ?E) ?Y = Some ?vl
|- activated (_, ?E, stmtExtern ?x ?f ?Y ?s) ] ⇒
eexists (ExternI f vl 0); eexists; try (now (econstructor; eauto))
end.
Ltac extern_step :=
let STEP := fresh "STEP" in
eapply bisimExtern;
[ eapply star2_refl
| eapply star2_refl
| try step_activated
| try step_activated
| intros ? ? STEP; inv STEP
| intros ? ? STEP; inv STEP
].
Definition same_call (e e´:extern) := extern_fnc e = extern_fnc e´ ∧ extern_args e = extern_args e´.
Definition receptive S `{StateType S} :=
∀ σ σ´ ext, step σ (EvtExtern ext) σ´
→ ∀ ext´, same_call ext ext´ → ∃ σ´´, step σ (EvtExtern ext´) σ´´.
Arguments receptive S [H].
Definition determinate S `{StateType S} :=
∀ σ σ´ σ´´ ext ext´, step σ (EvtExtern ext) σ´
→ step σ (EvtExtern ext´) σ´´ → same_call ext ext´.
Arguments determinate S [H].
Lemma bisimExternDet {S} `{StateType S} {S´} `{StateType S´} (pσ1:S) (pσ2:S´) (σ1:S) (σ2:S´)
(RCPT:receptive S) (DET:determinate S´)
: star2 step pσ1 nil σ1
→ star2 step pσ2 nil σ2
→ activated σ1
→ (∀ evt σ1´, step σ1 evt σ1´ → ∃ σ2´, step σ2 evt σ2´ ∧ bisim σ1´ σ2´)
→ bisim pσ1 pσ2.
Proof.
intros.
econstructor 2; eauto.
- inv H3. dcr. edestruct H4; eauto. firstorder.
- intros. inv H3. dcr. exploit H4; eauto; dcr.
destruct evt.
+ exploit DET. eauto. eapply H5.
exploit RCPT; eauto. dcr.
exploit H4. eapply H6. dcr.
eexists; split. eapply H6.
exploit step_externally_determined. eapply H11. eapply H5. subst. eauto.
+ exfalso. exploit step_internally_deterministic; eauto; dcr. congruence.
Qed.
: bisim σ σ.
Proof.
revert σ. cofix.
intros. destruct (step_dec σ) as [[[] []]|].
- eapply bisimExtern; intros; eauto using star2_refl; eexists; eauto.
- eapply bisimSilent; eauto using plus2O.
- eapply bisimTerm; eauto using star2_refl.
Qed.
Lemma bisim_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
: bisim σ σ´ → bisim σ´ σ.
Proof.
revert σ σ´. cofix; intros.
inv H1.
- eapply bisimSilent; eauto.
- eapply bisimExtern; eauto; intros.
edestruct H7; eauto; dcr. eexists; eauto.
edestruct H6; eauto; dcr. eexists; eauto.
- eapply bisimTerm; eauto using star2_refl.
Qed.
Inductive bisim_gen
{S} `{StateType S} {S´} `{StateType S´} (r: S → S´ → Prop) : S → S´ → Prop :=
| bisim´Silent (σ1 σ1´:S) (σ2 σ2´:S´) :
plus2 step σ1 nil σ1´
→ plus2 step σ2 nil σ2´
→ r σ1´ σ2´
→ bisim_gen r σ1 σ2
| bisim´Extern (pσ1 σ1:S) (pσ2 σ2:S´) :
star2 step pσ1 nil σ1
→ star2 step pσ2 nil σ2
→ activated σ1
→ activated σ2
→ (∀ evt σ1´, step σ1 evt σ1´ → ∃ σ2´, step σ2 evt σ2´ ∧ r σ1´ σ2´)
→ (∀ evt σ2´, step σ2 evt σ2´ → ∃ σ1´, step σ1 evt σ1´ ∧ r σ1´ σ2´)
→ bisim_gen r pσ1 pσ2
| bisim´Term (σ1 σ1´:S) (σ2 σ2´:S´)
: result σ1´ = result σ2´
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ normal2 step σ1´
→ normal2 step σ2´
→ bisim_gen r σ1 σ2.
Arguments bisim_gen [S] {H} [S´] {H0} r _ _.
Hint Constructors bisim_gen.
Definition bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
:= paco2 (@bisim_gen S _ S´ _) bot2 σ1 σ2.
Hint Unfold bisim´.
Definition bisim´r {S} `{StateType S} {S´} `{StateType S´} r (σ1:S) (σ2:S´)
:= paco2 (@bisim_gen S _ S´ _) r σ1 σ2.
Hint Unfold bisim´.
Lemma bisim_gen_mon {S} `{StateType S} {S´} `{StateType S´}
: monotone2 (@bisim_gen S _ S´ _).
Proof.
hnf; intros. inv IN.
- econstructor 1; eauto.
- econstructor 2; eauto; intros.
edestruct H5; eauto; dcr. eexists; eauto.
edestruct H6; eauto; dcr. eexists; eauto.
- econstructor 3; eauto.
Qed.
Arguments bisim_gen_mon [S] {H} [S´] {H0} [x0] [x1] r r´ IN LE.
Hint Resolve bisim_gen_mon : paco.
Lemma bisim_bisim´ {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim σ1 σ2 → bisim´ σ1 σ2.
Proof.
revert σ1 σ2. pcofix CIH.
intros. pfold.
inv H2.
- econstructor; eauto.
- econstructor 2; eauto; intros.
+ edestruct H6; eauto; dcr. eexists; eauto.
+ edestruct H7; eauto; dcr. eexists; eauto.
- econstructor 3; eauto.
Qed.
Lemma bisim´_bisim {S} `{StateType S} {S´} `{StateType S´} (σ1:S) (σ2:S´)
: bisim´ σ1 σ2 → bisim σ1 σ2.
Proof.
revert σ1 σ2. cofix CIH.
intros.
(assert (bisim_gen (paco2 (bisim_gen (S´:=S´)) bot2 \2/ bot2) σ1 σ2)).
punfold H1.
destruct H2. destruct H4.
- econstructor; eauto.
- exfalso; intuition.
- econstructor 2; eauto; intros.
+ edestruct H6; eauto; dcr. destruct H11. eexists; eauto. exfalso; intuition.
+ edestruct H7; eauto; dcr. destruct H11. eexists; eauto. exfalso; intuition.
- econstructor 3; eauto.
Qed.
Lemma bisim´_refl {S} `{StateType S} (σ:S)
: bisim´ σ σ.
Proof.
eapply bisim_bisim´. eapply bisim_refl.
Qed.
Lemma bisim´_sym {S} `{StateType S} {S´} `{StateType S´} (σ:S) (σ´:S´)
: bisim´ σ σ´ → bisim´ σ´ σ.
Proof.
intros. eapply bisim_bisim´. eapply bisim_sym. eapply bisim´_bisim; eauto.
Qed.
Lemma bisim´_expansion_closed {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´) r
: bisim´r r σ1´ σ2´
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ bisim´r r σ1 σ2.
Proof.
intros. pinversion H1; subst; pfold.
- econstructor; eauto.
+ eapply (star2_plus2_plus2 H2 H4).
+ eapply (star2_plus2_plus2 H3 H5).
- econstructor 2.
+ eapply (star2_trans H2 H4).
+ eapply (star2_trans H3 H5).
+ eauto.
+ eauto.
+ intros. edestruct H6; eauto.
+ intros. edestruct H7; eauto.
- econstructor 3; eauto using star2_trans.
+ eapply (star2_trans H2 H5).
+ eapply (star2_trans H3 H6).
Qed.
Lemma bisim´_reduction_closed_1 {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2:S´)
: bisim´ σ1 σ2
→ star2 step σ1 nil σ1´
→ bisim´ σ1´ σ2.
Proof.
intros. eapply star2_star2n in H2. destruct H2 as [n ?].
revert σ1 σ1´ σ2 H1 H2.
pattern n.
eapply size_induction with (f:=id); intros; unfold id in *; simpl in ×.
pinversion H2; subst.
- inv H3; eauto.
eapply plus2_plus2n in H4. destruct H4. eapply plus2n_star2n in H4.
edestruct (star2n_reach H3 H4); eauto. eapply H.
+ eapply bisim´_expansion_closed. eapply H6.
eauto using star2n_star2. eauto using plus2_star2.
+ eapply H1; try eapply H9. omega.
eapply bisim´_expansion_closed. eapply H6. eapply star2_refl.
eauto using plus2_star2.
- eapply star2n_star2 in H3. eapply activated_star_reach in H3; eauto.
- pfold. eapply star2n_star2 in H3.
eapply star2_reach_normal in H3; eauto. eapply H.
Qed.
Lemma bisim´_terminate {S1} `{StateType S1} (σ1 σ1´:S1)
{S2} `{StateType S2} (σ2:S2)
: star2 step σ1 nil σ1´
→ normal2 step σ1´
→ bisim´ σ1 σ2
→ ∃ σ2´, star2 step σ2 nil σ2´ ∧ normal2 step σ2´ ∧ result σ1´ = result σ2´.
Proof.
intros. general induction H1.
- pinversion H3; subst.
+ exfalso. eapply H2. inv H1; do 2 eexists; eauto.
+ exfalso. eapply star2_normal in H1; eauto. subst.
eapply (activated_normal _ H5); eauto.
+ eapply star2_normal in H4; eauto; subst.
eexists; split; eauto.
- destruct y; isabsurd. simpl.
eapply IHstar2; eauto.
eapply bisim´_reduction_closed_1; eauto using star2.
eapply (S_star2 _ _ H); eauto using star2_refl.
Qed.
Lemma bisim´_activated {S1} `{StateType S1} (σ1:S1)
{S2} `{StateType S2} (σ2:S2)
: activated σ1
→ bisim´ σ1 σ2
→ ∃ σ2´, star2 step σ2 nil σ2´ ∧ activated σ2´ ∧
( ∀ (evt : event) (σ1´´ : S1),
step σ1 evt σ1´´ →
∃ σ2´´ : S2,
step σ2´ evt σ2´´ ∧
(paco2 (bisim_gen (S´:=S2)) bot2 σ1´´ σ2´´))
∧
( ∀ (evt : event) (σ2´´ : S2),
step σ2´ evt σ2´´ →
∃ σ1´ : S1,
step σ1 evt σ1´ ∧
(paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´´)).
Proof.
intros.
pinversion H2; subst.
- exfalso. edestruct (plus2_destr_nil H3); dcr.
destruct H1 as [? []].
exploit (step_internally_deterministic _ _ _ _ H7 H1); dcr; congruence.
- assert (σ1 = σ0). eapply activated_star_eq; eauto. subst σ1.
eexists σ3; split; eauto. split; eauto. split.
intros. edestruct H7; eauto; dcr. destruct H12; isabsurd.
eexists; split; eauto.
intros. edestruct H8; eauto; dcr. destruct H12; isabsurd.
eexists; split; eauto.
- exfalso. refine (activated_normal_star _ H1 _ _); eauto using star2.
Qed.
Lemma plus_step_activated {S1} `{StateType S1} (σ1 σ1´:S1)
{S2} `{StateType S2} (σ2a σ2´ σ2b σ4:S2)
{S3} `{StateType S3} (σ3 σ5:S3) (r : S1 → S3 → Prop)
(H6:plus2 step σ2a nil σ2´)
(H2:star2 step σ2a nil σ2b)
(H10:star2 step σ2b nil σ4)
(H11 : star2 step σ3 nil σ5)
(H4 : plus2 step σ1 nil σ1´)
(H13 : activated σ5)
(H12 : activated σ4)
(H7 : paco2 (bisim_gen (S´:=S2)) bot2 σ1´ σ2´)
(H14 : ∀ (evt : event) (σ1´ : S2),
step σ4 evt σ1´ →
∃ σ2´ : S3,
step σ5 evt σ2´ ∧
(paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
(H15 : ∀ (evt : event) (σ2´ : S3),
step σ5 evt σ2´ →
∃ σ1´ : S2,
step σ4 evt σ1´ ∧
(paco2 (bisim_gen (S´:=S3)) bot2 σ1´ σ2´ ∨ bot2 σ1´ σ2´))
(CIH : ∀ (σ1 : S1) (σ2a σ2b : S2) (σ3 : S3),
bisim´ σ1 σ2a →
star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a →
bisim´ σ2b σ3 → r σ1 σ3)
: paco2 (bisim_gen (S´:=S3)) r σ1 σ3.
Proof.
pfold.
eapply star2_trans in H10; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H6.
exploit (activated_star_reach H12 H10 H6); eauto.
eapply bisim´_sym in H7.
eapply bisim´_reduction_closed_1 in H7; eauto.
destruct (bisim´_activated H12 H7); dcr.
econstructor 2.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H3). eapply H11.
eauto. eauto.
+ intros. edestruct H16; eauto. destruct H9.
edestruct H14; eauto. dcr.
eexists; split; eauto. destruct H20; isabsurd.
right. eapply CIH. eapply bisim´_sym in H17. eauto.
left. eapply star2_refl. eauto.
+ intros. edestruct H15; eauto; dcr.
edestruct H5; eauto; dcr. destruct H9.
eexists; split; eauto. destruct H18; isabsurd.
right. eapply CIH. eapply bisim´_sym. eapply H19.
left; eapply star2_refl.
eauto.
Qed.
Lemma bisim´_zigzag {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2a σ2b:S2) {S3} `{StateType S3} (σ3:S3)
: bisim´ σ1 σ2a
→ (star2 step σ2a nil σ2b ∨ star2 step σ2b nil σ2a)
→ bisim´ σ2b σ3
→ bisim´ σ1 σ3.
Proof.
revert σ1 σ2a σ2b σ3. pcofix CIH; intros.
destruct H4.
- {
pinversion H3; pinversion H5; subst.
- pfold. eapply star2_plus2_plus2 in H10; eauto. clear H2; simpl in ×.
edestruct (plus2_reach H6 H10); eauto.
eapply H0.
-
eapply (@plus_step_activated S1 _ _ _ S2 _ _ _ _ _ S3); eauto.
-
eapply star2_trans in H11; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H6.
exploit (star2_reach_normal H11 H6); eauto. eapply H0.
edestruct (bisim´_terminate X H13 (bisim´_sym H7)); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H10. eapply H10.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8); eauto.
eauto. eauto. eauto.
-
pfold.
eapply plus2_star2 in H13.
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
exploit (activated_star_reach H8 H6 H13); eauto.
eapply bisim´_reduction_closed_1 in H15; eauto.
destruct (bisim´_activated H8 H15); dcr.
econstructor 2. eauto.
eapply plus2_star2 in H14.
eapply (star2_trans H14 H11). eauto.
eauto.
+ intros.
edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H12 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto.
left; eapply star2_refl.
-
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
exploit (both_activated H6 H13); eauto. subst.
pfold. econstructor 2; eauto; intros.
+ edestruct H9; eauto. dcr.
edestruct H17; eauto; dcr.
eexists. split; eauto.
destruct H19, H21; isabsurd.
right. eapply CIH; try eapply H11; try eapply H19.
left. eapply star2_refl.
+ edestruct H18; eauto. dcr.
edestruct H10; eauto; dcr.
eexists. split; eauto.
destruct H19, H21; isabsurd.
right. eapply CIH; try eapply H11; try eapply H19.
left. eapply star2_refl.
-
eapply star2_trans in H14; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H6); eauto.
-
eapply plus2_star2 in H12.
eapply star2_trans in H12; eauto. clear H2; simpl in ×.
exploit (star2_reach_normal H7 H12); eauto. eapply H0.
edestruct (bisim´_terminate X H9 H14); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H4. eapply H4.
eauto.
eapply plus2_star2 in H13.
eapply (star2_trans H13 H10); eauto.
eauto. eauto.
- eapply star2_trans in H12; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H12 H14 H7); eauto.
-
pfold.
eapply star2_trans in H13; eauto. clear H2; simpl in ×.
edestruct (star2_reach H7 H13); eauto. eapply H0.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H9. do 2 eexists; eauto.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H15. do 2 eexists; eauto.
}
-{
pinversion H3; pinversion H5; subst.
- pfold. eapply star2_plus2_plus2 in H6; eauto. clear H2; simpl in ×.
edestruct (plus2_reach H6 H10); eauto.
eapply H0.
-
pfold.
eapply plus2_star2 in H6.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (activated_star_reach H12 H10 H6); eauto.
eapply bisim´_sym in H7.
eapply bisim´_reduction_closed_1 in H7; eauto.
destruct (bisim´_activated H12 H7); dcr.
econstructor 2.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8). eapply H11.
eauto. eauto.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H14 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH. eapply bisim´_sym in H19; eauto.
left. eapply star2_refl. eauto.
+ intros.
edestruct H15 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H9 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH. eapply bisim´_sym in H21; eauto.
left; eapply star2_refl. eauto.
-
eapply plus2_star2 in H6.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (star2_reach_normal H11 H6); eauto. eapply H0.
edestruct (bisim´_terminate X H13 (bisim´_sym H7)); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H10. eapply H10.
eapply plus2_star2 in H4.
eapply (star2_trans H4 H8); eauto.
eauto. eauto. eauto.
-
pfold.
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H13.
exploit (activated_star_reach H8 H6 H13); eauto.
eapply bisim´_reduction_closed_1 in H15; eauto.
destruct (bisim´_activated H8 H15); dcr.
econstructor 2. eauto.
eapply plus2_star2 in H14.
eapply (star2_trans H14 H11). eauto.
eauto.
+ intros.
edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H12 as [? [? ?]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ intros.
edestruct H18 as [? [? ?]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto.
left; eapply star2_refl.
-
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exploit (both_activated H6 H13); eauto. subst.
pfold. econstructor 2; eauto; intros.
+ edestruct H9 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H17 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
+ edestruct H18 as [? [? [?|?]]]; eauto; isabsurd.
edestruct H10 as [? [? [?|?]]]; eauto; isabsurd.
eexists; split; eauto.
right. eapply CIH; eauto. left. eapply star2_refl.
-
eapply star2_trans in H6; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H6 H8 H14); eauto.
-
eapply star2_trans in H7; eauto. clear H2; simpl in ×.
eapply plus2_star2 in H12.
exploit (star2_reach_normal H7 H12); eauto. eapply H0.
edestruct (bisim´_terminate X H9 H14); eauto; dcr.
pfold.
econstructor 3. rewrite H16 in H4. eapply H4.
eauto.
eapply plus2_star2 in H13.
eapply (star2_trans H13 H10); eauto.
eauto. eauto.
- eapply star2_trans in H7; eauto. clear H2; simpl in ×.
exfalso; eapply (activated_normal_star H12 H14 H7); eauto.
-
pfold.
eapply star2_trans in H7; eauto. clear H2; simpl in ×.
edestruct (star2_reach H7 H13); eauto. eapply H0.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H9. do 2 eexists; eauto.
+ inv H2.
× econstructor 3; eauto. congruence.
× exfalso. eapply H15. do 2 eexists; eauto.
}
Qed.
Lemma bisim´_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: bisim´ σ1 σ2
→ bisim´ σ2 σ3
→ bisim´ σ1 σ3.
Proof.
intros. eauto using (bisim´_zigzag (S1:=S1) (S2:=S2) (S3:=S3)), star2_refl.
Qed.
Lemma bisim_trans {S1} `{StateType S1}
(σ1:S1) {S2} `{StateType S2} (σ2:S2) {S3} `{StateType S3} (σ3:S3)
: bisim σ1 σ2
→ bisim σ2 σ3
→ bisim σ1 σ3.
Proof.
intros. eapply bisim´_bisim.
eapply bisim_bisim´ in H2.
eapply bisim_bisim´ in H3.
eapply (bisim´_trans H2 H3).
Qed.
Lemma bisim´_reduction_closed {S} `{StateType S}
(σ1 σ1´:S) {S´} `{StateType S´} (σ2 σ2´:S´)
: bisim´ σ1 σ2
→ star2 step σ1 nil σ1´
→ star2 step σ2 nil σ2´
→ bisim´ σ1´ σ2´.
Proof.
intros. eapply bisim´_trans.
eapply bisim´_reduction_closed_1; eauto.
eapply bisim´_sym.
eapply bisim´_sym in H1.
eapply bisim´_reduction_closed_1; eauto.
eapply bisim´_refl.
Qed.
Instance bisim_progeq : ProgramEquivalence F.state F.state.
constructor. eapply (paco2 (@bisim_gen F.state _ F.state _)).
Defined.
Lemma simL_mon (r r0:rel2 F.state (fun _ : F.state ⇒ F.state)) A AR L1 L2 (AL:list A) L1´ L2´
: AIR5 (simB bisim_progeq r AR) L1 L2 AL L1´ L2´
→ (∀ x0 x1 : F.state, r x0 x1 → r0 x0 x1)
→ L1 = L1´
→ L2 = L2´
→ AIR5 (simB bisim_progeq r0 AR) L1 L2 AL L1´ L2´.
Proof.
intros. general induction H; eauto using AIR5.
econstructor; eauto.
inv pf. econstructor; eauto.
intros. eapply paco2_mon; eauto. eapply H3; eauto.
Qed.
Lemma subst_lemma A AR (a:A) AL s s´ V V´ E E´ Z Z´ L1 L2 t t´
: fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ ParamRel a Z Z´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ simL´ bisim_progeq bot2 AR AL L1 L2
→ (∀ r (L L´ : list F.block),
simL´ bisim_progeq r AR (a :: AL) L L´ →
paco2 (@bisim_gen F.state _ F.state _) r (L, V, t) (L´, V´, t´))
→ paco2 (@bisim_gen F.state _ F.state _) bot2 (F.blockI E Z s :: L1, V, t)
(F.blockI E´ Z´ s´ :: L2, V´, t´).
Proof.
revert_all; pcofix CIH; intros.
eapply H4.
econstructor. econstructor; eauto.
intros. pfold.
econstructor; try eapply plus2O.
econstructor; eauto using get; simpl.
edestruct RelsOK; eauto.
eapply omap_length in H. congruence. reflexivity.
econstructor; eauto using get; simpl. edestruct RelsOK; eauto.
eapply omap_length in H5. congruence. reflexivity.
simpl.
right. eapply CIH; eauto.
intros. eapply H0; eauto.
eapply simL_mon; eauto. intros; isabsurd.
Qed.
Lemma fix_compatible r A AR (a:A) AL s s´ E E´ Z Z´ L L´ Yv Y´v
: simL´ bisim_progeq r AR AL L L´
→ fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ ParamRel a Z Z´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ ArgRel E E´ a Yv Y´v
→ bisim´r r
(F.blockI E Z s :: L, E [Z <-- List.map Some Yv], s)
(F.blockI E´ Z´ s´ :: L´, E´ [Z´ <-- List.map Some Y´v], s´).
Proof.
revert_all; pcofix CIH; intros.
eapply H1; eauto.
hnf; intros. econstructor; eauto. econstructor; eauto; intros.
pfold. econstructor; try eapply plus2O.
- econstructor; eauto using get.
+ simpl. edestruct RelsOK; eauto.
exploit omap_length; try eapply H; eauto.
congruence.
- reflexivity.
- econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H6; eauto.
congruence.
- reflexivity.
- simpl. right. eapply CIH; eauto.
- eapply simL_mon; eauto.
Qed.
Lemma simL_extension´ r A AR (a:A) AL s s´ E E´ Z Z´ L L´
: simL´ bisim_progeq r AR AL L L´
→ fexteq´ bisim_progeq AR a (a::AL) E Z s E´ Z´ s´
→ BlockRel a (F.blockI E Z s) (F.blockI E´ Z´ s´)
→ simL´ bisim_progeq r AR (a::AL) (F.blockI E Z s :: L) (F.blockI E´ Z´ s´ :: L´).
Proof.
intros. destruct H0.
hnf; intros. econstructor; eauto. econstructor; eauto; intros.
+ pfold. econstructor; try eapply plus2O.
econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H3; eauto.
congruence. reflexivity.
econstructor; eauto using get. simpl.
edestruct RelsOK; eauto. exploit omap_length; try eapply H4; eauto.
congruence. reflexivity.
simpl. left.
eapply fix_compatible; eauto. split; eauto.
Qed.
Lemma get_drop_lab0 (L:F.labenv) l blk
: get L (counted l) blk
→ get (drop (labN l) L) (counted (LabI 0)) blk.
Proof.
intros. eapply drop_get; simpl. orewrite (labN l + 0 = labN l); eauto.
Qed.
Lemma drop_get_lab0 (L:F.labenv) l blk
: get (drop (labN l) L) (counted (LabI 0)) blk
→ get L (counted l) blk.
Proof.
intros. eapply get_drop in H; simpl in ×. orewrite (labN l + 0 = labN l) in H; eauto.
Qed.
Lemma bisim_drop_shift r l L E Y L´ E´ Y´
: paco2 (@bisim_gen F.state _ F.state _) r (drop (labN l) L, E, stmtApp (LabI 0) Y)
(drop (labN l) L´, E´, stmtApp (LabI 0) Y´)
→ paco2 (@bisim_gen F.state _ F.state _) r (L, E, stmtApp l Y)
(L´, E´, stmtApp l Y´).
Proof.
intros. pinversion H; subst.
- eapply plus2_destr_nil in H0.
eapply plus2_destr_nil in H1.
destruct H0; destruct H1; dcr. inv H3.
simpl in ×. inv H1; simpl in ×.
pfold. econstructor; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
eauto.
- inv H0.
+ exfalso. destruct H2 as [? [? ?]]. inv H2.
+ inv H1.
× exfalso. destruct H3 as [? [? ?]]. inv H3.
× inv H7; inv H10; simpl in ×.
pfold. subst yl yl0.
econstructor; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H9.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H12.
left. pfold. econstructor 2; try eapply star2_refl; eauto.
- inv H1; inv H2; simpl in ×.
+ pfold. econstructor 3; try eapply star2_refl. reflexivity.
× stuck2. eapply H3. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
× stuck2. eapply H4. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
+ inv H6.
pfold. econstructor 3; [
| eapply star2_refl
|
|
|].
Focus 2. rewrite <- H5. eapply S_star2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
simpl; eauto.
stuck2. eapply H3. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
+ inv H6.
pfold. econstructor 3; [
|
|eapply star2_refl
|
|].
Focus 2. rewrite <- H5. eapply S_star2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eauto.
simpl; eauto. eauto.
stuck2. eapply H4. do 2 eexists.
econstructor; eauto using get_drop_lab0, drop_get_lab0.
+ inv H6; inv H9. pfold. simpl in ×. subst yl yl0.
econstructor 1; try eapply star2_plus2.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H8.
econstructor; eauto using get_drop_lab0, drop_get_lab0. eapply H11.
left. pfold. econstructor 3; try eapply star2_refl; eauto.
Qed.
Ltac single_step :=
match goal with
| [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = true |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
econstructor; eauto; rewrite <- H; eauto; cset_tac; intuition
| [ H : agree_on _ ?E ?E´, I : val2bool (?E ?x) = false |- step (_, ?E´, stmtIf ?x _ _) _ ] ⇒
econstructor 3; eauto; rewrite <- H; eauto; cset_tac; intuition
| [ H : val2bool _ = false |- _ ] ⇒ econstructor 3 ; try eassumption; try reflexivity
| [ H : step (?L, _ , stmtApp ?l _) _, H´: get ?L (counted ?l) _ |- _] ⇒
econstructor; try eapply H´; eauto
| [ H´: get ?L (counted ?l) _ |- step (?L, _ , stmtApp ?l _) _] ⇒
econstructor; try eapply H´; eauto
| _ ⇒ econstructor; eauto
end.
Ltac one_step := eapply bisimSilent; [ eapply plus2O; single_step
| eapply plus2O; single_step
| ].
Ltac no_step := eapply bisimTerm;
try eapply star2_refl; try get_functional; try subst;
[ try reflexivity
| stuck2
| stuck2 ].
Ltac step_activated :=
match goal with
| [ H : omap (exp_eval ?E) ?Y = Some ?vl
|- activated (_, ?E, stmtExtern ?x ?f ?Y ?s) ] ⇒
eexists (ExternI f vl 0); eexists; try (now (econstructor; eauto))
end.
Ltac extern_step :=
let STEP := fresh "STEP" in
eapply bisimExtern;
[ eapply star2_refl
| eapply star2_refl
| try step_activated
| try step_activated
| intros ? ? STEP; inv STEP
| intros ? ? STEP; inv STEP
].
Definition same_call (e e´:extern) := extern_fnc e = extern_fnc e´ ∧ extern_args e = extern_args e´.
Definition receptive S `{StateType S} :=
∀ σ σ´ ext, step σ (EvtExtern ext) σ´
→ ∀ ext´, same_call ext ext´ → ∃ σ´´, step σ (EvtExtern ext´) σ´´.
Arguments receptive S [H].
Definition determinate S `{StateType S} :=
∀ σ σ´ σ´´ ext ext´, step σ (EvtExtern ext) σ´
→ step σ (EvtExtern ext´) σ´´ → same_call ext ext´.
Arguments determinate S [H].
Lemma bisimExternDet {S} `{StateType S} {S´} `{StateType S´} (pσ1:S) (pσ2:S´) (σ1:S) (σ2:S´)
(RCPT:receptive S) (DET:determinate S´)
: star2 step pσ1 nil σ1
→ star2 step pσ2 nil σ2
→ activated σ1
→ (∀ evt σ1´, step σ1 evt σ1´ → ∃ σ2´, step σ2 evt σ2´ ∧ bisim σ1´ σ2´)
→ bisim pσ1 pσ2.
Proof.
intros.
econstructor 2; eauto.
- inv H3. dcr. edestruct H4; eauto. firstorder.
- intros. inv H3. dcr. exploit H4; eauto; dcr.
destruct evt.
+ exploit DET. eauto. eapply H5.
exploit RCPT; eauto. dcr.
exploit H4. eapply H6. dcr.
eexists; split. eapply H6.
exploit step_externally_determined. eapply H11. eapply H5. subst. eauto.
+ exfalso. exploit step_internally_deterministic; eauto; dcr. congruence.
Qed.