Library HOC26EarlyBisimulation
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC09GVLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC12Guarded.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC15HObis.
Require Import HOC16CONbis.
Require Import HOC17NORbis.
Require Import HOC18ONORbis.
Require Import HOC19Coincide.
Require Import HOC20Barbed.
Require Import Relations.
Definition in_relation_early (R : RelWfP) : Prop :=
∀ (p q : wfprocess), (R p q) →
∀ (a : chan) (fp : abstraction), {{p -- LabIn a ->> (AA fp)}} →
∀ X, X # p → X # q →
∃ (fq : abstraction), {{q -- LabIn a ->> (AA fq)}} ∧
R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).
Definition in_normal_relation_early (R : RelWfP) : Prop :=
∀ p q, (R p q) → ∀ a fp, {{p--LabIn a->>(AA fp)}} →
∀ m, m ### p → m ### q →
∃ fq, {{q--LabIn a->>(AA fq)}} ∧
(R (wfp_inst_Abs fp (wfp_Send m wfp_Nil)) (wfp_inst_Abs fq (wfp_Send m wfp_Nil))).
Definition out_normal_relation_early (R : RelWfP) : Prop :=
∀ p q, (R p q) →
∀ a (p´ : wfprocess) (p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} →
∀ m X, m ### p → m ### q → X # p → X # q →
∃ (q´ : wfprocess), ∃ (q´´ : wfprocess),
({{q -- LabOut a q´´ ->> (AP q´)}} ∧
(R (wfp_Par (wfp_Abs m X p´´) p´)) (wfp_Par (wfp_Abs m X q´´) q´)).
Definition out_context_relation_early (R : RelWfP) : Prop :=
∀ p q, (R p q) →
∀ a (p´ p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} →
∀ X (s : wfprocess), (GV s) \c (singleton X) →
∃ (q´ : wfprocess), ∃ (q´´ : wfprocess),
({{q--LabOut a q´´->>(AP q´)}} ∧
(R (wfp_Par (wfp_subst p´´ X s) p´) (wfp_Par (wfp_subst q´´ X s) q´))).
Definition IO_bisimulation_early (R : RelWfP) : Prop :=
(Symmetric R) ∧ (in_relation_early R) ∧ (out_relation R) ∧ (var_relation R).
Definition IObis_early (p q : wfprocess) : Prop :=
∃ R, (IO_bisimulation_early R) ∧ (R p q).
Notation "p e≈ q" := (IObis_early p q) (at level 60).
Lemma IObis_eIObis : ∀ p q, p ≈ q ↔ p e≈ q.
Proof.
introv; splits; introv Hbis;
destruct Hbis as (R & (Hs & Hi & Ho & Hv) & Hr).
+ ∃ R; repeat splits×.
clear dependent p; clear dependent q.
introv Hr Ht Hfp Hfq.
specializes Hi Hr Ht.
destruct Hi as (fq & Htq & Hbis). ∃ fq; splits×.
+ rewrite IObis_IObis_ex.
∃ R; repeat splits×.
clear dependent p; clear dependent q.
introv Hr Ht.
lets (X & Hfx) : find_fresh (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfxp & Hfxq).
specializes Hi Hfxp Hfxq; try eassumption.
destruct Hi as (fq & Htq & Hbis).
∃ fq; splits×.
Qed.
Definition Normal_bisimulation_ex_ex (R:binary wfprocess) : Prop :=
(Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation_ex R) ∧ (in_normal_relation_ex R).
Definition NORbis_ex_ex p q : Prop :=
∃ R, (Normal_bisimulation_ex_ex R) ∧ (R p q).
Definition NORbisC_ex_ex (p q : wfprocess) : Prop :=
closed_process p ∧ closed_process q ∧ NORbis_ex_ex p q.
Lemma NORbisC_ex_NORbisC_ex_ex : ∀ p q, NORbisC_ex p q ↔ NORbisC_ex_ex p q.
Proof with automate.
introv. split; introv H. destruct H as (Hcp1 & Hcp2 & H). splits¬.
∃ NORbisC. split¬.
splits¬.
apply NORbisC_sym.
apply NORbisC_tau.
clear dependent p. clear dependent q.
introv Hr Ht.
lets Hyp : NORbisC_out_normal Hr Ht.
destruct Hyp as (q´ & q´´ & Htq & Hio).
∃ q´ q´´; splits×.
lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfm; destruct Hfm as (Hfmp & Hfmq).
lets (X & Hfx) : find_fresh (proc p´´ :: proc q´´ :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfxp & Hfxq).
∃ m X; splits×.
apply in_nor_forall_exists. apply NORbisC_in_normal.
rewrite¬ NORbis_NORbis_ex. splits×.
destruct H as (Hcp & Hcq & Hbis). rewrite <- NORbis_NORbis_ex. splits×.
destruct Hbis as (R & Hbis & Hr).
∃ (R_Swap R); splits×. clear dependent p; clear dependent q. splits×.
introv Hr. inductions Hr.
constructor. apply¬ Hbis.
apply¬ RswCh.
introv Hr. induction Hr; introv Ht.
destruct Hbis as (HR1 & HR2 & HR3 & HR4). eapply HR2 in H; eauto.
edestruct (H p´ Ht) as (q´ & Htq & Hr).
∃ q´. splits¬.
forwards Ht´: wfp_trans_swap_chan_tau m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
edestruct IHHr as (q´ & Htq & Hr´).
eassumption.
∃ (wfp_swap_chan m n q´). splits.
applys¬ wfp_trans_swap_chan_tau.
erewrite <- wfp_swap_chan_involutive at 1. apply¬ RswCh.
introv Hr. induction Hr; introv Ht.
destruct Hbis as (HR1 & HR2 & HR3 & HR4). eapply HR3 in H; auto.
edestruct H as (q´ & q´´ & Htq & m & X & Hfmp & Hfmq & Hfxp´´ & Hfxq´´ & Hr´); try eassumption.
∃ q´ q´´. splits¬.
intros n Y Hfnp Hfnq HfYp´´ HfYq´´.
lets Hr´´ : Rswr Hr´. apply RswCh with (m := m) (n := n) in Hr´´...
assert (Hscp´ : wfp_swap_chan m n p´ = p´).
applys¬ wfp_fresh_chan_swap.
applys× (wfp_cfresh_out _ _ _ _ _ Hfmp Ht).
applys× (wfp_cfresh_out _ _ _ _ _ Hfnp Ht).
assert (Hscq´ : wfp_swap_chan m n q´ = q´).
applys¬ wfp_fresh_chan_swap.
applys× (wfp_cfresh_out _ _ _ _ _ Hfmq Htq).
applys× (wfp_cfresh_out _ _ _ _ _ Hfnq Htq).
assert (Hscp´´ : wfp_swap_chan m n p´´ = p´´).
applys¬ wfp_fresh_chan_swap.
applys× (wfp_cfresh_out _ _ _ _ _ Hfmp Ht).
applys× (wfp_cfresh_out _ _ _ _ _ Hfnp Ht).
assert (Hscq´´ : wfp_swap_chan m n q´´ = q´´).
applys¬ wfp_fresh_chan_swap.
applys× (wfp_cfresh_out _ _ _ _ _ Hfmq Htq).
applys× (wfp_cfresh_out _ _ _ _ _ Hfnq Htq).
repeat rewrite Hscp´, Hscq´, Hscp´´, Hscq´´ in ×.
clear Hscp´ Hscq´ Hscp´´ Hscq´´.
unfolds swap_name; cases_if*; clear e.
assert (Heq_abs_p : wfp_Abs n Y p´´ = wfp_Abs n X p´´).
rewrite wfprocess_eq. simpls. unfolds Abs; fequals.
rewrite (XHE_GoodF X Y). unfolds f; fequals.
unfold swap_gvar; repeat cases_if×.
rewrite¬ <- gfresh_subst_is_swap. rewrite¬ gfresh_subst_rewrite.
do 2 rewrite¬ gfresh_subst_rewrite.
assert (Heq_abs_q : wfp_Abs n Y q´´ = wfp_Abs n X q´´).
rewrite wfprocess_eq. simpls. unfolds Abs; fequals.
rewrite (XHE_GoodF X Y). unfolds f; fequals.
unfold swap_gvar; repeat cases_if×.
rewrite¬ <- gfresh_subst_is_swap. rewrite¬ gfresh_subst_rewrite.
do 2 rewrite¬ gfresh_subst_rewrite.
rewrite Heq_abs_p, Heq_abs_q; auto.
lets Ht´: wfp_trans_swap_chan_out a m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
specialize (IHHr ({{|m, n|}}a) _ _ Ht´).
destruct IHHr as (q´ & q´´ & Htq & Hr´).
lets Htq´ : wfp_trans_swap_chan_out ({{|m, n|}}a) m n Htq.
simpl in Htq´; rewrite swap_name_involutive in Htq´.
eexists; eexists. splits. eassumption.
introv Hfm0p Hfm0q HfXp´´ HfXq´´.
eapply wfp_fresh_chan_cswap in Hfm0p.
simpl in Hfm0p; rewrite¬ swap_chan_involutive in Hfm0p.
eapply wfp_fresh_chan_cswap in Hfm0q.
simpl in Hfm0q; rewrite¬ swap_chan_involutive in Hfm0q.
apply wfp_fresh_gvar_cswap with (m := m) (n := n) in HfXp´´.
apply wfp_fresh_gvar_cswap with (m := m) (n := n) in HfXq´´.
rewrite wfp_swap_chan_involutive in HfXq´´.
specializes Hr´ X Hfm0q HfXq´´.
apply RswCh with (m := m) (n := n) in Hr´...
repeat rewrite swap_name_involutive in ×.
repeat rewrite wfp_swap_chan_involutive in ×. auto.
unfolds.
introv Hr. inductions Hr; introv Ht.
destruct Hbis as (_&_&_& HR4). eapply HR4 in H; eauto.
edestruct H as (fq & Htq & m & Hf1 & Hf2 & Hrq)...
∃ fq; splits...
intros n Hf3 Hf4.
forwards Hre1: wfp_inst_chan_swap (wfp_Send m wfp_Nil) Hf1 Hf3 Ht...
rewrite swap_name_left in Hre1.
forwards Hre2: wfp_inst_chan_swap (wfp_Send m wfp_Nil) Hf2 Hf4 Htq...
rewrite swap_name_left in Hre2.
rewrite <- Hre1, <- Hre2.
applys¬ RswCh; constructor; eapply Hrq.
rename fp into fp0.
forwards (fp & Ht´ & Heq1): wfp_trans_swap_chan_in a m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
specialize (IHHr ({{|m, n|}}a) fp Ht´). destruct IHHr as (fq & Htq & Hr´).
forwards (fq0 & Htq´ & Heq2): wfp_trans_swap_chan_in ({{|m, n|}}a) m n Htq.
simpl in Htq´; rewrite swap_name_involutive in Htq´.
∃ fq0; splits...
introv Hf3 Hf4.
specializes Heq1 (wfp_Send m0 wfp_Nil); specializes Heq2 (wfp_Send ({{|m, n|}}m0) wfp_Nil)...
rewrite swap_name_involutive in Heq2.
rewrite <- (wfp_swap_chan_involutive m n (wfp_inst_Abs fp0 _)).
rewrite Heq1; rewrite <- Heq2.
apply RswCh. apply Hr´.
eapply wfp_fresh_chan_cswap in Hf3. simpl in Hf3; rewrite¬ swap_chan_involutive in Hf3.
eapply wfp_fresh_chan_cswap in Hf4. simpl in Hf4; rewrite¬ swap_chan_involutive in Hf4.
Qed.
Definition Normal_bisimulation_early (R : RelWfP) : Prop :=
(Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation_early R) ∧ (in_normal_relation_early R).
Definition NORbis_early p q : Prop :=
∃ R, (Normal_bisimulation_early R) ∧ (R p q).
Definition NORbisC_early (p q : wfprocess) : Prop :=
closed_process p ∧ closed_process q ∧ NORbis_early p q.
Notation "p e≈NOR q" := (NORbisC_early p q) (at level 60).
Lemma NORbisC_eNORbisC : ∀ p q, p ≈NOR q ↔ p e≈NOR q.
Proof.
introv; splits; introv Hbis;
destruct Hbis as (Hcp & Hcq & (R & (Hs & Htau & Ho & Hi) & Hr));
[ | rewrite NORbis_NORbis_ex; rewrite NORbisC_ex_NORbisC_ex_ex];
splits*; ∃ R; repeat splits*; clear dependent p; clear dependent q;
introv Hr Ht.
+ introv Hfmp Hfmq Hfxp Hfxq.
specializes Ho Hr Ht.
destruct Ho as (q´ & q´´ & Htq & Hbis). ∃ q´ q´´; splits×.
applys× Hbis.
- lets Hgv : GV_trans_out Ht.
intros Hin; apply Hfxp.
rewrite Hgv; rewrite¬ in_union.
- lets Hgv : GV_trans_out Htq.
intros Hin; apply Hfxq.
rewrite Hgv; rewrite¬ in_union.
+ introv Hfp Hfq.
specializes Hi Hr Ht.
destruct Hi as (fq & Htq & Hbis). ∃ fq; splits×.
+ lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfm; destruct Hfm as (Hfmp & Hfmq).
lets (X & Hfx) : find_fresh (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfxp & Hfxq).
specializes Ho Hfxp Hfxq.
destruct Ho as (q´ & q´´ & Htq & Hbis).
∃ q´ q´´; splits×. ∃ m X; splits×.
- lets Hgv : GV_trans_out Ht.
intros Hin; apply Hfxp.
rewrite Hgv; rewrite¬ in_union.
- lets Hgv : GV_trans_out Htq.
intros Hin; apply Hfxq.
rewrite Hgv; rewrite¬ in_union.
+ lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfm; destruct Hfm as (Hfmp & Hfmq).
specializes Hi Hfmp Hfmq.
destruct Hi as (fq & Htq & Hbis).
∃ fq; splits×.
Qed.