Library Nom_Bisimulation
Require Export TLC.LibRelation.
Require Export Nom_Semantics.
Notation Rincl := LibRelation.rel_incl.
Definition comp_rel {A:Type} (R S :binary A) x y := ∃ z, R x z ∧ S z y.
Notation "R ° S" := (@comp_rel _ R S) (at level 42, right associativity).
Lemma comp_trans{A}: ∀ (R S:binary A),
inverse (R°S) = (inverse S ° inverse R).
Proof.
intros. apply binary_ext.
split; intros H; destruct H as [ z [ H1 H2 ]]; eexists; eauto.
Qed.
Lemma comp_assoc {A} : ∀ (R S T:binary A),
R ° S ° T = (R ° S) ° T.
Proof.
intros. apply binary_ext. intros.
split; introv H; inverts H as [H1 H2].
inverts H2; repeat (eexists; intuition eauto).
inverts H1; repeat (eexists; intuition eauto).
Qed.
Ltac destruct_hyps :=
repeat match goal with H: ?T |- _ ⇒
match T with
| _ ∧ _ ⇒ destruct H
| ∃ a, _ ⇒ destruct H
end
end.
Ltac destruct_comp :=
repeat match goal with
| H: (_ ° _) _ _ |- _ ⇒ unfold comp_rel in H; destruct_hyps
end.
Inductive sim_test : binary proc0 → agent → agent → Prop :=
| st_proc : ∀ (Rel:binary proc0) P Q,
Rel P Q → sim_test Rel (ag_proc P) (ag_proc Q)
| st_abs : ∀ (Rel:binary proc0) F F', (∀ (C:conc), conc_wf C →
Rel (appr F C) (appr F' C)) → sim_test Rel (ag_abs F) (ag_abs F')
| st_conc : ∀ (Rel:binary proc0) C C', (∀ (F:abs),
Rel (appr F C) (appr F C')) → sim_test Rel (ag_conc C) (ag_conc C').
Hint Constructors sim_test:bisim.
Definition simulation_late (Rel: binary proc0) : Prop := ∀ P Q, Rel P Q →
∀ l A, lts P l A → ∃ A', lts Q l A' ∧ sim_test Rel A A'.
Ltac destruct_agent_sim A :=
destructA A;simpl;
[ apply st_proc | apply st_abs; intros []; intros
| apply st_conc; intros ].
Hint Unfold simulation_late comp_rel:bisim.
Lemma sim_test_trans : ∀ Rel, trans Rel → trans (sim_test Rel).
Proof.
intros_all. destruct x; destruct y;
inverts H0; destruct z; inverts H1; subst; eauto with bisim.
Qed.
Lemma sim_test_sym : ∀ Rel, sym Rel → sym (sim_test Rel).
Proof.
intros_all.
destruct x; destruct y; inverts H0; subst; auto with bisim.
Qed.
Notation test_proc Rel P Q :=
(∀ P', lts P tau (ag_proc P') →
∃ Q', lts Q tau (ag_proc Q') ∧ Rel P' Q').
Notation test_abs Rel P Q :=
(∀ a (F:abs), lts P (inp a) (ag_abs F) → ∀ (C:conc), conc_wf C →
∃ (F':abs), lts Q (inp a) (ag_abs F') ∧ Rel (appr F C) (appr F' C)).
Notation test_conc Rel P Q :=
(∀ a (C:conc), lts P (out a) (ag_conc C) → ∀ (F:abs),
∃ (C':conc), lts Q (out a) (ag_conc C') ∧ Rel (appr F C) (appr F C')).
Definition simulation (Rel: binary proc0) : Prop := ∀ P Q, Rel P Q →
test_proc Rel P Q ∧ test_abs Rel P Q ∧ test_conc Rel P Q.
Definition bisimulation (Rel : binary proc0) : Prop :=
(simulation Rel) ∧ (simulation (inverse Rel)).
Ltac forwards_test Rel := try (match goal with
| H1: simulation Rel, H2: Rel ?P ?Q |- _ ⇒ specialize (H1 P Q H2)
end); intuition auto;
match goal with
| H1: test_proc Rel ?P ?Q, H2: lts ?P tau _ |- _ ⇒
let H' := fresh "H" in
let Q' := fresh "Q'" in forwards H': H1 H2; destruct H' as [Q' []]
| H1: test_abs Rel ?P ?Q, H2: lts ?P (inp _) ?F, H3: conc_wf ?C |- _ ⇒
let H' := fresh "H" in
let F' := fresh "F'" in forwards× H': H1 H2 C; destruct H' as [F' []]
| H1: test_conc Rel ?P ?Q, H2: lts ?P (out _) ?C, F : abs |- _ ⇒
let H' := fresh "H" in
let F' := fresh "C'" in forwards× H': H1 H2 F; destruct H' as [F' []]
end.
Lemma transp_bisim_is_bisim: ∀ Rel,
bisimulation (inverse Rel) ↔ bisimulation Rel.
Proof.
unfold bisimulation; intuition.
Qed.
Lemma sim_sym_imply_bisim : ∀ Rel,
simulation Rel → sym Rel → bisimulation Rel.
Proof.
intros Rel Hsim Hsym.
split; intuition.
rewrite inverse_sym; auto.
Qed.
Lemma comp_sim_is_sim : ∀ R S,
simulation R → simulation S → simulation (R°S).
Proof.
intros_all. inverts H1. inverts H2. specialize (H P x H1).
forwards_test R; forwards_test S; eexists; split;
try solve [eassumption]; unfold comp_rel; eexists; split; eassumption.
Qed.
Lemma sim_tclosure : ∀ Rel, simulation Rel → simulation (tclosure Rel).
Proof. intros. unfold simulation. apply tclosure_ind_l.
- intros. splits; intros_all; forwards_test Rel;
eexists; intuition; try solve [eassumption]; constructor; auto.
- intros. destruct_hyps. splits;
intros_all; forwards_test Rel; forwards_test (tclosure Rel);
eexists; split; try solve [eassumption]; econstructor 2;
try solve [constructor; eauto]; auto.
Qed.
Lemma comp_bisim_is_bisim : ∀ R S,
bisimulation R → bisimulation S → bisimulation (R°S).
Proof.
unfold bisimulation. intros; split; intuition auto using comp_sim_is_sim.
rewrite @comp_trans. auto using comp_sim_is_sim.
Qed.
Lemma union_sim_is_sim : ∀ Rel Rel', simulation Rel → simulation Rel'
→ simulation (LibRelation.union Rel Rel').
Proof.
intros_all. destruct H1; splits; intros_all;
try forwards_test Rel; try forwards_test Rel'; eexists; split;
try solve [eassumption]; try solve [left*]; right×.
Qed.
Lemma late_implies_sim : ∀ Rel, simulation_late Rel → simulation Rel.
Proof.
unfold simulation. intros. splits; intros.
- forwards*: H H1. destruct H2 as [A' [ ]]. forwards*: lts_tau_proc H2.
destruct H4. inverts H4. ∃ x; intuition. inverts× H3.
- forwards*: H H1. destruct H3 as [A' [ ]]. forwards*: lts_inp_abs H3.
destruct H5. inverts H5. ∃ x; intuition. inverts H4. forwards*: H8 C.
- forwards*: H H1. destruct H2 as [A' [ ]]. forwards*: lts_out_conc H2.
destruct H4. inverts H4. ∃ x; intuition.
destruct C as []; destruct x as []; inverts H3. forwards*: H7 F.
Qed.
Definition bisimilarity (P Q:proc0) := ∃ Rel, bisimulation Rel ∧ Rel P Q.
Lemma bisim_sym: sym bisimilarity.
Proof.
intros_all. destruct H as [ Rel ]. ∃ (inverse Rel); intuition.
apply transp_bisim_is_bisim; auto.
Qed.
Lemma bisim_trans: trans bisimilarity.
Proof.
intros_all. inversion H as [ Rel ]. inversion H0 as [ Rel' ].
∃ (Rel ° Rel'). intuition. apply comp_bisim_is_bisim; auto.
∃ y; auto.
Qed.
Hint Unfold bisimulation bisimilarity:bisim.
Definition mod_aeq {V} (Rel : binary (proc V)) := ∀ (P P' Q Q': proc V),
Rel P Q → P=A=P' → Q=A=Q' → Rel P' Q'.
Lemma bisim_refl: refl bisimilarity.
Proof.
intros P. ∃ (@eq proc0). intuition. apply sim_sym_imply_bisim.
- split; [|split]; rewrite H; intros_all; eexists; intuition; auto.
- intros_all. auto.
Qed.
Lemma bisim_is_bisimulation : bisimulation bisimilarity.
Proof.
apply sim_sym_imply_bisim.
+ unfold simulation. intros. inverts H. destruct H0. assert (Hbisim:=H).
destruct H as [Hr Hrconv].
forwards_test x; eexists; intuition; try eassumption; ∃ x; intuition.
+ apply bisim_sym.
Qed.
Lemma aeq_bisimulation : bisimulation aeq.
Proof.
apply sim_sym_imply_bisim.
+ unfold simulation. intros. splits;
intros; forwards: aeq_lts_2 H H0; destruct_hyps.
- inversion H1; subst. ∃ Q0. intuition.
- inversion H2. subst. ∃ Q0. intuition. rewrite H5. reflexivity.
- inversion H1. subst. ∃ C'. intuition. rewrite H4. reflexivity.
+ unfold sym. intros. rewrite H. reflexivity.
Qed.
Lemma bisim_exists_sym_rel_mod_aeq : ∀ P Q, bisimilarity P Q →
∃ Rel, sym Rel ∧ mod_aeq Rel ∧ simulation Rel ∧ Rel P Q.
Proof.
intros.
destruct H as [Rel [Hbis Hpq]].
∃ (tclosure (LibRelation.union (LibRelation.union Rel (inverse Rel)) aeq )).
destruct Hbis as [ Hsim Hsimsym ].
splits.
- apply sym_tclosure. intros_all. destruct H. destruct H.
+ left. right. auto.
+ left. left. auto.
+ right. symmetry; auto.
- intros_all. eapply trans_tclosure. eapply trans_tclosure.
+ constructor. right. symmetry. eauto.
+ apply H.
+ constructor. right. auto.
- apply sim_tclosure. apply union_sim_is_sim. apply union_sim_is_sim; auto.
apply aeq_bisimulation.
- constructor. left. left. auto.
Qed.
Lemma bisim_aeq : mod_aeq bisimilarity.
Proof. intros_all. apply bisim_exists_sym_rel_mod_aeq in H. destruct_hyps.
∃ x. split.
+ apply sim_sym_imply_bisim; auto.
+ eapply H2; eauto.
Qed.
Definition mod_swap {V} (Rel : binary (proc V)) := ∀ (P Q: proc V) b c,
Rel P Q → Rel (swap b c P) (swap b c Q).
Lemma bisim_swap : mod_swap bisimilarity.
Proof. unfold mod_swap. intros. forwards: bisim_exists_sym_rel_mod_aeq H.
destruct H0 as [Rel]. clear H. destruct_hyps. ∃ (fun x y ⇒
Rel (swap b c x) (swap b c y)). split. 2:simpl_swap. clears P Q.
apply sim_sym_imply_bisim. 2: intros_all; auto. clear H.
intros_all. splits; intros;
forwards: swap_lts b c H2; destruct_hyps; unfold swap_lab in ×.
- inversion H3; subst. forwards_test Rel. forwards: swap_lts b c H6.
simpl_swap in H10. destruct_hyps. unfold swap_lab in ×. inversion H10; subst.
∃ P1. intuition. eapply H0. apply H9. auto. rewrite H14; simpl_swap.
- inversion H4; subst. apply (swap_conc_wf b c) in H3.
forwards_test Rel. forwards: swap_lts b c H7. simpl_swap in H11. destruct_hyps.
unfold swap_lab in ×. rewrite swap_aux_invo in H12.
inversion H11; subst. ∃ P1. intuition. applys (>>H0 H10);
rewrite swap_appr; try rewrite H8; try rewrite H15; simpl_swap.
- inversion H3; subst. clear H3.
specialize (H1 (swap b c P) (swap b c Q) H). destruct_hyps.
forwards: H5 H4 (swap b c F). destruct H6 as [C'0]. destruct_hyps.
forwards: swap_lts b c H6. unfold swap_lab in ×. simpl_swap in H9.
destruct_hyps. inversion H9; subst. clear H9. ∃ C1. intuition.
applys (>>H0 H8); rewrite swap_appr; try rewrite H7;
try rewrite H13; simpl_swap.
Qed.
Definition open_extension {V:Set} (Rel:binary proc0) (P Q:proc V) :=
∀ (f: V→ proc0) N, fn P [<=] N → fn Q [<=] N →
(∀ x, fn (f x) [<=] N) → Rel (bind f N P) (bind f N Q).
Lemma oe_refl {V:Set} : ∀ Rel, refl Rel → refl (@open_extension V Rel).
Proof. intros_all. apply H. Qed.
Lemma oe_sym {V:Set} : ∀ Rel, sym Rel → sym (@open_extension V Rel).
Proof. intros_all. apply H; auto. Qed.
Lemma oe_trans {V:Set} : ∀ Rel,
mod_aeq Rel → trans Rel → trans (@open_extension V Rel).
Proof. intros_all.
assert (Rel (bind f (union N (fn y)) x) (bind f (union N (fn y)) z)).
eapply H0; [ apply H1; intros; try rewrite H5; fsetdec |].
apply H2; intros; try rewrite H5; fsetdec.
eapply H; eauto; apply aeq_bind_2; intros; try rewrite H5; fsetdec.
Qed.
Lemma oe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
mod_aeq Rel → open_extension Rel P Q →
open_extension Rel (mapV f P)(mapV f Q).
Proof.
intros_all. simpl_swap in H1; simpl_swap in H2.
repeat rewrite bind_mapV_comp; auto.
Qed.
Lemma oe_bind {V W:Set}: ∀ Rel (P Q:proc V) (f:V→ proc W) N,
fn P [<=] N → fn Q [<=] N → (∀ x, fn (f x) [<=] N) →
mod_aeq Rel → open_extension Rel P Q →
open_extension Rel (bind f N P)(bind f N Q).
Proof. intros_all. eapply H2. revgoals. shelve.
rewrites (>> aeq_bind_2 N0 (union N0 N));
intros; try rewrite H6; try fsetdec;
rewrites (>> aeq_bind_3 (bind f (union N0 N) P));
[ rewrite fn_bind; intros; try rewrite H1; fsetdec
| apply aeq_bind_2; intros; try rewrite H1; fsetdec
| rewrite bind_bind; try reflexivity;
intros; try rewrite H1; try rewrite H6; fsetdec ].
rewrites (>> aeq_bind_2 N0 (union N0 N));
intros; try rewrite H6; try fsetdec;
rewrites (>> aeq_bind_3 (bind f (union N0 N) Q));
[ rewrite fn_bind; intros; try rewrite H1; fsetdec
| apply aeq_bind_2; intros; try rewrite H1; fsetdec
| rewrite bind_bind; try reflexivity;
intros; try rewrite H1; try rewrite H6; fsetdec ].
Unshelve. apply H3. fsetdec. fsetdec. intro. apply fn_bind.
rewrite H1; fsetdec. intro; rewrite H6; fsetdec.
Qed.
Lemma oe_proc0 : ∀ (Rel:binary proc0) (P Q:proc0),
mod_aeq Rel → Rel P Q → open_extension Rel P Q.
Proof.
intros_all; eapply H; try apply H0; symmetry;
apply bind_return; auto; intro; inversion x.
Qed.
Lemma oe_swap {V:Set}: ∀ Rel (P Q:proc V) b c,
mod_aeq Rel → open_extension Rel P Q →
mod_swap Rel → open_extension Rel (swap b c P) (swap b c Q).
Proof. intros_all. rewrite <- (swap_invo _ b c). rewrite <- (swap_invo _ b c) at 1.
simpl_swap in H3 H2. eapply H. 2-3: rewrite swap_bind; simpl_swap.
apply H1. apply H0; try intro; simpl_swap.
Qed.
Lemma mod_aeq_oe {V:Set} : ∀ Rel, mod_aeq Rel →
mod_aeq (@open_extension V Rel).
Proof. intros_all. eapply H. apply H0. rewrite H1; eauto. rewrite H2; auto.
eauto. apply aeq_bind_3; auto. apply aeq_bind_3; auto.
Qed.
Require Export Nom_Semantics.
Notation Rincl := LibRelation.rel_incl.
Definition comp_rel {A:Type} (R S :binary A) x y := ∃ z, R x z ∧ S z y.
Notation "R ° S" := (@comp_rel _ R S) (at level 42, right associativity).
Lemma comp_trans{A}: ∀ (R S:binary A),
inverse (R°S) = (inverse S ° inverse R).
Proof.
intros. apply binary_ext.
split; intros H; destruct H as [ z [ H1 H2 ]]; eexists; eauto.
Qed.
Lemma comp_assoc {A} : ∀ (R S T:binary A),
R ° S ° T = (R ° S) ° T.
Proof.
intros. apply binary_ext. intros.
split; introv H; inverts H as [H1 H2].
inverts H2; repeat (eexists; intuition eauto).
inverts H1; repeat (eexists; intuition eauto).
Qed.
Ltac destruct_hyps :=
repeat match goal with H: ?T |- _ ⇒
match T with
| _ ∧ _ ⇒ destruct H
| ∃ a, _ ⇒ destruct H
end
end.
Ltac destruct_comp :=
repeat match goal with
| H: (_ ° _) _ _ |- _ ⇒ unfold comp_rel in H; destruct_hyps
end.
Inductive sim_test : binary proc0 → agent → agent → Prop :=
| st_proc : ∀ (Rel:binary proc0) P Q,
Rel P Q → sim_test Rel (ag_proc P) (ag_proc Q)
| st_abs : ∀ (Rel:binary proc0) F F', (∀ (C:conc), conc_wf C →
Rel (appr F C) (appr F' C)) → sim_test Rel (ag_abs F) (ag_abs F')
| st_conc : ∀ (Rel:binary proc0) C C', (∀ (F:abs),
Rel (appr F C) (appr F C')) → sim_test Rel (ag_conc C) (ag_conc C').
Hint Constructors sim_test:bisim.
Definition simulation_late (Rel: binary proc0) : Prop := ∀ P Q, Rel P Q →
∀ l A, lts P l A → ∃ A', lts Q l A' ∧ sim_test Rel A A'.
Ltac destruct_agent_sim A :=
destructA A;simpl;
[ apply st_proc | apply st_abs; intros []; intros
| apply st_conc; intros ].
Hint Unfold simulation_late comp_rel:bisim.
Lemma sim_test_trans : ∀ Rel, trans Rel → trans (sim_test Rel).
Proof.
intros_all. destruct x; destruct y;
inverts H0; destruct z; inverts H1; subst; eauto with bisim.
Qed.
Lemma sim_test_sym : ∀ Rel, sym Rel → sym (sim_test Rel).
Proof.
intros_all.
destruct x; destruct y; inverts H0; subst; auto with bisim.
Qed.
Notation test_proc Rel P Q :=
(∀ P', lts P tau (ag_proc P') →
∃ Q', lts Q tau (ag_proc Q') ∧ Rel P' Q').
Notation test_abs Rel P Q :=
(∀ a (F:abs), lts P (inp a) (ag_abs F) → ∀ (C:conc), conc_wf C →
∃ (F':abs), lts Q (inp a) (ag_abs F') ∧ Rel (appr F C) (appr F' C)).
Notation test_conc Rel P Q :=
(∀ a (C:conc), lts P (out a) (ag_conc C) → ∀ (F:abs),
∃ (C':conc), lts Q (out a) (ag_conc C') ∧ Rel (appr F C) (appr F C')).
Definition simulation (Rel: binary proc0) : Prop := ∀ P Q, Rel P Q →
test_proc Rel P Q ∧ test_abs Rel P Q ∧ test_conc Rel P Q.
Definition bisimulation (Rel : binary proc0) : Prop :=
(simulation Rel) ∧ (simulation (inverse Rel)).
Ltac forwards_test Rel := try (match goal with
| H1: simulation Rel, H2: Rel ?P ?Q |- _ ⇒ specialize (H1 P Q H2)
end); intuition auto;
match goal with
| H1: test_proc Rel ?P ?Q, H2: lts ?P tau _ |- _ ⇒
let H' := fresh "H" in
let Q' := fresh "Q'" in forwards H': H1 H2; destruct H' as [Q' []]
| H1: test_abs Rel ?P ?Q, H2: lts ?P (inp _) ?F, H3: conc_wf ?C |- _ ⇒
let H' := fresh "H" in
let F' := fresh "F'" in forwards× H': H1 H2 C; destruct H' as [F' []]
| H1: test_conc Rel ?P ?Q, H2: lts ?P (out _) ?C, F : abs |- _ ⇒
let H' := fresh "H" in
let F' := fresh "C'" in forwards× H': H1 H2 F; destruct H' as [F' []]
end.
Lemma transp_bisim_is_bisim: ∀ Rel,
bisimulation (inverse Rel) ↔ bisimulation Rel.
Proof.
unfold bisimulation; intuition.
Qed.
Lemma sim_sym_imply_bisim : ∀ Rel,
simulation Rel → sym Rel → bisimulation Rel.
Proof.
intros Rel Hsim Hsym.
split; intuition.
rewrite inverse_sym; auto.
Qed.
Lemma comp_sim_is_sim : ∀ R S,
simulation R → simulation S → simulation (R°S).
Proof.
intros_all. inverts H1. inverts H2. specialize (H P x H1).
forwards_test R; forwards_test S; eexists; split;
try solve [eassumption]; unfold comp_rel; eexists; split; eassumption.
Qed.
Lemma sim_tclosure : ∀ Rel, simulation Rel → simulation (tclosure Rel).
Proof. intros. unfold simulation. apply tclosure_ind_l.
- intros. splits; intros_all; forwards_test Rel;
eexists; intuition; try solve [eassumption]; constructor; auto.
- intros. destruct_hyps. splits;
intros_all; forwards_test Rel; forwards_test (tclosure Rel);
eexists; split; try solve [eassumption]; econstructor 2;
try solve [constructor; eauto]; auto.
Qed.
Lemma comp_bisim_is_bisim : ∀ R S,
bisimulation R → bisimulation S → bisimulation (R°S).
Proof.
unfold bisimulation. intros; split; intuition auto using comp_sim_is_sim.
rewrite @comp_trans. auto using comp_sim_is_sim.
Qed.
Lemma union_sim_is_sim : ∀ Rel Rel', simulation Rel → simulation Rel'
→ simulation (LibRelation.union Rel Rel').
Proof.
intros_all. destruct H1; splits; intros_all;
try forwards_test Rel; try forwards_test Rel'; eexists; split;
try solve [eassumption]; try solve [left*]; right×.
Qed.
Lemma late_implies_sim : ∀ Rel, simulation_late Rel → simulation Rel.
Proof.
unfold simulation. intros. splits; intros.
- forwards*: H H1. destruct H2 as [A' [ ]]. forwards*: lts_tau_proc H2.
destruct H4. inverts H4. ∃ x; intuition. inverts× H3.
- forwards*: H H1. destruct H3 as [A' [ ]]. forwards*: lts_inp_abs H3.
destruct H5. inverts H5. ∃ x; intuition. inverts H4. forwards*: H8 C.
- forwards*: H H1. destruct H2 as [A' [ ]]. forwards*: lts_out_conc H2.
destruct H4. inverts H4. ∃ x; intuition.
destruct C as []; destruct x as []; inverts H3. forwards*: H7 F.
Qed.
Definition bisimilarity (P Q:proc0) := ∃ Rel, bisimulation Rel ∧ Rel P Q.
Lemma bisim_sym: sym bisimilarity.
Proof.
intros_all. destruct H as [ Rel ]. ∃ (inverse Rel); intuition.
apply transp_bisim_is_bisim; auto.
Qed.
Lemma bisim_trans: trans bisimilarity.
Proof.
intros_all. inversion H as [ Rel ]. inversion H0 as [ Rel' ].
∃ (Rel ° Rel'). intuition. apply comp_bisim_is_bisim; auto.
∃ y; auto.
Qed.
Hint Unfold bisimulation bisimilarity:bisim.
Definition mod_aeq {V} (Rel : binary (proc V)) := ∀ (P P' Q Q': proc V),
Rel P Q → P=A=P' → Q=A=Q' → Rel P' Q'.
Lemma bisim_refl: refl bisimilarity.
Proof.
intros P. ∃ (@eq proc0). intuition. apply sim_sym_imply_bisim.
- split; [|split]; rewrite H; intros_all; eexists; intuition; auto.
- intros_all. auto.
Qed.
Lemma bisim_is_bisimulation : bisimulation bisimilarity.
Proof.
apply sim_sym_imply_bisim.
+ unfold simulation. intros. inverts H. destruct H0. assert (Hbisim:=H).
destruct H as [Hr Hrconv].
forwards_test x; eexists; intuition; try eassumption; ∃ x; intuition.
+ apply bisim_sym.
Qed.
Lemma aeq_bisimulation : bisimulation aeq.
Proof.
apply sim_sym_imply_bisim.
+ unfold simulation. intros. splits;
intros; forwards: aeq_lts_2 H H0; destruct_hyps.
- inversion H1; subst. ∃ Q0. intuition.
- inversion H2. subst. ∃ Q0. intuition. rewrite H5. reflexivity.
- inversion H1. subst. ∃ C'. intuition. rewrite H4. reflexivity.
+ unfold sym. intros. rewrite H. reflexivity.
Qed.
Lemma bisim_exists_sym_rel_mod_aeq : ∀ P Q, bisimilarity P Q →
∃ Rel, sym Rel ∧ mod_aeq Rel ∧ simulation Rel ∧ Rel P Q.
Proof.
intros.
destruct H as [Rel [Hbis Hpq]].
∃ (tclosure (LibRelation.union (LibRelation.union Rel (inverse Rel)) aeq )).
destruct Hbis as [ Hsim Hsimsym ].
splits.
- apply sym_tclosure. intros_all. destruct H. destruct H.
+ left. right. auto.
+ left. left. auto.
+ right. symmetry; auto.
- intros_all. eapply trans_tclosure. eapply trans_tclosure.
+ constructor. right. symmetry. eauto.
+ apply H.
+ constructor. right. auto.
- apply sim_tclosure. apply union_sim_is_sim. apply union_sim_is_sim; auto.
apply aeq_bisimulation.
- constructor. left. left. auto.
Qed.
Lemma bisim_aeq : mod_aeq bisimilarity.
Proof. intros_all. apply bisim_exists_sym_rel_mod_aeq in H. destruct_hyps.
∃ x. split.
+ apply sim_sym_imply_bisim; auto.
+ eapply H2; eauto.
Qed.
Definition mod_swap {V} (Rel : binary (proc V)) := ∀ (P Q: proc V) b c,
Rel P Q → Rel (swap b c P) (swap b c Q).
Lemma bisim_swap : mod_swap bisimilarity.
Proof. unfold mod_swap. intros. forwards: bisim_exists_sym_rel_mod_aeq H.
destruct H0 as [Rel]. clear H. destruct_hyps. ∃ (fun x y ⇒
Rel (swap b c x) (swap b c y)). split. 2:simpl_swap. clears P Q.
apply sim_sym_imply_bisim. 2: intros_all; auto. clear H.
intros_all. splits; intros;
forwards: swap_lts b c H2; destruct_hyps; unfold swap_lab in ×.
- inversion H3; subst. forwards_test Rel. forwards: swap_lts b c H6.
simpl_swap in H10. destruct_hyps. unfold swap_lab in ×. inversion H10; subst.
∃ P1. intuition. eapply H0. apply H9. auto. rewrite H14; simpl_swap.
- inversion H4; subst. apply (swap_conc_wf b c) in H3.
forwards_test Rel. forwards: swap_lts b c H7. simpl_swap in H11. destruct_hyps.
unfold swap_lab in ×. rewrite swap_aux_invo in H12.
inversion H11; subst. ∃ P1. intuition. applys (>>H0 H10);
rewrite swap_appr; try rewrite H8; try rewrite H15; simpl_swap.
- inversion H3; subst. clear H3.
specialize (H1 (swap b c P) (swap b c Q) H). destruct_hyps.
forwards: H5 H4 (swap b c F). destruct H6 as [C'0]. destruct_hyps.
forwards: swap_lts b c H6. unfold swap_lab in ×. simpl_swap in H9.
destruct_hyps. inversion H9; subst. clear H9. ∃ C1. intuition.
applys (>>H0 H8); rewrite swap_appr; try rewrite H7;
try rewrite H13; simpl_swap.
Qed.
Definition open_extension {V:Set} (Rel:binary proc0) (P Q:proc V) :=
∀ (f: V→ proc0) N, fn P [<=] N → fn Q [<=] N →
(∀ x, fn (f x) [<=] N) → Rel (bind f N P) (bind f N Q).
Lemma oe_refl {V:Set} : ∀ Rel, refl Rel → refl (@open_extension V Rel).
Proof. intros_all. apply H. Qed.
Lemma oe_sym {V:Set} : ∀ Rel, sym Rel → sym (@open_extension V Rel).
Proof. intros_all. apply H; auto. Qed.
Lemma oe_trans {V:Set} : ∀ Rel,
mod_aeq Rel → trans Rel → trans (@open_extension V Rel).
Proof. intros_all.
assert (Rel (bind f (union N (fn y)) x) (bind f (union N (fn y)) z)).
eapply H0; [ apply H1; intros; try rewrite H5; fsetdec |].
apply H2; intros; try rewrite H5; fsetdec.
eapply H; eauto; apply aeq_bind_2; intros; try rewrite H5; fsetdec.
Qed.
Lemma oe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
mod_aeq Rel → open_extension Rel P Q →
open_extension Rel (mapV f P)(mapV f Q).
Proof.
intros_all. simpl_swap in H1; simpl_swap in H2.
repeat rewrite bind_mapV_comp; auto.
Qed.
Lemma oe_bind {V W:Set}: ∀ Rel (P Q:proc V) (f:V→ proc W) N,
fn P [<=] N → fn Q [<=] N → (∀ x, fn (f x) [<=] N) →
mod_aeq Rel → open_extension Rel P Q →
open_extension Rel (bind f N P)(bind f N Q).
Proof. intros_all. eapply H2. revgoals. shelve.
rewrites (>> aeq_bind_2 N0 (union N0 N));
intros; try rewrite H6; try fsetdec;
rewrites (>> aeq_bind_3 (bind f (union N0 N) P));
[ rewrite fn_bind; intros; try rewrite H1; fsetdec
| apply aeq_bind_2; intros; try rewrite H1; fsetdec
| rewrite bind_bind; try reflexivity;
intros; try rewrite H1; try rewrite H6; fsetdec ].
rewrites (>> aeq_bind_2 N0 (union N0 N));
intros; try rewrite H6; try fsetdec;
rewrites (>> aeq_bind_3 (bind f (union N0 N) Q));
[ rewrite fn_bind; intros; try rewrite H1; fsetdec
| apply aeq_bind_2; intros; try rewrite H1; fsetdec
| rewrite bind_bind; try reflexivity;
intros; try rewrite H1; try rewrite H6; fsetdec ].
Unshelve. apply H3. fsetdec. fsetdec. intro. apply fn_bind.
rewrite H1; fsetdec. intro; rewrite H6; fsetdec.
Qed.
Lemma oe_proc0 : ∀ (Rel:binary proc0) (P Q:proc0),
mod_aeq Rel → Rel P Q → open_extension Rel P Q.
Proof.
intros_all; eapply H; try apply H0; symmetry;
apply bind_return; auto; intro; inversion x.
Qed.
Lemma oe_swap {V:Set}: ∀ Rel (P Q:proc V) b c,
mod_aeq Rel → open_extension Rel P Q →
mod_swap Rel → open_extension Rel (swap b c P) (swap b c Q).
Proof. intros_all. rewrite <- (swap_invo _ b c). rewrite <- (swap_invo _ b c) at 1.
simpl_swap in H3 H2. eapply H. 2-3: rewrite swap_bind; simpl_swap.
apply H1. apply H0; try intro; simpl_swap.
Qed.
Lemma mod_aeq_oe {V:Set} : ∀ Rel, mod_aeq Rel →
mod_aeq (@open_extension V Rel).
Proof. intros_all. eapply H. apply H0. rewrite H1; eauto. rewrite H2; auto.
eauto. apply aeq_bind_3; auto. apply aeq_bind_3; auto.
Qed.