Library Bisimulation
Definition is_proc_Rel {V:Set} (Rel: binary (proc V)) := ∀ P Q, Rel P Q → is_proc P ∧ is_proc Q.
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), is_agent C → 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), is_agent F →
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 := is_proc_Rel Rel ∧
∀ 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 []; 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:var) (F:abs), lts P (inp a) (ag_abs F) → ∀ (C:conc), is_agent (ag_conc C)
→ 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), is_agent (ag_abs F)
→ ∃ (C':conc), lts Q (out a)(ag_conc C') ∧ Rel (appr F C) (appr F C')).
Definition simulation (Rel: binary proc0) : Prop := is_proc_Rel Rel ∧
∀ 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)).
Hint Extern 1 (is_proc_Rel ?Rel) ⇒
match goal with
| H : simulation Rel |- _ ⇒ destruct H; intuition
| H : simulation_late Rel |- _ ⇒ destruct H; intuition
end:bisim.
Hint Extern 1 (is_proc ?P) ⇒
match goal with
| H1 : is_proc_Rel ?Rel, H2: ?Rel P _ |- _ ⇒ forwards: H1 H2; intuition
| H1 : is_proc_Rel ?Rel, H2: ?Rel _ P |- _ ⇒ forwards: H1 H2; intuition
| H1 : simulation ?Rel, H2: ?Rel P _ |- _ ⇒ destruct H1; intuition
| H1 : simulation ?Rel, H2: ?Rel _ P |- _ ⇒ destruct H1; intuition
| H1 : simulation_late ?Rel, H2: ?Rel P _ |- _ ⇒ destruct H1; intuition
| H1 : simulation_late ?Rel, H2: ?Rel _ P |- _ ⇒ destruct H1; intuition
| H1 : bisimulation ?Rel, H2: ?Rel P _ |- _ ⇒ destruct H1; intuition
| H1 : bisimulation ?Rel, H2: ?Rel _ P |- _ ⇒ destruct H1; intuition
end:bisim.
Ltac forwards_test Rel := try (match goal with
| H1: ∀ P Q, Rel P Q → _
,
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 _) _, H3: is_agent (ag_conc ?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 _) _, H3: is_agent (ag_abs ?F) |- _ ⇒
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 H. inverts H0. split.
+ intros_all. inverts H0. intuition.
+ intros. inverts H0. destruct H4. forwards_test R; forwards_test S; eexists;
intuition; try solve [eassumption]; eexists; intuition eassumption.
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 H. destruct H0. split.
+ intros_all. inverts H3; intuition.
+ intros. inverts H3;
[forwards_test Rel; eexists; intuition eauto; left× |
forwards_test Rel'; eexists; intuition eauto; right*].
Qed.
Lemma late_implies_sim : ∀ Rel, simulation_late Rel → simulation Rel.
Proof.
intros. destruct H. split×.
intros. splits; intros.
- forwards*: H0 H1 H2. destruct H3 as [A' [ ]]. forwards*: lts_tau_proc H3.
destruct H5. inverts H5. ∃ x; intuition. inverts× H4.
- forwards*: H0 H1 H2. destruct H5 as [A' [ ]]. forwards*: lts_inp_abs H5.
destruct H7. inverts H7. ∃ x; intuition.
destruct F as []; destruct x as []; inverts H6. forwards*: H10 C.
- forwards*: H0 H1 H2. destruct H4 as [A' [ ]]. forwards*: lts_out_conc H4.
destruct H6. inverts H6. ∃ x; intuition.
destruct C as []; destruct x as []; inverts H5. forwards*: H9 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.
Definition id_bisim (P Q:proc0) := P=Q ∧ is_proc P.
Hint Unfold id_bisim bisimulation bisimilarity:bisim.
Lemma id_bisim_bisim: bisimulation id_bisim.
Proof.
apply sim_sym_imply_bisim.
+ split. intros_all. unfold id_bisim in ×. destruct H. subst. intuition.
intros. unfold id_bisim in *; destruct H; subst; eexists; intuition eauto with hopi.
+ intros_all. unfold id_bisim in *; destruct H; subst; intuition.
Qed.
Lemma bisim_refl: ∀ P, is_proc P → bisimilarity P P.
Proof.
intros P. ∃ id_bisim. split. apply id_bisim_bisim. auto with bisim.
Qed.
Lemma bisim_is_bisimulation : bisimulation bisimilarity.
Proof.
apply sim_sym_imply_bisim.
+ split.
- intros_all. unfold bisimilarity in H. destruct H. intuition.
- intros. inverts H. destruct H0. assert (Hbisim:=H).
destruct H as [Hr Hrconv]. destruct Hr.
forwards_test x; eexists; intuition; try eassumption; ∃ x; intuition.
+ apply bisim_sym.
Qed.
two bisimilar terms are related by a symetric bisimulation
Lemma bisim_exists_sym_rel : ∀ P Q, bisimilarity P Q →
∃ Rel, sym Rel ∧ simulation Rel ∧ Rel P Q.
Proof.
intros.
destruct H as [Rel [Hbis Hpq]].
∃ (LibRelation.union Rel (inverse Rel)).
destruct Hbis as [ Hsim Hsimsym ].
splits.
- intros_all. destruct H. right. auto. left. auto.
- apply union_sim_is_sim; auto.
- left. auto.
Qed.
Definition rename_compatible {V:Set} Rel := ∀ (P Q:proc V) k x,
x \notin fn P \u fn Q → is_proc (open k x P) → is_proc (open k x Q)
→ Rel (open k x P) (open k x Q) →
∀ y, y \notin fn P \u fn Q → Rel (open k y P) (open k y Q).
Inductive rel_renamed (Rel: binary proc0) : binary proc0 :=
| rrenamed_base : ∀ (P Q:proc0), Rel P Q → rel_renamed Rel P Q
| rrenamed_def : ∀ (P Q:proc0) k x y, rel_renamed Rel (open k x P) (open k x Q)
→ is_proc (open k x P) → is_proc (open k x Q)
→ x \notin fn P \u fn Q→ y \notin fn P \u fn Q
→ rel_renamed Rel (open k y P) (open k y Q).
Lemma simulation_rel_renamed: ∀ Rel, simulation Rel → simulation (rel_renamed Rel).
Proof.
intros_all. split.
× intros_all. induction H0. auto with bisim.
split; apply is_proc_rename with x; intuition.
× intros. destruct H. induction H0; intros.
+ forwards_test Rel; eauto using rrenamed_base.
+ destruct (classic (x=y)).
subst. apply IHrel_renamed; auto.
assert (HnotinP:∀ P k x l A, x \notin fn P → x \notin fn_agent A →
lts (open k x P) l (open_agent k x A) →
∀ y, y \notin fn P → y \notin fn_agent A).
intros. forwards*: lts_fn H9. forwards: @fn_agent_open_rev A k0 x0.
forwards: @subset_trans H12 H11. clear H12 H11. intros_all.
destruct (classic (y0 = x0)). subst. autofnF. apply H13 in H11. autofnF.
splits; intros.
- remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H8 as [[P'' |[]|[]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H9 x). rewrite subst_lab_id in H9; try solve [simpl; auto].
remember (open k x Q) as Q0x. forwards_test (rel_renamed Rel).
forwards*: lts_open HeqQ0x H11.
destruct H15 as [[Q'' |[]|[]] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
rewrite subst_lab_id in HltsA''; try solve [simpl; auto]. simpl in HltsA'', H9.
∃ (open k y Q''); intuition.
eapply rrenamed_def; eauto with hopi bisim.
forwards*: HnotinP P k y (ag_proc P'') x. eassumption.
forwards*: HnotinP Q k x (ag_proc Q'') y. eassumption.
- rename H9 into HwfC. remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H9 as [[ |[P'']|[]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H10 x).
assert (x ≠ a).
subst. forwards*: notin_fn_notin_fnlab x H7. autofnF.
remember (open k x Q) as Q0x. simpl in H10.
intuition. clear H15 H12.
forwards*: decomp_agent (ag_conc C) k y.
destruct H12 as [[ | []|[]] [Hc Hyc]]; inverts Hc.
forwards*: decomp_agent_gen (ag_conc (conc_def n p p0))(S k) x.
autobnF. assert (x0 = S k+n) by omega. subst. forwards: H8 (S k+n). autobnF.
left. intuition. omega.
assert (x0 = S k+n) by omega. subst. forwards: H8 (S k+n). autobnF.
right. intuition. omega.
destruct H12 as [[ | []|[]] [Hc' Hxc]]; inverts Hc'.
rename n0 into n. rename p1 into p. rename p2 into p0.
pick_fresh_fset_V Empty_set (fn P'') z.
replace (S k +n) with (S (k+n)) in × by omega.
forwards*: H14 H10 (conc_def n (open (k+n) x (open (S(k+n)) z p))
(open (k+n) x (open (S(k+n)) z p0))).
intros_all. forwards: H8 k0. autobnF. auto.
intros_all. repeat (rewrite bn_open). simpl in HwfC, Hyc.
forwards*: HwfC k0. autobnF.
destruct H12 as [F' [ HltsF' HrelF']].
forwards*: lts_open HeqQ0x HltsF'.
destruct H12 as [ [|[Q'']|[]] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
replace (inp (If a = y then x else a)) with (subst_lab (inp a) y x) in HltsA''
at 1 by auto.
rewrite subst_lab_inv in HltsA''; try solve [simpl; autofs].
simpl in HltsA'', H9.
∃ (abs_def (open k y Q'')); intuition.
simpl in HrelF'.
assert (∀ P, genNu n
(subst ((shiftN n) (open k x P)) (open (k + n) x (open (S (k + n)) z p)) //
open (k + n) x (open (S (k + n)) z p0)) =
open k x (genNu n (subst ((shiftN n) P) (open (S (k + n)) z p) //
open (S (k + n)) z p0))).
intros. forwards: (appr_open (open (S (k + n)) z p)(open (S (k + n)) z p0) P0 n k) x.
rewrite× H12.
rewrite (H12 P'') in HrelF'. rewrite (H12 Q'') in HrelF'. clear H12.
assert (bn P'' \c \{ k}).
assert (is_proc (open k x P'')) by auto with hopi.
forwards: @is_proc_bn H12. rewrite bn_open in H13.
apply remove_subset_union in H13. rewrite× union_empty_l in H13.
assert (bn Q'' \c \{ k}).
assert (is_proc (open k x Q'')) by auto with hopi.
forwards: @is_proc_bn H13. rewrite bn_open in H15.
apply remove_subset_union in H15. rewrite× union_empty_l in H15.
forwards: rrenamed_def k x y HrelF'.
rewrite open_genNu. apply is_proc_genNu. intros. apply H8.
autobnF. false. omega.
rewrite open_genNu. apply is_proc_genNu. intros. apply H8.
autobnF. false. omega.
forwards*: HnotinP P k y (abs_def P'') x. eassumption.
autofnF.
forwards*: HnotinP Q k x (abs_def Q'') y. eassumption.
assert (y \notin
fn_agent (conc_def n (open (S (k + n)) z p) (open (S (k + n)) z p0))).
autofnF. apply H5. forwards: @fn_open_rev p (S (k+n)) x. autofs.
apply H20. forwards: @fn_open_rev p0 (S (k+n)) x. autofs.
autofnF.
clear HrelF'.
assert (idP'': ∀ z, P'' = open (S k) z P'').
intros; rewrite open_id. auto. autofs. omega.
assert (idQ'': ∀ z, Q'' = open (S k) z Q'').
intros; rewrite open_id. auto. autofs. omega.
rewrite (idP'' z), (idQ'' z) in H15.
assert (∀ P z, genNu n
(subst ((shiftN n) (open (S k) z P)) (open (S (k + n)) z p) //
open (S (k + n)) z p0) =
open (S k) z (genNu n (subst ((shiftN n) P) p // p0))).
intros. forwards*: (appr_open p p0 P0 n (S k)) z0.
rewrite (H16 P''), (H16 Q'') in H15.
do 2 (rewrite (open_open _ k (S k)) in H15; try solve [autofs]).
forwards: rrenamed_def (S k) z x H15.
repeat (rewrite open_genNu). apply is_proc_genNu. intros. apply H8; autobnF.
false; omega.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H8; autobnF. false; omega.
forwards*: HnotinP P k y (abs_def P'') z. eassumption.
forwards*: HnotinP Q k x (abs_def Q'') z. eassumption.
autofnF.
forwards*: HnotinP P k y (abs_def P'') x. eassumption.
autofnF.
clear H15. do 2 (rewrite (open_open _ (S k) k) in H17; try solve [autofs]).
rewrite <- (H16 P'' x), <- (H16 Q'' x) in H17.
rewrite <- (idP'' x), <- (idQ'' x) in H17.
clear H16. simpl.
assert (∀ P, open k y (genNu n (subst ((shiftN n) P)(open (S (k + n)) x p) // open (S (k + n)) x p0))
= genNu n (subst ((shiftN n) (open k y P)) (open (k + n) y (open (S (k + n)) x p)) //
open (k + n) y (open (S (k + n)) x p0))).
intros. forwards*: (appr_open (open (S (k + n)) x p) (open (S (k + n)) x p0) P0 n k y).
rewrite <- (H15 P''). rewrite× <- (H15 Q'').
- remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H9 as [[ |[]|[n p p0]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H10 x).
assert (x ≠ a).
subst. forwards*: notin_fn_notin_fnlab x H7. autofnF.
remember (open k x Q) as Q0x. simpl in H10.
intuition. clear H14 H12.
forwards*: decomp_agent F k y.
destruct H12 as [[ | [P'']|[]] [Hc HyF]]; inverts Hc.
forwards*: decomp_agent_gen (abs_def P'') (S k) x.
forwards: @is_proc_bn H8. autobnF. assert (S k \in bn P'' \- \{k}). autofs. omega.
rewrite H12 in H9. autofs.
destruct H12 as [[ | [P']|[]] [Hf HxF]]; inverts Hf. rename P' into P''.
pick_fresh_fset_V Empty_set (fn P'') z.
forwards*: H15 H10 (abs_def (open k x (open (S k) z P''))).
simpl. apply is_proc_rename with y.
rewrite open_open; try solve [autofs].
apply is_proc_rename with x. simpl in H8.
rewrite open_open; try solve [autofs].
destruct H12 as [C' [ HltsC' HrelC']].
forwards*: lts_open HeqQ0x HltsC'.
destruct H12 as [ [|[]|[n' p' p0']] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
replace (out (If a = y then x else a)) with (subst_lab (out a) y x) in HltsA''
at 1 by auto.
rewrite subst_lab_inv in HltsA''; try solve [simpl; autofs].
simpl in HltsA'', H9.
∃ (conc_def n' (open (k+n') y p')(open (k+n') y p0')); intuition.
simpl in HrelC'.
assert (∀ p p0 n,
genNu n (subst ((shiftN n) (open k x (open (S k) z P''))) (open (k + n) x p) //
open (k + n) x p0) =
open k x (genNu n (subst ((shiftN n)(open (S k) z P'')) p // p0))).
intros. forwards: (appr_open p1 p2 (open (S k) z P'') n0 k) x.
rewrite× H12.
rewrite (H12 p p0 n) in HrelC'. rewrite (H12 p' p0' n') in HrelC'. clear H12.
assert (is_agent (conc_def n (open (k+n) x p)(open (k+n) x p0))) by auto with hopi.
assert (is_agent (conc_def n' (open (k+n') x p')(open (k+n') x p0'))) by auto with hopi.
assert (bn P'' \c \{k} \u \{S k}).
forwards: @is_proc_bn H8. repeat (rewrite bn_open in H14).
apply remove_subset_union in H14. autofs. destruct (classic (x0=S k)); intuition auto.
left. assert (x0 \in bn P'' \- \{S k}) by autofs. apply H14 in H31. autofs.
forwards: rrenamed_def k x y HrelC'.
rewrite open_genNu. apply is_proc_genNu. intros.
apply H12; autobnF. false. omega.
rewrite open_genNu. apply is_proc_genNu. intros.
apply H13. autobnF. false. omega.
forwards*: HnotinP P k y (conc_def n p p0) x. eassumption.
autofnF.
forwards*: HnotinP Q k x (conc_def n' p' p0') y. eassumption.
assert (y \notin fn (open (S k) z P'')).
autofnF. apply HyF. forwards: @fn_open_rev P'' (S k) x. autofs.
autofnF.
clear HrelC'.
assert (Hpz: ∀ z, p = open ((S k)+n) z p).
intros; rewrite open_id. auto. intros_all. forwards: H12 ((S k)+n).
autobnF. left. autobnF. intuition. omega.
assert (Hp0z: ∀ z, p0 = open ((S k)+n) z p0).
intros; rewrite open_id. auto. intros_all. forwards: H12 ((S k)+n).
autobnF. right. autobnF. intuition. omega.
assert (Hp'z: ∀ z, p' = open ((S k)+n') z p').
intros; rewrite open_id. auto. intros_all. forwards: H13 ((S k)+n').
autobnF. left. autobnF. intuition. omega.
assert (Hp0'z: ∀ z, p0' = open ((S k)+n') z p0').
intros; rewrite open_id. auto. intros_all. forwards: H13 ((S k)+n').
autobnF. right. autobnF. intuition. omega.
rewrite (Hpz z), (Hp0z z), (Hp'z z), (Hp0'z z) in H16.
assert (∀ p p0 n z, genNu n
(subst ((shiftN n) (open (S k) z P'')) (open ((S k) + n) z p) //
open ((S k) + n) z p0) =
open (S k) z (genNu n (subst ((shiftN n) P'') p // p0))).
intros. forwards: (appr_open p1 p2 P'' n0 (S k)) z0.
replace (S (k+n0)) with ((S k)+n0) in H17 by omega. rewrite× H17.
rewrite (H17 p p0 n), (H17 p' p0' n') in H16.
do 2 (rewrite (open_open _ k (S k)) in H16; try solve [autofs]).
forwards: rrenamed_def (S k) z x H16.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H12; autobnF; false; omega.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H13; autobnF; false; omega.
forwards*: HnotinP P k y (conc_def n p p0) z. eassumption.
forwards*: HnotinP Q k x (conc_def n' p' p0') z. eassumption.
autofnF.
forwards*: HnotinP P k y (conc_def n p p0) x. eassumption.
autofnF.
clear H16. do 2 (rewrite (open_open _ (S k) k) in H18; try solve [autofs]).
rewrite <- (H17 p p0 n x), <- (H17 p' p0' n' x) in H18.
rewrite <- (Hpz x), <- (Hp0z x), <- (Hp'z x), <- (Hp0'z x) in H18.
simpl.
assert (∀ p p0 n, open k y (genNu n (subst ((shiftN n)(open (S k) x P'')) p // p0))
= genNu n (subst ((shiftN n) (open k y (open (S k) x P''))) (open (k + n) y p) // open (k + n) y p0)).
intros. forwards*: (appr_open p1 p2 (open (S k) x P'') n0 k) y.
rewrite <- (H16 p p0 n). rewrite× <- (H16 p' p0' n').
Qed.
Lemma bisim_rename_compatible : rename_compatible bisimilarity.
Proof.
intros_all.
forwards: bisim_exists_sym_rel H2.
destruct H4 as [Rel [Hsym [Hsim Hpq]]].
∃ (rel_renamed Rel).
split.
- apply sim_sym_imply_bisim.
apply× simulation_rel_renamed.
intros_all. induction H4. apply rrenamed_base; auto. eapply rrenamed_def; eauto.
- eapply rrenamed_def; eauto. apply rrenamed_base; auto.
Qed.
∃ Rel, sym Rel ∧ simulation Rel ∧ Rel P Q.
Proof.
intros.
destruct H as [Rel [Hbis Hpq]].
∃ (LibRelation.union Rel (inverse Rel)).
destruct Hbis as [ Hsim Hsimsym ].
splits.
- intros_all. destruct H. right. auto. left. auto.
- apply union_sim_is_sim; auto.
- left. auto.
Qed.
Definition rename_compatible {V:Set} Rel := ∀ (P Q:proc V) k x,
x \notin fn P \u fn Q → is_proc (open k x P) → is_proc (open k x Q)
→ Rel (open k x P) (open k x Q) →
∀ y, y \notin fn P \u fn Q → Rel (open k y P) (open k y Q).
Inductive rel_renamed (Rel: binary proc0) : binary proc0 :=
| rrenamed_base : ∀ (P Q:proc0), Rel P Q → rel_renamed Rel P Q
| rrenamed_def : ∀ (P Q:proc0) k x y, rel_renamed Rel (open k x P) (open k x Q)
→ is_proc (open k x P) → is_proc (open k x Q)
→ x \notin fn P \u fn Q→ y \notin fn P \u fn Q
→ rel_renamed Rel (open k y P) (open k y Q).
Lemma simulation_rel_renamed: ∀ Rel, simulation Rel → simulation (rel_renamed Rel).
Proof.
intros_all. split.
× intros_all. induction H0. auto with bisim.
split; apply is_proc_rename with x; intuition.
× intros. destruct H. induction H0; intros.
+ forwards_test Rel; eauto using rrenamed_base.
+ destruct (classic (x=y)).
subst. apply IHrel_renamed; auto.
assert (HnotinP:∀ P k x l A, x \notin fn P → x \notin fn_agent A →
lts (open k x P) l (open_agent k x A) →
∀ y, y \notin fn P → y \notin fn_agent A).
intros. forwards*: lts_fn H9. forwards: @fn_agent_open_rev A k0 x0.
forwards: @subset_trans H12 H11. clear H12 H11. intros_all.
destruct (classic (y0 = x0)). subst. autofnF. apply H13 in H11. autofnF.
splits; intros.
- remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H8 as [[P'' |[]|[]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H9 x). rewrite subst_lab_id in H9; try solve [simpl; auto].
remember (open k x Q) as Q0x. forwards_test (rel_renamed Rel).
forwards*: lts_open HeqQ0x H11.
destruct H15 as [[Q'' |[]|[]] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
rewrite subst_lab_id in HltsA''; try solve [simpl; auto]. simpl in HltsA'', H9.
∃ (open k y Q''); intuition.
eapply rrenamed_def; eauto with hopi bisim.
forwards*: HnotinP P k y (ag_proc P'') x. eassumption.
forwards*: HnotinP Q k x (ag_proc Q'') y. eassumption.
- rename H9 into HwfC. remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H9 as [[ |[P'']|[]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H10 x).
assert (x ≠ a).
subst. forwards*: notin_fn_notin_fnlab x H7. autofnF.
remember (open k x Q) as Q0x. simpl in H10.
intuition. clear H15 H12.
forwards*: decomp_agent (ag_conc C) k y.
destruct H12 as [[ | []|[]] [Hc Hyc]]; inverts Hc.
forwards*: decomp_agent_gen (ag_conc (conc_def n p p0))(S k) x.
autobnF. assert (x0 = S k+n) by omega. subst. forwards: H8 (S k+n). autobnF.
left. intuition. omega.
assert (x0 = S k+n) by omega. subst. forwards: H8 (S k+n). autobnF.
right. intuition. omega.
destruct H12 as [[ | []|[]] [Hc' Hxc]]; inverts Hc'.
rename n0 into n. rename p1 into p. rename p2 into p0.
pick_fresh_fset_V Empty_set (fn P'') z.
replace (S k +n) with (S (k+n)) in × by omega.
forwards*: H14 H10 (conc_def n (open (k+n) x (open (S(k+n)) z p))
(open (k+n) x (open (S(k+n)) z p0))).
intros_all. forwards: H8 k0. autobnF. auto.
intros_all. repeat (rewrite bn_open). simpl in HwfC, Hyc.
forwards*: HwfC k0. autobnF.
destruct H12 as [F' [ HltsF' HrelF']].
forwards*: lts_open HeqQ0x HltsF'.
destruct H12 as [ [|[Q'']|[]] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
replace (inp (If a = y then x else a)) with (subst_lab (inp a) y x) in HltsA''
at 1 by auto.
rewrite subst_lab_inv in HltsA''; try solve [simpl; autofs].
simpl in HltsA'', H9.
∃ (abs_def (open k y Q'')); intuition.
simpl in HrelF'.
assert (∀ P, genNu n
(subst ((shiftN n) (open k x P)) (open (k + n) x (open (S (k + n)) z p)) //
open (k + n) x (open (S (k + n)) z p0)) =
open k x (genNu n (subst ((shiftN n) P) (open (S (k + n)) z p) //
open (S (k + n)) z p0))).
intros. forwards: (appr_open (open (S (k + n)) z p)(open (S (k + n)) z p0) P0 n k) x.
rewrite× H12.
rewrite (H12 P'') in HrelF'. rewrite (H12 Q'') in HrelF'. clear H12.
assert (bn P'' \c \{ k}).
assert (is_proc (open k x P'')) by auto with hopi.
forwards: @is_proc_bn H12. rewrite bn_open in H13.
apply remove_subset_union in H13. rewrite× union_empty_l in H13.
assert (bn Q'' \c \{ k}).
assert (is_proc (open k x Q'')) by auto with hopi.
forwards: @is_proc_bn H13. rewrite bn_open in H15.
apply remove_subset_union in H15. rewrite× union_empty_l in H15.
forwards: rrenamed_def k x y HrelF'.
rewrite open_genNu. apply is_proc_genNu. intros. apply H8.
autobnF. false. omega.
rewrite open_genNu. apply is_proc_genNu. intros. apply H8.
autobnF. false. omega.
forwards*: HnotinP P k y (abs_def P'') x. eassumption.
autofnF.
forwards*: HnotinP Q k x (abs_def Q'') y. eassumption.
assert (y \notin
fn_agent (conc_def n (open (S (k + n)) z p) (open (S (k + n)) z p0))).
autofnF. apply H5. forwards: @fn_open_rev p (S (k+n)) x. autofs.
apply H20. forwards: @fn_open_rev p0 (S (k+n)) x. autofs.
autofnF.
clear HrelF'.
assert (idP'': ∀ z, P'' = open (S k) z P'').
intros; rewrite open_id. auto. autofs. omega.
assert (idQ'': ∀ z, Q'' = open (S k) z Q'').
intros; rewrite open_id. auto. autofs. omega.
rewrite (idP'' z), (idQ'' z) in H15.
assert (∀ P z, genNu n
(subst ((shiftN n) (open (S k) z P)) (open (S (k + n)) z p) //
open (S (k + n)) z p0) =
open (S k) z (genNu n (subst ((shiftN n) P) p // p0))).
intros. forwards*: (appr_open p p0 P0 n (S k)) z0.
rewrite (H16 P''), (H16 Q'') in H15.
do 2 (rewrite (open_open _ k (S k)) in H15; try solve [autofs]).
forwards: rrenamed_def (S k) z x H15.
repeat (rewrite open_genNu). apply is_proc_genNu. intros. apply H8; autobnF.
false; omega.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H8; autobnF. false; omega.
forwards*: HnotinP P k y (abs_def P'') z. eassumption.
forwards*: HnotinP Q k x (abs_def Q'') z. eassumption.
autofnF.
forwards*: HnotinP P k y (abs_def P'') x. eassumption.
autofnF.
clear H15. do 2 (rewrite (open_open _ (S k) k) in H17; try solve [autofs]).
rewrite <- (H16 P'' x), <- (H16 Q'' x) in H17.
rewrite <- (idP'' x), <- (idQ'' x) in H17.
clear H16. simpl.
assert (∀ P, open k y (genNu n (subst ((shiftN n) P)(open (S (k + n)) x p) // open (S (k + n)) x p0))
= genNu n (subst ((shiftN n) (open k y P)) (open (k + n) y (open (S (k + n)) x p)) //
open (k + n) y (open (S (k + n)) x p0))).
intros. forwards*: (appr_open (open (S (k + n)) x p) (open (S (k + n)) x p0) P0 n k y).
rewrite <- (H15 P''). rewrite× <- (H15 Q'').
- remember (open k y P) as P1'.
forwards*: lts_open HeqP1' H7. subst; eapply is_proc_rename; eauto.
destruct H9 as [[ |[]|[n p p0]] [Ha' HltsA']]; inverts Ha'. destruct HltsA'.
specialize (H10 x).
assert (x ≠ a).
subst. forwards*: notin_fn_notin_fnlab x H7. autofnF.
remember (open k x Q) as Q0x. simpl in H10.
intuition. clear H14 H12.
forwards*: decomp_agent F k y.
destruct H12 as [[ | [P'']|[]] [Hc HyF]]; inverts Hc.
forwards*: decomp_agent_gen (abs_def P'') (S k) x.
forwards: @is_proc_bn H8. autobnF. assert (S k \in bn P'' \- \{k}). autofs. omega.
rewrite H12 in H9. autofs.
destruct H12 as [[ | [P']|[]] [Hf HxF]]; inverts Hf. rename P' into P''.
pick_fresh_fset_V Empty_set (fn P'') z.
forwards*: H15 H10 (abs_def (open k x (open (S k) z P''))).
simpl. apply is_proc_rename with y.
rewrite open_open; try solve [autofs].
apply is_proc_rename with x. simpl in H8.
rewrite open_open; try solve [autofs].
destruct H12 as [C' [ HltsC' HrelC']].
forwards*: lts_open HeqQ0x HltsC'.
destruct H12 as [ [|[]|[n' p' p0']] [Ha'' [HxnotinA'' HltsA'']]]; inverts Ha''.
specialize (HltsA'' y). subst.
replace (out (If a = y then x else a)) with (subst_lab (out a) y x) in HltsA''
at 1 by auto.
rewrite subst_lab_inv in HltsA''; try solve [simpl; autofs].
simpl in HltsA'', H9.
∃ (conc_def n' (open (k+n') y p')(open (k+n') y p0')); intuition.
simpl in HrelC'.
assert (∀ p p0 n,
genNu n (subst ((shiftN n) (open k x (open (S k) z P''))) (open (k + n) x p) //
open (k + n) x p0) =
open k x (genNu n (subst ((shiftN n)(open (S k) z P'')) p // p0))).
intros. forwards: (appr_open p1 p2 (open (S k) z P'') n0 k) x.
rewrite× H12.
rewrite (H12 p p0 n) in HrelC'. rewrite (H12 p' p0' n') in HrelC'. clear H12.
assert (is_agent (conc_def n (open (k+n) x p)(open (k+n) x p0))) by auto with hopi.
assert (is_agent (conc_def n' (open (k+n') x p')(open (k+n') x p0'))) by auto with hopi.
assert (bn P'' \c \{k} \u \{S k}).
forwards: @is_proc_bn H8. repeat (rewrite bn_open in H14).
apply remove_subset_union in H14. autofs. destruct (classic (x0=S k)); intuition auto.
left. assert (x0 \in bn P'' \- \{S k}) by autofs. apply H14 in H31. autofs.
forwards: rrenamed_def k x y HrelC'.
rewrite open_genNu. apply is_proc_genNu. intros.
apply H12; autobnF. false. omega.
rewrite open_genNu. apply is_proc_genNu. intros.
apply H13. autobnF. false. omega.
forwards*: HnotinP P k y (conc_def n p p0) x. eassumption.
autofnF.
forwards*: HnotinP Q k x (conc_def n' p' p0') y. eassumption.
assert (y \notin fn (open (S k) z P'')).
autofnF. apply HyF. forwards: @fn_open_rev P'' (S k) x. autofs.
autofnF.
clear HrelC'.
assert (Hpz: ∀ z, p = open ((S k)+n) z p).
intros; rewrite open_id. auto. intros_all. forwards: H12 ((S k)+n).
autobnF. left. autobnF. intuition. omega.
assert (Hp0z: ∀ z, p0 = open ((S k)+n) z p0).
intros; rewrite open_id. auto. intros_all. forwards: H12 ((S k)+n).
autobnF. right. autobnF. intuition. omega.
assert (Hp'z: ∀ z, p' = open ((S k)+n') z p').
intros; rewrite open_id. auto. intros_all. forwards: H13 ((S k)+n').
autobnF. left. autobnF. intuition. omega.
assert (Hp0'z: ∀ z, p0' = open ((S k)+n') z p0').
intros; rewrite open_id. auto. intros_all. forwards: H13 ((S k)+n').
autobnF. right. autobnF. intuition. omega.
rewrite (Hpz z), (Hp0z z), (Hp'z z), (Hp0'z z) in H16.
assert (∀ p p0 n z, genNu n
(subst ((shiftN n) (open (S k) z P'')) (open ((S k) + n) z p) //
open ((S k) + n) z p0) =
open (S k) z (genNu n (subst ((shiftN n) P'') p // p0))).
intros. forwards: (appr_open p1 p2 P'' n0 (S k)) z0.
replace (S (k+n0)) with ((S k)+n0) in H17 by omega. rewrite× H17.
rewrite (H17 p p0 n), (H17 p' p0' n') in H16.
do 2 (rewrite (open_open _ k (S k)) in H16; try solve [autofs]).
forwards: rrenamed_def (S k) z x H16.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H12; autobnF; false; omega.
repeat (rewrite open_genNu). apply is_proc_genNu. intros.
apply H13; autobnF; false; omega.
forwards*: HnotinP P k y (conc_def n p p0) z. eassumption.
forwards*: HnotinP Q k x (conc_def n' p' p0') z. eassumption.
autofnF.
forwards*: HnotinP P k y (conc_def n p p0) x. eassumption.
autofnF.
clear H16. do 2 (rewrite (open_open _ (S k) k) in H18; try solve [autofs]).
rewrite <- (H17 p p0 n x), <- (H17 p' p0' n' x) in H18.
rewrite <- (Hpz x), <- (Hp0z x), <- (Hp'z x), <- (Hp0'z x) in H18.
simpl.
assert (∀ p p0 n, open k y (genNu n (subst ((shiftN n)(open (S k) x P'')) p // p0))
= genNu n (subst ((shiftN n) (open k y (open (S k) x P''))) (open (k + n) y p) // open (k + n) y p0)).
intros. forwards*: (appr_open p1 p2 (open (S k) x P'') n0 k) y.
rewrite <- (H16 p p0 n). rewrite× <- (H16 p' p0' n').
Qed.
Lemma bisim_rename_compatible : rename_compatible bisimilarity.
Proof.
intros_all.
forwards: bisim_exists_sym_rel H2.
destruct H4 as [Rel [Hsym [Hsim Hpq]]].
∃ (rel_renamed Rel).
split.
- apply sim_sym_imply_bisim.
apply× simulation_rel_renamed.
intros_all. induction H4. apply rrenamed_base; auto. eapply rrenamed_def; eauto.
- eapply rrenamed_def; eauto. apply rrenamed_base; auto.
Qed.
Definition open_extension {V:Set} (Rel:binary proc0) (P Q:proc V) :=
∀ (f: V→ proc0), (∀ v, is_proc (f v)) → Rel (bind f P) (bind f 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, trans Rel → trans (@open_extension V Rel).
Proof.
intros_all. eauto.
Qed.
Lemma oe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
open_extension Rel P Q → open_extension Rel (mapV f P)(mapV f Q).
Proof.
intros_all. repeat(rewrite bind_mapV_comp); auto.
Qed.
Lemma oe_bind{V W:Set}: ∀ Rel (P Q:proc V) (f:V→ proc W), (∀ v, is_proc (f v)) →
open_extension Rel P Q → open_extension Rel (bind f P)(bind f Q).
Proof.
unfold open_extension. intros. repeat (rewrite bind_bind). apply H0.
intros. apply is_proc_bind; auto.
Qed.
Lemma oe_proc0 : ∀ (Rel:binary proc0) (P Q:proc0), Rel P Q → open_extension Rel P Q.
Proof.
intros_all. repeat (rewrite bind_proc0); auto.
Qed.
Lemma oe_rename: ∀ (Rel:binary proc0), (rename_compatible Rel) →
∀ V, (@rename_compatible V (open_extension Rel)).
Proof.
intros_all.
destruct (classic (x = y)).
subst. auto.
forwards*: @decomp_f f k x.
destruct H6 as [f'].
pick_fresh_fset_V V (fn (bind f' (open k y P)) \u fn (bind f' (open k y Q))) z.
remember (fun v ⇒ open k x (close k y (open k z (f' v)))) as f''. unfold decomp in H6.
assert (∀ v, is_proc (f'' v)).
intros; subst. specialize (H6 v). unfold body in H6. apply is_proc_open_close. intuition.
specialize (H2 f'' H7). rewrite Heqf'' in H2.
do 2 (rewrite× @bind_open' in H2).
forwards: X H2 y.
autofnF; apply fn_bind in H13; auto; intros;
destruct (H6 v); autofnF.
rewrite <- bind_open'. rewrite <- Heqf''. apply is_proc_bind; auto.
rewrite <- bind_open'. rewrite <- Heqf''. apply is_proc_bind; auto.
autofnF; apply fn_bind in H13; auto; intros; autofnF.
repeat (rewrite <- bind_open' in H8).
asserts_rewrite ((fun y0 ⇒ open k y (close k y (open k z (f' y0))))
= fun y0 ⇒ open k z (f' y0)) in H8.
extens; intros; rewrite× @open_close. destruct× (H6 x1) as [ [ ] []].
assert (Hzp: open k y P = open k z (open k y P)).
rewrite (is_proc_open _ k z); auto; eapply is_proc_rename; eauto.
assert (Hzq: open k y Q = open k z (open k y Q)).
rewrite (is_proc_open _ k z); auto; eapply is_proc_rename; eauto.
rewrite Hzp, Hzq in H8; repeat (rewrite bind_open' in H8).
forwards*: (X (bind f' (open k y P)) (bind f' (open k y Q)) k z) x.
rewrite× <- @bind_open'. apply× @is_proc_bind. rewrite× <- Hzp.
eapply is_proc_rename; eauto. intros. destruct× (H6 x0) as [ [] []].
rewrite× <- @bind_open'. apply× @is_proc_bind. rewrite <- Hzq.
eapply is_proc_rename; eauto. intros. destruct× (H6 x0) as [ [] []].
autofnF; apply fn_bind in H14; auto; autofnF; intros; destruct (H6 v); autofnF.
repeat (rewrite <- bind_open' in H9).
do 2 (rewrite (is_proc_open _ k x) in H9); try solve [eapply is_proc_rename; eauto].
replace (fun y ⇒ open k x (f' y)) with f in H9
by (extens; intros v; destruct (H6 v); auto); auto.
Qed.