Library HOC14IObis
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 HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC12Guarded.
Require Import HOC13Bisimulations.
Require Import Relations.
Inductive R_refl : binary wfprocess :=
| Rrefl : ∀ p, R_refl p p.
Hint Resolve Rrefl.
Lemma IObis_refl : Reflexive IObis.
Proof.
intros p. ∃ R_refl. split¬.
clear p. unfolds. splits.
unfold Symmetric. introv Hr. inverts Hr. constructor.
unfold in_relation. introv Hr Ht. inverts Hr. ∃¬ fp.
unfold out_relation. introv Hr Ht. inverts Hr. ∃ p´ p´´. splits¬.
unfold var_relation. introv Hr Ht. inverts Hr. ∃ p´. splits¬.
Qed.
Lemma IObis_sym : Symmetric IObis.
Proof.
introv H. inversion H as (R & ((Hs & Hi & Ho & Hv) & Hr));
∃ R; repeat splits×.
Qed.
Lemma IObis_in : in_relation IObis.
Proof.
introv Hio; introv Ht. destruct Hio as (R & HB & HR). inversion HB as (_ & HI & _).
specializes HI (>> p q HR a fp); specialize (HI Ht).
destruct HI as (q´ & H´ & Hr). ∃ q´; splits¬.
introv Hf1 Hf2. ∃ R. splits×.
Qed.
Lemma IObis_out : out_relation IObis.
Proof.
introv Hio; introv Ht. destruct Hio as (R & HB & HR). inversion HB as (_ & _ & HO & _).
specializes HO (>> p q HR a p´ p´´ Ht).
destruct HO as (q´ & q´´ & Hq).
∃ q´ q´´. splits*; ∃× R.
Qed.
Lemma IObis_var : var_relation IObis.
Proof.
introv Hio; introv Ht. destruct Hio as (R & HB & HR). inversion HB as (_ & _ & _ & HV).
unfolds var_relation. specializes HV (>> p q HR X p´ Ht).
destruct HV as (q´ & Hq). ∃ q´. splits*; ∃× R.
Qed.
Theorem sizeX_IObis : ∀ X p q,
p ≈ q → sizeX X p = sizeX X q.
Proof.
intro X. induction p using (measure_induction wfp_size). introv Hio.
remember (sizeX X p) as sp. destruct sp.
remember (sizeX X q) as sq. destruct¬ sq.
assert (Hin: sizeX X q > 0) by nat_math.
apply sizeX_GV in Hin. eapply trans_GV in Hin.
destruct Hin as [[q´ Hq] |[[a [fq Hq]] |[a [q´ [q´´ Hq]]]]]; apply IObis_sym in Hio.
lets (p´ & Hp & Hio´): (IObis_var q p Hio X q´ Hq). apply sizeX_remove in Hp. nat_math.
lets (fp & Hp & Hio´): (IObis_in q p Hio a fq Hq).
lets (Z & Hex2): (find_fresh ((proc p)::(proc q)::(Gvar X)::nil)). rewrite Forall_to_conj_3 in Hex2.
destruct Hex2 as (Hf1 & Hf2 & Hneq). rewrite gfresh_gvar in Hneq.
apply not_eq_sym in Hneq.
lets Hsp: (>> sizeX_in a X p (wfp_Gvar Z) fp).
lets Hsq: (>> sizeX_in a X q (wfp_Gvar Z) fq).
etransitivity. eassumption.
etransitivity. apply¬ Hsp. simpl. cases_if¬.
etransitivity. apply H with (q := wfp_inst_Abs fq (wfp_Gvar Z))...
unfolds wfp_size; simpls.
lets Hp´ : Hp; apply (size_in a p (wfp_Gvar Z) fp) in Hp´; simpl in Hp´. nat_math. simpls¬.
apply IObis_sym. apply¬ Hio´.
etransitivity. symmetry. applys¬ Hsq. simpl. cases_if¬. auto.
lets (p´ & p´´ & Hp & Hio´ & Hio´´): (>> IObis_out q p Hio a q´ q´´ Hq).
lets Hsp: (>> sizeX_out a X p p´ p´´ Hp).
lets Hsq: (>> sizeX_out a X q q´ q´´ Hq).
etransitivity. eassumption.
etransitivity. apply Hsp.
transitivity (sizeX X q´ + sizeX X q´´).
fequals.
apply H.
unfolds wfp_size. apply size_out in Hp. rewrite Hp. nat_math.
apply¬ IObis_sym.
apply H.
unfolds wfp_size. apply size_out in Hp. rewrite Hp. nat_math.
apply¬ IObis_sym.
rewrite¬ Heqsq.
assert (Hin: sizeX X p > 0).
nat_math.
apply sizeX_GV in Hin. eapply trans_GV in Hin.
rewrite Heqsp. destruct Hin as [[p´ Hp] |[[a [fp Hp]] |[a [p´ [p´´ Hp]]]]].
lets (q´ & Hq & Hio´): (>> IObis_var p q Hio X p´ Hp).
lets Hsp: (>> sizeX_remove X p p´ Hp).
lets Hsq: (>> sizeX_remove X q q´ Hq).
rewrite Hsp, Hsq. fequals. applys¬ H.
unfold wfp_size.
apply size_remove in Hp. nat_math.
lets (fq & Hq & Hio´): (IObis_in p q Hio a fp Hp).
lets (Z & Hex): (>> find_fresh ((proc p)::(proc q)::(Gvar X)::nil)). rewrite Forall_to_conj_3 in Hex.
destruct Hex as (Hf1 & Hf2 & Hneq). rewrite gfresh_gvar in Hneq.
lets Hsp: (>> sizeX_in a X p (wfp_Gvar Z) fp).
lets Hsq: (>> sizeX_in a X q (wfp_Gvar Z) fq).
etransitivity. apply¬ Hsp. simpl. cases_if¬.
symmetry. etransitivity. apply¬ Hsq. simpl. cases_if¬.
symmetry.
apply¬ H.
unfolds wfp_size; simpl.
lets Hp´ : Hp; apply size_in with (m:=(wfp_Gvar Z)) in Hp´. nat_math. auto.
lets (q´ & q´´ & Hq & Hio´ & Hio´´): (>> IObis_out p q Hio a p´ p´´ Hp).
lets Hsp: (>> sizeX_out a X p p´ p´´ Hp).
lets Hsq: (>> sizeX_out a X q q´ q´´ Hq).
etransitivity. eassumption.
symmetry. etransitivity. eassumption. symmetry.
fequals; apply¬ H; unfolds wfp_size; apply size_out in Hp; nat_math.
Qed.
Lemma gfresh_IObis : ∀ X p q,
p≈q → X#p → X#q.
Proof.
introv Hio Hf.
apply sizeX_gfresh. apply sizeX_gfresh in Hf.
rewrite <- Hf. symmetry. apply¬ sizeX_IObis.
Qed.
Inductive R_trans : binary wfprocess :=
| Rtrans : ∀ p q r, p≈q → q≈r → R_trans p r.
Hint Resolve Rtrans.
Lemma IObis_trans : Transitive IObis.
Proof.
intros p q r Hio1 Hio2. ∃ R_trans. split×.
clear p q r Hio1 Hio2. unfold IO_bisimulation. splits.
introv Hr. inverts Hr. econstructor.
applys× IObis_sym. applys× IObis_sym.
introv Hr Ht; inverts Hr.
lets (fq0 & Ht2 & Hq0): (IObis_in p q0 H a fp Ht).
lets (fq & Htq & Hq): (IObis_in q0 q H0 a fq0 Ht2).
∃ fq; splits¬.
introv Hf1 Hf2.
econstructor; [apply¬ Hq0 | apply ¬Hq];
apply¬ (gfresh_IObis X q q0); applys¬ IObis_sym.
introv Hr; introv Ht. inverts Hr.
lets (q0´ & q0´´ & Ht2 & Hq0): (>> IObis_out p q0 H a p´ p´´ Ht).
lets (q´ & q´´ & Hq): (>> IObis_out q0 q H0 a q0´ q0´´ Ht2).
∃ q´ q´´. splits×.
introv Hr; introv Ht. inverts Hr.
lets (q0´ & Ht2 & Hq0): (IObis_var p q0 H X p´ Ht).
lets (q´ & Hq): (>> IObis_var q0 q H0 X q0´ Ht2).
∃ q´. split×.
Qed.
Instance IObis_is_eq_rel : Equivalence IObis.
Proof.
split. apply IObis_refl. apply IObis_sym. apply IObis_trans.
Qed.
Hint Resolve IObis_refl IObis_sym IObis_trans IObis_is_eq_rel.
Lemma R_IObis_up_to_up_to_R_IObis : ∀ Re R, Transitive Re → IO_bisimulation Re → IO_bisimulation_up_to Re R → IO_bisimulation (up_to Re R).
Proof.
introv HTrRe HRe HR.
inversion HRe as (HRe1 & HRe2 & HRe3 & HRe4).
destruct HR as (HR1 & HR2 & HR3 & HR4). splits.
introv Hr. inverts Hr. destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
constructor. ∃× q1 p1.
introv Hr Ht; inverts Hr.
destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
generalize (HRe2 p p1 Hre1 a fp Ht); intro HRe2´; destruct HRe2´ as (fp1 & Ht1 & Hre1´).
specialize (HR2 p1 q1 Hr1 a fp1 Ht1). destruct HR2 as (fq1 & Ht2 & Hr2).
specialize (HRe2 q1 q Hre2 a fq1 Ht2). destruct HRe2 as (fq & Ht3 & Hre2´).
∃ fq; splits¬.
introv Hf1 Hf2; constructor.
assert (Hf1´: X # p1). applys¬ (gfresh_IObis X p). ∃ Re. splits¬.
assert (Hf2´: X # q1). applys¬ (gfresh_IObis X q). ∃ Re. splits¬.
specializes Hr2 X Hf1´ Hf2´. inverts Hr2. destruct H as (p1´ & q1´ & Hre1´´ & Hre2´´& Hr1´).
∃ p1´ q1´. split×.
introv Hr; introv Ht. inverts Hr. destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
forwards¬ HRe3´: HRe3 Hre1 Ht. destruct HRe3´ as (p1´ & p1´´ & Ht1 & Hre1´ & Hre1´´).
specializes HR3 Hr1 Ht1. destruct HR3 as (q1´ & q1´´ & Ht2 & Hr1´ & Hr1´´).
specializes HRe3 Hre2 Ht2. destruct HRe3 as (q´ & q´´ & Ht3 & Hre2´ & Hre2´´).
∃ q´ q´´. splits¬.
inverts Hr1´. destruct H as (p2´ & q2´ & Hre3 & Hre4 & Hr2).
constructor. ∃ p2´ q2´. splits×.
inverts Hr1´´. destruct H as (p2´´ & q2´´ & Hre3 & Hre4 & Hr2).
constructor. ∃ p2´´ q2´´. splits×.
introv Hr; introv Ht. inverts Hr. destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
forwards¬ HRe4´: HRe4 Hre1 Ht. destruct HRe4´ as (p1´ & Ht1 & Hre1´).
specializes HR4 Hr1 Ht1. destruct HR4 as (q1´ & Ht2 & Hre2´).
specializes HRe4 Hre2 Ht2. destruct HRe4 as (q´ & Ht3 & Hre3).
∃ q´. split¬.
inverts Hre2´. destruct H as (p3´ & q3´ & Hre10 & Hre11 & Hr10).
constructor. ∃ p3´ q3´. splits×.
Qed.
Lemma IObis_up_to_IObis : ∀ Re, Equivalence Re → IO_bisimulation Re →
∀ p q, (IObis_up_to Re p q ↔ IObis p q).
Proof.
introv HEqRe HRe. introv; split; intros Hio; destruct Hio as (R & HR & Hr).
∃ (up_to Re R). split.
applys× R_IObis_up_to_up_to_R_IObis.
applys× up_to_eq.
∃ R. split¬. clear p q Hr.
destruct HR as (HR1 & HR2 & HR3 & HR4). splits¬.
unfold in_relation in HR2.
introv Hr Ht. forwards¬ (fq & Ht´ & Hf): HR2 p q Hr a fp.
∃ fq; splits¬. introv Hf1 Hf2.
applys× up_to_eq.
introv Hr; introv Ht. forwards¬ (q´ & q´´ & Ht´ & Hr´): HR3 Hr Ht.
∃ q´ q´´. splits~; applys× up_to_eq.
introv Hr; introv Ht. forwards¬ (q´ & Ht´ & Hr´): HR4 Hr Ht.
∃ q´. split¬. applys× up_to_eq.
Qed.
Lemma IObis_up_to_cgr_IObis : ∀ p q, (IObis_up_to wfcgr p q ↔ IObis p q).
Proof.
apply IObis_up_to_IObis; auto with congr_bisim.
Qed.
Lemma IO_bisimulation_up_to_refl : ∀ R, IO_bisimulation R → IO_bisimulation_up_to R R.
Proof.
introv (Hs & Hin & Hout & Hvar).
splits¬.
introv Hr Ht.
specialize (Hin p q Hr _ _ Ht).
destruct Hin as (fq & H´ & Hq).
∃ fq; splits~; introv Hfp Hfq.
specializes¬ Hq Hfq.
constructor.
∃ (wfp_inst_Abs fq (wfp_Gvar X)).
∃× (wfp_inst_Abs fp (wfp_Gvar X)).
introv Hr Ht.
lets (q´ & q´´ & Htq & Hr´ & Hr´´) : Hout Hr Ht.
∃ q´ q´´; splits~; constructor.
∃× q´ p´.
∃× q´´ p´´.
introv Hr Ht.
lets (q´ & Htq & Hr´) : Hvar Hr Ht.
∃ q´; splits~; constructor.
∃¬ q´ p´.
Qed.
Lemma congr_IObis : ∀ (p q : wfprocess), p ≡* q → p ≈ q.
Proof.
introv Hc.
∃ wfcgr; auto with congr_bisim.
Qed.
Inductive R_swap : binary wfprocess :=
| Rswap : ∀ X Y p q, p ≈ q → R_swap (wfp_swap X Y p) (wfp_swap X Y q).
Hint Resolve Rswap.
Lemma R_swap_IObis : IO_bisimulation R_swap.
Proof.
assert (Haux : ∀ X Y Z, wfp_swap X Y (wfp_Gvar Z) = wfp_Gvar ({{X, Y}}Z)).
introv; rewrite_wfp_swap; unfold swap_gvar; repeat cases_if×.
splits.
unfold Symmetric. introv Hr. inverts¬ Hr.
introv Hr Ht; inverts Hr; inverts keep Ht; clear H1.
lets (fp0 & Ht2 & Hp) : wfp_trans_swap_in X Y Ht.
rewrite wfp_swap_involutive in Ht2.
lets (fq & Ht3 & Hq): (IObis_in p0 q0 H a fp0 Ht2).
lets (fq´ & Ht4 & Hq´): (wfp_trans_swap_in a X Y q0 fq Ht3).
∃ fq´. splits¬.
introv Hf0 Hf1.
rewrite <- wfp_swap_involutive with (X:=X) (Y:=Y) at 1.
rewrite <- wfp_swap_involutive with (p:=wfp_Gvar X1) (X:=X) (Y:=Y) at 2.
rewrite Hp; rewrite <- Hq´; simpl.
constructor.
repeat rewrite Haux.
apply¬ Hq; simpls;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf0;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf1;
rewrite swap_involutive in *; auto.
lets (fp0 & Ht2 & Hp) : (>> wfp_trans_swap_in a X Y (wfp_swap X Y p0) fp Ht).
rewrite wfp_swap_involutive in Ht2.
lets (fq & Ht3 & Hq): (IObis_in p0 q0 H a fp0 Ht2).
lets (fq´ & Ht4 & Hq´): (wfp_trans_swap_in a X Y q0 fq Ht3).
∃ fq´; splits¬.
introv Hf0 Hf1.
rewrite <- wfp_swap_involutive with (X:=X) (Y:=Y) at 1.
rewrite <- wfp_swap_involutive with (p:=wfp_Gvar X0) (X:=X) (Y:=Y) at 2.
rewrite Hp; rewrite <- Hq´; simpl.
constructor.
repeat rewrite Haux.
apply¬ Hq; simpls;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf0;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf1;
rewrite swap_involutive in *; auto.
lets (fp0 & Ht2 & Hp) : (>> wfp_trans_swap_in a X Y (wfp_swap X Y p0) fp Ht).
rewrite wfp_swap_involutive in Ht2.
lets (fq & Ht3 & Hq): (IObis_in p0 q0 H a fp0 Ht2).
lets (fq´ & Ht4 & Hq´): (wfp_trans_swap_in a X Y q0 fq Ht3).
∃ fq´; splits¬.
introv Hf0 Hf1.
rewrite <- wfp_swap_involutive with (X:=X) (Y:=Y) at 1.
rewrite <- wfp_swap_involutive with (p:=wfp_Gvar X0) (X:=X) (Y:=Y) at 2.
rewrite Hp; rewrite <- Hq´; simpl.
constructor.
repeat rewrite Haux.
apply¬ Hq; simpls;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf0;
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hf1;
rewrite swap_involutive in *; auto.
introv Hr Ht; inverts Hr.
lets Ht2: (wfp_trans_swap_out a X Y (wfp_swap X Y p0) p´ p´´ Ht).
rewrite wfp_swap_involutive in Ht2.
lets (q´ & q´´ & Hq) : (IObis_out p0 q0 H a (wfp_swap X Y p´) (wfp_swap X Y p´´) Ht2).
∃ (wfp_swap X Y q´) (wfp_swap X Y q´´). splits¬.
applys× wfp_trans_swap_out.
rewrite <- (wfp_swap_involutive X Y p´). constructor×.
rewrite <- (wfp_swap_involutive X Y p´´); constructor×.
introv Hr; introv Ht. inverts Hr.
lets Ht2: (wfp_trans_swap_rem X0 Y X (wfp_swap X0 Y p0) p´ Ht).
rewrite wfp_swap_involutive in Ht2.
lets (q´ & Hq): (IObis_var p0 q0 H ({{X0, Y}}X) (wfp_swap X0 Y p´) Ht2).
∃ (wfp_swap X0 Y q´). splits¬.
rewrite <- swap_gvar_involutive with (X:=X0) (X´:=Y) (Y:=X).
applys× wfp_trans_swap_rem.
rewrite <- (wfp_swap_involutive X0 Y p´); constructor×.
Qed.
Lemma IObis_swap : ∀ X Y p q,
p ≈ q → (wfp_swap X Y p) ≈ (wfp_swap X Y q).
Proof.
introv Hio. unfolds. ∃ R_swap. split¬. apply R_swap_IObis.
Qed.
Lemma IObis_size_unguardedX : ∀ X p q,
p≈q → size_unguardedX X p = size_unguardedX X q.
Proof.
introv Hio.
remember (size_unguardedX X p).
gen p q. induction n; intros.
tests : (guarded X q).
rewrite guarded_size_unguardedX in C; nat_math.
apply wfp_not_guarded_unguarded in C.
destruct C as [q´ Htq]. symmetry in Hio.
lets (p´ & Ht´ & Hr´) : IObis_var Hio Htq.
apply size_unguardedX_remove in Ht´; nat_math.
assert (Hng: ¬ guarded X p).
introv Hg. apply guarded_size_unguardedX in Hg. nat_math.
apply wfp_not_guarded_unguarded in Hng.
destruct Hng as [p´ Htp].
lets (q´ & Ht´ & Hr´) : IObis_var Hio Htp.
lets : Ht´.
apply size_unguardedX_remove in H. apply size_unguardedX_remove in Ht´.
apply size_unguardedX_remove in Htp.
rewrite Ht´. fequals. eapply IHn; try eassumption. nat_math.
Qed.
Lemma wfp_guarded_IObis : ∀ X p q,
p≈q → ∃ (p´ : wfprocess), ∃ (q´ : wfprocess),
(guarded X p´) ∧ (p ≡* (wfp_Par p´ (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X p)))) ∧
(guarded X q´) ∧ (q ≡* (wfp_Par q´ (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X p)))) ∧
p´≈q´.
Proof with (automate; try solve [applys× t_step]).
introv Hio.
remember (size_unguardedX X p).
gen p q. induction n; introv Hs Hio.
∃ p q. splits... apply guarded_size_unguardedX. nat_math.
apply guarded_size_unguardedX. erewrite IObis_size_unguardedX; eauto.
assert (Hngu: ¬ guarded X p). intros Hgu.
apply guarded_size_unguardedX in Hgu. nat_math.
apply wfp_not_guarded_unguarded in Hngu.
destruct Hngu as [p´ Hru].
specialize (IObis_var p q Hio X p´ Hru). intros Hex.
destruct Hex as [q´ [Hru2 Hio2]].
specializes IHn Hio2. apply size_unguardedX_remove in Hru. nat_math.
destruct IHn as [p´´ [q´´ [Hgu1 [Hc1 [Hgu2 [Hc2 Hio3]]]]]].
∃ p´´ q´´. splits...
apply wfp_remove_congr in Hru.
etransitivity. eassumption.
assert (wfp_Gvar X ≡* wfp_Gvar X)...
apply wfcgr_par with (p2 := wfp_Gvar X) (q2 := wfp_Gvar X) in Hc1...
etransitivity. eassumption.
etransitivity. constructor. apply WfCgrPar_assoc2.
apply wfcgr_par...
apply wfp_remove_congr in Hru2.
etransitivity. eassumption.
assert (wfp_Gvar X ≡* wfp_Gvar X)...
apply wfcgr_par with (p2 := wfp_Gvar X) (q2 := wfp_Gvar X) in Hc2...
etransitivity. eassumption.
etransitivity. constructor. apply WfCgrPar_assoc2.
apply wfcgr_par...
Qed.
Lemma wfp_sizeP_S_tr : ∀ (p : wfprocess),
wfp_sizeP p > 0 ↔ (∃ (X : var) (p´ : wfprocess), {{p--LabRem X->>(AP p´)}})
∨ (∃ a, ∃ f, {{p--LabIn a->>(AA f)}})
∨ (∃ a, ∃ (p´ : wfprocess), ∃ (p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}}).
Proof with automate.
introv; split.
induction p using (wfp_ind); introv Ht.
branch 3. ∃ a wfp_Nil p...
branch 2. ∃ a. eexists...
branch 1. ∃ X wfp_Nil...
assert (Hsize : wfp_sizeP p1 > 0 ∨ wfp_sizeP p2 > 0)...
clear Ht; inverts Hsize; [specializes IHp1 H; clear IHp2; inverts IHp1 | specializes IHp2 H; clear IHp1; inverts IHp2].
destruct H0 as (X & p´ & Ht).
branch 1. ∃ X (wfp_Par p´ p2)...
inverts H0.
destruct H1 as (a & fp & Ht).
branch 2. ∃ a (AbsPar1 fp p2)...
destruct H1 as (a & p´ & p´´ & Ht).
branch 3. ∃ a (wfp_Par p´ p2) p´´...
destruct H0 as (X & p´ & Ht).
branch 1. ∃ X (wfp_Par p1 p´)...
inverts H0.
destruct H1 as (a & fp & Ht).
branch 2. ∃ a (AbsPar2 p1 fp)...
destruct H1 as (a & p´ & p´´ & Ht).
branch 3. ∃ a (wfp_Par p1 p´) p´´...
unfold wfp_sizeP in Ht; simpls; nat_math.
introv Ht; unfolds wfp_sizeP; inverts Ht.
destruct H as (X & p´ & Htp).
apply sizeP_remove in Htp; nat_math.
inverts H.
destruct H0 as (a & fp & Htp).
lets (X & _) : find_fresh (@nil process).
eapply sizeP_in with (m := (wfp_Gvar X)) in Htp; jauto; nat_math.
destruct H0 as (a & p´ & p´´ & Htp).
eapply sizeP_out in Htp; nat_math.
Qed.
Lemma IObis_sizeP_eq : ∀ p q, p ≈ q → wfp_sizeP p = wfp_sizeP q.
Proof with automate.
induction p using (measure_induction wfp_sizeP); introv (R & (Hsym & Hin & Hout & Hvar) & Hr).
destruct_wf p.
assert (Htp : {{wfp_Send a p0 -- LabOut a p0 ->> AP wfp_Nil}}) by auto.
lets Haux : Hout; specializes Haux Hr Htp.
destruct Haux as (q´ & q´´ & Htq & Hr´ & Hr´´).
assert (Hbis1 : wfp_Nil ≈ q´) by (∃ R; repeat splits*).
assert (Hbis2 : p0 ≈ q´´) by (∃ R; repeat splits*).
apply H in Hbis1...
apply H in Hbis2...
lets Hsize1 : sizeP_out Htp; lets Hsize2 : sizeP_out Htq...
assert (Htp : {{wfp_Abs a X p0 -- LabIn a ->> AA (AbsPure X p0)}}) by auto.
lets Haux : Hin; specializes Haux Hr. specialize (Haux _ _ Htp).
destruct Haux as (fq & Htq & Hr´).
lets Hf : find_fresh (proc (wfp_Abs a X p0) :: (proc q) :: nil).
destruct Hf as (Y & Hfy); rewrite Forall_to_conj_2 in Hfy; destruct Hfy as (Hfy1 & Hfy2).
specializes Hr´ Hfy1 Hfy2.
assert (Haux : sizeP (wfp_Gvar Y) = 1) by auto.
lets Hsize1 : sizeP_in Htp. apply Haux.
lets Hsize2 : sizeP_in Htq. apply Haux.
assert (Hbis1 : (wfp_inst_Abs (AbsPure X p0) (wfp_Gvar Y))
≈ (wfp_inst_Abs fq (wfp_Gvar Y))) by (∃ R; repeat splits*).
apply H in Hbis1; simpls...
assert (Htp : {{wfp_Gvar X -- LabRem X ->> AP wfp_Nil}}) by auto.
lets Haux : Hvar; specializes Haux Hr Htp.
destruct Haux as (q´ & Htq & Hr´).
assert (Hbis1 : wfp_Nil ≈ q´) by (∃ R; repeat splits*).
apply H in Hbis1...
lets Hsize1 : sizeP_remove Htp; lets Hsize2 : sizeP_remove Htq...
elim (zerop (wfp_sizeP (wfp_Par p1 p2))); auto; intro Hcmp.
rewrite Hcmp; symmetry; symmetry in Hr.
assert (Hntr : ¬ (wfp_sizeP (wfp_Par p1 p2) > 0)) by nat_math; clear Hcmp.
rewrite wfp_sizeP_S_tr in Hntr; rew_logic in *; destruct Hntr as (Hntvar & Hntin & Hntout).
elim (zerop (wfp_sizeP q)); auto; intro Hcmpq.
assert (Ht : wfp_sizeP q > 0) by nat_math; clear Hcmpq.
apply wfp_sizeP_S_tr in Ht.
elim Ht; clear Ht; intro Ht.
destruct Ht as (X & q´ & Ht).
specializes Hvar Hr Ht.
destruct Hvar as (p´ & Htp & _).
specialize (Hntvar X); rew_logic in Hntvar; specialize (Hntvar p´); false¬.
elim Ht; clear Ht; intro Ht.
destruct Ht as (a & fq & Ht).
specialize (Hin _ _ Hr _ _ Ht).
destruct Hin as (fp´ & Htp & _).
specialize (Hntin a); rew_logic in Hntin; specialize (Hntin fp´); false¬.
destruct Ht as (a & q´ & q´´ & Ht).
specializes Hout Hr Ht.
destruct Hout as (p´ & p´´ & Htp & _).
specialize (Hntout a); rew_logic in Hntout; specialize (Hntout p´); rew_logic in Hntout;
specialize (Hntout p´´); false¬.
assert (Ht : wfp_sizeP (wfp_Par p1 p2) > 0) by nat_math; clear Hcmp.
remember (wfp_Par p1 p2) as p; clear Heqp.
apply wfp_sizeP_S_tr in Ht.
elim Ht; clear Ht; intro Ht.
destruct Ht as (X & p´ & Htp).
lets Haux : Hvar; specializes Haux Hr Htp.
destruct Haux as (q´ & Htq & Hr´).
assert (Hbis1 : p´ ≈ q´) by (∃ R; repeat splits*).
apply H in Hbis1...
lets Hsize1 : sizeP_remove Htp; lets Hsize2 : sizeP_remove Htq...
apply sizeP_remove in Htp...
elim Ht; clear Ht; intro Ht.
destruct Ht as (a & fp & Htp).
lets Haux : Hin; specialize (Haux _ _ Hr _ _ Htp).
destruct Haux as (fq & Htq & Hr´).
lets Hf : find_fresh (proc p :: proc q :: nil).
destruct Hf as (X & Hfx); rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfx1 & Hfx2).
specializes Hr´ Hfx1 Hfx2.
assert (Haux : sizeP (wfp_Gvar X) = 1) by auto.
lets Hsize1 : sizeP_in Htp. apply Haux.
lets Hsize2 : sizeP_in Htq. apply Haux.
assert (Hbis1 : (wfp_inst_Abs fp (wfp_Gvar X))
≈ (wfp_inst_Abs fq (wfp_Gvar X))) by (∃ R; repeat splits*).
apply H in Hbis1...
destruct Ht as (a & p´ & p´´ & Htp).
lets Haux : Hout; specializes Haux Hr Htp.
destruct Haux as (q´ & q´´ & Htq & Hr´ & Hr´´).
assert (Hbis1 : p´ ≈ q´) by (∃ R; repeat splits*).
assert (Hbis2 : p´´ ≈ q´´) by (∃ R; repeat splits*).
apply H in Hbis1; apply H in Hbis2;
lets Hsize1 : sizeP_out Htp; lets Hsize2 : sizeP_out Htq...
clear H.
symmetry; symmetry in Hr.
elim (zerop (wfp_sizeP q)); auto; intro Hcmp.
assert (Ht : wfp_sizeP q > 0)... clear Hcmp.
apply wfp_sizeP_S_tr in Ht.
elim Ht; clear Ht; intro Ht.
destruct Ht as (X & q´ & Ht).
specializes Hvar Hr Ht.
destruct Hvar as (p´ & Htp & _); inverts Htp.
elim Ht; clear Ht; intro Ht.
destruct Ht as (a & fq & Ht).
specialize (Hin _ _ Hr _ _ Ht).
destruct Hin as (fp & Htp & _); inverts Htp.
destruct Ht as (a & q´ & q´´ & Ht).
specializes Hout Hr Ht.
destruct Hout as (p´ & p´´ & Htp & _); inverts Htp.
Qed.
Definition in_relation_ex (R:binary wfprocess) : Prop :=
∀ p q, (R p q) → ∀ a fp, {{p--LabIn a->>(AA fp)}} →
∃ fq, {{q--LabIn a->>(AA fq)}} ∧ ∃ X, X#p ∧ X#q ∧ (R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X))).
Definition in_relation_ex_up_to (Re R:binary wfprocess) : Prop :=
∀ p q, (R p q) → ∀ a fp, {{p--LabIn a->>(AA fp)}} →
∃ fq, {{q--LabIn a->>(AA fq)}} ∧ ∃ X, X#p ∧ X#q ∧ up_to Re R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).
Definition IO_bisimulation_ex (R:binary wfprocess) : Prop :=
(Symmetric R) ∧ (in_relation_ex R) ∧ (out_relation R) ∧ (var_relation R).
Definition IO_bisimulation_ex_up_to (Re R:binary wfprocess) : Prop :=
(Symmetric R) ∧ (in_relation_ex_up_to Re R) ∧ (out_relation_up_to Re R) ∧ (var_relation_up_to Re R).
Definition IO_bisimulation_full (R:binary wfprocess) : Prop :=
(Symmetric R) ∧ (in_full_relation R) ∧ (out_relation R) ∧ (var_relation R).
Definition IObis_ex p q : Prop :=
∃ R, (IO_bisimulation_ex R) ∧ (R p q).
Definition IObis_ex_up_to Re p q : Prop :=
∃ R, (IO_bisimulation_ex_up_to Re R) ∧ (R p q).
Definition IObis_full p q : Prop :=
∃ R, (IO_bisimulation_full R) ∧ (R p q).
Lemma in_forall_exists : ∀ R, in_relation R → in_relation_ex R.
Proof with automate.
introv Hi Hr Ht. specializes Hi Hr Ht. destruct Hi as (fq & Ht´ & Hr´).
∃ fq; splits...
lets (Z & Hf): find_fresh ((proc p):: (proc q)::nil). rewrite× Forall_to_conj_2 in Hf.
Qed.
Lemma in_full_forall : ∀ R, in_full_relation R → in_relation R.
Proof with automate.
introv Hi Hr Ht. specializes Hi Hr Ht. destruct Hi as (fq & Ht´ & Hr´).
∃ fq; splits...
Qed.
Definition swap_relation (R: binary wfprocess) : Prop := ∀ X Y p q,
R p q → R (wfp_swap X Y p) (wfp_swap X Y q).
Lemma IObisim_ex_IObisim_when_swap : ∀ (R : binary wfprocess), swap_relation R → (IO_bisimulation_ex R ↔ IO_bisimulation R).
Proof with automate.
introv Hyp; split; introv (Hs & Hi & Ho & Hv); splits¬.
lets Haux : wfp_trans_swap_inst_Abs_eq.
Focus 2.
introv Hr Ht.
lets (X & Hfx) : find_fresh (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfx1 & Hfx2).
lets (fq & H´ & Hrest) : (Hi _ _ Hr _ _ Ht).
∃ fq; splits...
introv Hr Ht.
lets (fq & Ht´ & X & Hfxp & Hfxq & Hrs) : Hi Hr Ht.
∃ fq; splits~; intros Y Hfyp Hfyq.
specializes Hyp X Y Hrs.
replace (wfp_inst_Abs fp (wfp_Gvar Y)) with (wfp_swap X Y (wfp_inst_Abs fp (wfp_Gvar X)));
replace (wfp_inst_Abs fq (wfp_Gvar Y)) with (wfp_swap X Y (wfp_inst_Abs fq (wfp_Gvar X)))...
Qed.
Inductive R_swap2 R : binary wfprocess :=
| Rswr : ∀ p q, R p q → R_swap2 R p q
| Rsw : ∀ X Y p q, R_swap2 R p q → R_swap2 R (wfp_swap X Y p) (wfp_swap X Y q).
Hint Resolve Rswr Rsw.
Lemma IObis_IObis_ex : ∀ p q, IObis p q ↔ IObis_ex p q.
Proof.
introv. split; introv H.
∃ IObis. split¬.
splits¬.
introv Hio Ht. lets (fq & Htq & Hio2): (IObis_in p0 q0 Hio a fp Ht).
∃ fq; splits¬.
lets (X & Hf): find_fresh ((proc p0)::(proc q0)::nil). rewrite Forall_to_conj_2 in Hf.
destruct Hf.
∃¬ X.
apply IObis_out.
apply IObis_var.
destruct H as (R & HR & Hr). ∃ (R_swap2 R). split¬.
rewrite <- IObisim_ex_IObisim_when_swap. splits.
Focus 5. introv Hr´; apply¬ Rsw.
introv Hr´. induction Hr´.
constructor. apply¬ HR.
apply¬ Rsw.
introv Hr´. induction Hr´; introv Ht.
destruct HR as (HR1 & HR2 & HR3). eapply HR2 in H; auto.
edestruct (H a fp Ht) as (fq & Htq & Z & Hf1 & Hf2 & Hrq).
∃ fq; splits¬. ∃× Z.
rename fp into fps.
forwards (fp0 & Ht´ & Heq1): wfp_trans_swap_in a X Y Ht.
rewrite wfp_swap_involutive in Ht´.
specialize (IHHr´ a fp0 Ht´). destruct IHHr´ as (fq & Htq & Hr´´).
forwards (fqs & Htq´ & Heq2): wfp_trans_swap_in a X Y Htq.
∃ fqs. splits¬.
destruct Hr´´ as (Z & Hzp & Hzq & Hrz).
∃ ({{X, Y}}Z); splits; simpls.
apply¬ gfresh_swap_inv. apply¬ gfresh_swap_inv.
assert (wfp_Gvar ({{X, Y}}Z) = wfp_swap X Y (wfp_Gvar Z)).
rewrite wfp_eq_swap_gvar; unfold swap_gvar; repeat cases_if×.
repeat rewrite H. rewrite <- Heq2.
rewrite <- (wfp_swap_involutive X Y (wfp_inst_Abs fps (wfp_swap X Y (wfp_Gvar Z)))).
apply Rsw. rewrite Heq1. rewrite¬ wfp_swap_involutive.
introv Hr´. induction Hr´; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4). eapply HR3 in H; auto.
edestruct H as (q´ & q´´ & Htq & Hr1 & Hr2); try eassumption.
∃ q´ q´´. splits¬.
forwards Ht´: wfp_trans_swap_out X Y Ht; simpl in Ht´.
rewrite wfp_swap_involutive in Ht´.
edestruct (IHHr´ a (wfp_swap X Y p´) (wfp_swap X Y p´´)) as (q´ & q´´ & Htq & Hr1 & Hr2). assumption.
∃ (wfp_swap X Y q´) (wfp_swap X Y q´´). splits.
applys¬ wfp_trans_swap_out.
erewrite <- wfp_swap_involutive at 1. apply¬ Rsw.
erewrite <- wfp_swap_involutive at 1. apply¬ Rsw.
introv Hr´. induction Hr´; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4). eapply HR4 in H; auto. edestruct H as (q´ & Htq & Hr´´).
eassumption.
∃ q´. split¬.
forwards Ht´: wfp_trans_swap_rem X Y Ht.
simpl in Ht´; rewrite wfp_swap_involutive in Ht´.
edestruct (IHHr´ _ (wfp_swap X Y p´) Ht´) as (q´ & Htq & Hr´´).
∃ (wfp_swap X Y q´). split.
erewrite <- swap_gvar_involutive with (Y:=X0). apply¬ wfp_trans_swap_rem.
erewrite <- wfp_swap_involutive at 1. apply¬ Rsw.
Qed.
Lemma in_up_to_forall_exists : ∀ Re,
∀ R, in_relation_up_to Re R → in_relation_ex_up_to Re R.
Proof.
introv H; introv Hr Ht. forwards¬ (fq & Ht´ & Hr´): (H p q Hr a fp Ht). ∃ fq; splits¬.
lets (Z & Hf): (find_fresh ((proc p)::(proc q)::nil)). rewrite× Forall_to_conj_2 in Hf.
Qed.
Lemma IObisim_ex_up_to_IObisim_up_to_when_swap : ∀ Re (R : binary wfprocess), swap_relation Re → swap_relation R → (IO_bisimulation_ex_up_to Re R ↔ IO_bisimulation_up_to Re R).
Proof with automate.
introv HypRe HypR; split; introv (Hs & Hi & Ho & Hv); splits¬.
lets Haux : wfp_trans_swap_inst_Abs_eq.
Focus 2.
introv Hr Ht.
lets (X & Hfx) : find_fresh (proc p :: proc q :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfx1 & Hfx2).
lets (fq & H´ & Hrest) : (Hi _ _ Hr _ _ Ht).
∃ fq; splits...
introv Hr Ht.
lets (fq & Ht´ & X & Hfxp & Hfxq & Hrs) : Hi Hr Ht.
∃ fq; splits~; intros Y Hfyp Hfyq.
inverts Hrs as Hrs. destruct Hrs as (p´ & q´ & Hre1 & Hre2 & Hr1).
specializes HypR X Y Hr1.
constructor. ∃ (wfp_swap X Y p´) (wfp_swap X Y q´). splits~; clear dependent R.
apply (HypRe X Y) in Hre1. erewrite Haux in Hre1; try eassumption.
apply (HypRe X Y) in Hre2. erewrite Haux in Hre2; try eassumption.
Qed.
Lemma IObis_ex_up_to_IObis_up_to : ∀ Re, swap_relation Re →
∀ p q, IObis_ex_up_to Re p q ↔ IObis_up_to Re p q.
Proof with automate.
introv HSwRe. split; intros.
destruct H as (R & HR & HR´). ∃ (R_swap2 R). split¬.
rewrite¬ <- IObisim_ex_up_to_IObisim_up_to_when_swap.
destruct HR as (HR1 & HR2 & HR3 & HR4). splits.
introv Hr. induction Hr. constructor¬. apply¬ Rsw.
introv Hr´. induction Hr´; introv Ht.
eapply HR2 in H; auto.
edestruct (H a fp Ht) as (fq & Htq & Z & Hf1 & Hf2 & Hrq).
∃ fq; splits¬. ∃ Z; splits...
inverts Hrq as Hrq. destruct Hrq as (p´ & q´ & Hre1 & Hre2 & Hr1).
constructor. ∃ p´ q´; splits¬.
rename fp into fps.
forwards (fp0 & Ht´ & Heq1): wfp_trans_swap_in a X Y Ht.
rewrite wfp_swap_involutive in Ht´.
specialize (IHHr´ a fp0 Ht´). destruct IHHr´ as (fq & Htq & Hr´´).
forwards (fqs & Htq´ & Heq2): wfp_trans_swap_in a X Y Htq.
∃ fqs. splits¬.
destruct Hr´´ as (Z & Hzp & Hzq & Hrz).
∃ ({{X, Y}}Z); splits; simpls.
apply¬ gfresh_swap_inv. apply¬ gfresh_swap_inv.
inverts Hrz as Hrz. destruct Hrz as (p´ & q´ & Hre1 & Hre2 & Hr1).
assert (wfp_Gvar ({{X, Y}}Z) = wfp_swap X Y (wfp_Gvar Z)).
rewrite wfp_eq_swap_gvar; unfold swap_gvar; repeat cases_if×.
repeat rewrite H.
constructor. ∃ (wfp_swap X Y p´) (wfp_swap X Y q´); splits¬.
rewrite <- (wfp_swap_involutive X Y (wfp_inst_Abs fps (wfp_swap X Y (wfp_Gvar Z)))).
rewrite Heq1. rewrite wfp_swap_involutive...
rewrite <- Heq2...
introv Hr. induction Hr; introv Ht.
eapply HR3 in H; auto. edestruct H as (q´ & q´´ & Htq & Hr1 & Hr2).
eassumption.
∃ q´ q´´. splits¬.
inverts Hr1. destruct H0 as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ p1 q1. splits¬.
inverts Hr2. destruct H0 as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ p1 q1. splits¬.
lets Ht´: (wfp_trans_swap_out _ X Y _ _ _ Ht). simpl in Ht´; rewrite wfp_swap_involutive in Ht´.
edestruct (IHHr a (wfp_swap X Y p´) (wfp_swap X Y p´´)) as (q´ & q´´ & Htq & Hr1 & Hr2); simpls¬.
∃ (wfp_swap X Y q´) (wfp_swap X Y q´´). splits.
applys¬ wfp_trans_swap_out.
rewrite <- wfp_swap_involutive with (X:=X) (Y:=Y) at 1. inverts Hr1.
destruct H as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ (wfp_swap X Y p1) (wfp_swap X Y q1). splits¬.
inverts Hr2.
destruct H as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ (wfp_swap X Y p1) (wfp_swap X Y q1). splits¬.
erewrite <- wfp_swap_involutive at 1. apply¬ HSwRe.
introv Hr. induction Hr; introv Ht. eapply HR4 in H; auto.
edestruct H as (q´ & Htq & Hr). eassumption. ∃ q´. split¬.
inverts Hr. destruct H0 as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ p1 q1. split¬.
lets Ht´: (wfp_trans_swap_rem X Y _ _ _ Ht). simpl in Ht´; rewrite wfp_swap_involutive in Ht´.
edestruct (IHHr ({{X, Y}}X0) (wfp_swap X Y p´)) as (q´ & Htq & Hr´). eassumption.
∃ (wfp_swap X Y q´). split.
rewrite <- swap_gvar_involutive with (X:=X) (X´:=Y) (Y:=X0).
applys¬ wfp_trans_swap_rem.
inverts Hr´. destruct H as (p1 & q1 & Hc1 & Hc2 & Hr´´). constructor.
∃ (wfp_swap X Y p1) (wfp_swap X Y q1). splits¬.
rewrite <- wfp_swap_involutive with (X:=X) (Y:=Y) at 1. apply¬ HSwRe.
introv...
destruct H as (R & HR & Hr). ∃ R. split¬. clear p q Hr.
destruct HR as (HR1 & HR2 & HR3 & HR4). splits¬.
introv Hio Ht. forwards (fq & Ht2 & Hio2): (HR2 p q Hio a fp Ht).
∃ fq; splits¬.
lets (X & Hf): (find_fresh ((proc p)::(proc q)::nil)). rewrite Forall_to_conj_2 in Hf.
∃× X.
Qed.
Inductive R_send : binary wfprocess :=
| Rs : ∀ a p q, p≈q → (R_send (wfp_Send a p) (wfp_Send a q))
| Rsbis : ∀ p q, p≈q → (R_send p q)
| RsN : (R_send wfp_Nil wfp_Nil).
Hint Resolve Rs Rsbis RsN.
Lemma IObis_congr_send : ∀ a p q,
p≈q → (wfp_Send a p) ≈ (wfp_Send a q).
Proof with automate.
introv Hio. ∃ R_send. split¬.
clear; splits.
introv Hr. inverts¬ Hr.
introv Hr Ht. inverts Hr.
inverts Ht.
lets (fq & Hq´ & Hq): (IObis_in p q H a fp Ht). ∃ fq; splits¬.
inverts Ht.
introv Hr Ht. inverts Hr. inverts Ht...
lets (q´ & q´´ & Hq): (IObis_out p q H a p´ p´´ Ht). ∃ q´ q´´...
inverts Ht.
introv Hr; introv Ht. inverts Hr.
inverts Ht.
lets (q´ & Hq): (>> IObis_var p q H X p´ Ht). ∃ q´...
inverts Ht.
Qed.
Inductive R_abs : binary wfprocess :=
| Rabs : ∀ a X p q, p≈q → R_abs (wfp_Abs a X p) (wfp_Abs a X q)
| Rbis : ∀ p q, p≈q → R_abs p q.
Hint Resolve Rabs Rbis.
Lemma IObis_congr_abs : ∀ a X p q,
p≈q → (wfp_Abs a X p) ≈ (wfp_Abs a X q).
Proof with automate.
introv Hio. unfold IObis. ∃ R_abs. split¬.
clear. splits.
introv Hr. inverts¬ Hr.
introv Hr Ht. inverts Hr.
lets Heq : wfp_trans_in_chan_eq Ht; subst.
lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst;
∃ (AbsPure X q0); splits¬.
intros Y Hf0 Hf1; simpls; unfold Abs in *; rewrite gfresh_receive in ×.
tests Hneqxy : (X = Y).
repeat rewrite wfp_subst_gvar_idem...
repeat rewrite wfp_gfresh_subst_is_swap; try fresh_solve.
constructor. apply¬ IObis_swap.
destruct Hyp as (Z & Hneq & Hfz & Heq); subst.
intros Y Hf0 Hf1; simpls; unfold Abs in *; rewrite gfresh_receive in ×.
tests Hneqxy : (X = Y).
rewrite¬ <- wfp_subst_decomposition_g.
repeat rewrite wfp_subst_gvar_idem...
rewrite¬ <- wfp_subst_decomposition_g.
repeat rewrite wfp_gfresh_subst_is_swap; try fresh_solve.
constructor. apply¬ IObis_swap.
lets (fq & H´ & Hq) : IObis_in H Ht. ∃ fq...
introv Hr Ht. inverts Hr.
inverts Ht.
apply IObis_out in H; auto. specializes H a p´ p´´ Ht.
destruct H as (q´ & q´´ & Hq1 & Hq2 & Hq3). ∃ q´ q´´...
introv Hr Ht. inverts Hr.
inverts Ht.
apply IObis_var in H; auto. specializes H X p´ Ht.
destruct H as (q´ & Hq1 & Hq2). ∃ q´...
Qed.
Inductive R_par1 : binary wfprocess :=
| Rp1 : ∀ p q r, p≈q → (R_par1 (wfp_Par p r) (wfp_Par q r))
| Rp1refl : ∀ p q, p≈q → (R_par1 p q).
Hint Resolve Rp1 Rp1refl.
Lemma IObis_congr_par1 : ∀ p q r,
p ≈ q → (wfp_Par p r) ≈ (wfp_Par q r).
Proof with (automate; freshen_up).
introv Hio. ∃ R_par1; splits¬.
clear; splits.
unfold Symmetric. introv Hr. inverts× Hr.
introv Hr Ht; inverts Hr.
inverts Ht...
destruct ap; inverts H4.
lets (fq & H´ & Hq) : IObis_in H H3.
∃ (AbsPar1 fq r); splits...
introv Hf0 Hf1; simpls...
destruct aq; inverts H4.
∃ (AbsPar2 q0 a0); splits...
introv Hf0 Hf1; simpls...
lets (fq & H´ & Hq): IObis_in H Ht.
∃ fq; splits...
introv Hr Ht; inverts Hr.
inverts Ht...
destruct ap; inverts H4.
lets (q´ & q´´ & Hq) : IObis_out H H3.
∃ (wfp_Par q´ r) q´´; splits...
destruct aq; inverts H4.
∃ (wfp_Par q0 w) p´´. splits...
lets (q´ & q´´ & Hq): (IObis_out p q H a p´ p´´ Ht).
∃ q´ q´´. split×.
introv Hr Ht; inverts Hr.
inverts Ht...
destruct ap; inverts H4.
lets (q´ & Hq & Hio): IObis_var H H3.
∃ (wfp_Par q´ r). splits...
destruct aq; inverts H4.
∃ (wfp_Par q0 w). splits...
lets (q´ & Hq & Hio): (IObis_var p q H X p´ Ht).
∃ q´. split¬.
Qed.
Lemma IObis_congr_nil_l : ∀ p, p ≈ (wfp_Par p wfp_Nil).
Proof.
introv; apply congr_IObis. apply wfcgr_nil_l.
Qed.
Lemma IObis_congr_nil_r : ∀ p, (wfp_Par p wfp_Nil) ≈ p.
Proof.
introv; apply congr_IObis. apply wfcgr_nil_r.
Qed.
Lemma IObis_congr_par_com : ∀ p q, (wfp_Par p q) ≈ (wfp_Par q p).
Proof.
introv; apply congr_IObis. apply wfcgr_par_com.
Qed.
Lemma IObis_par_assoc_l : ∀ p q r, (wfp_Par p (wfp_Par q r)) ≈ (wfp_Par (wfp_Par p q) r).
Proof.
introv; apply congr_IObis. apply wfcgr_par_assoc_l.
Qed.
Lemma IObis_par_assoc_r : ∀ p q r, (wfp_Par (wfp_Par p q) r) ≈ (wfp_Par p (wfp_Par q r)).
Proof.
introv; apply congr_IObis. apply wfcgr_par_assoc_r.
Qed.
Lemma IObis_congr_par : ∀ p1 p2 q1 q2,
p1 ≈ p2 → q1 ≈ q2 → wfp_Par p1 q1 ≈ wfp_Par p2 q2.
Proof.
introv Hio1 Hio2. etransitivity.
apply IObis_congr_par1. eassumption.
etransitivity.
apply IObis_congr_par_com.
etransitivity.
apply IObis_congr_par1. eassumption.
apply IObis_congr_par_com.
Qed.
Inductive R_subst : binary wfprocess :=
| Rsb : ∀ X (p q l r : wfprocess), (guarded X p) → (guarded X q)
→ p≈q → R_subst (wfp_Par (wfp_subst r X p) l) (wfp_Par (wfp_subst r X q) l).
Hint Resolve R_subst.
Lemma IObis_subst1 : ∀ X (p q r : wfprocess),
p≈q → (wfp_subst r X p) ≈ (wfp_subst r X q).
Proof with (try solve [applys× t_step]); automate.
intros X p q r Hio.
specialize (wfp_guarded_IObis X _ _ Hio). intros Hex.
destruct Hex as [p1 [q1 [Hgu1_1 [Hc1 [Hgu2_1 [Hc2 Hio1]]]]]].
eapply IObis_trans. apply congr_IObis. applys¬ wfcgr_subst2. apply Hc1.
apply IObis_sym.
eapply IObis_trans. apply congr_IObis. applys¬ wfcgr_subst2. apply Hc2.
apply (IObis_up_to_IObis wfcgr); auto with congr_bisim.
rewrite <- IObis_ex_up_to_IObis_up_to. ∃ R_subst. split.
2: repeat rewrite wfp_eq_subst_par; constructor¬.
Focus 2.
introv Hc. inverts Hc; apply congr_swap...
etransitivity; eassumption.
clear.
splits. introv Hr; inverts Hr... constructor¬.
intros p0 q0 Hr a fp0 Ht0´.
inversion Hr as [X p q l r Hgu1 Hgu2 Hio Hre1 Hre2]; subst p0 q0.
inversion Ht0´...
destruct ap; inverts H3. subst.
rename H2 into Htp0, a0 into fp0.
lets (fp & Htp & Heq1) : wfp_guarded_subst_trans_in Hgu1 Htp0.
lets (fq & Htq & Hc) : IObis_in Hio Htp.
lets (fq0 & Htq0 & Heq2) : wfp_trans_subst_in X r Htq.
∃ (AbsPar1 fq0 l); splits...
lets (Y & Hfy) : find_fresh (proc (wfp_Par (wfp_subst r X p) l) :: proc (wfp_Par (wfp_subst r X q) l) :: proc p :: proc q :: Gvar X :: nil).
inverts Hfy as Hfyp1. rewrite Forall_to_conj_4 in H3.
destruct H3 as (Hfyp2 & Hfyp & Hfyq & Hff).
specializes¬ Hc Hfyq.
assert (Hfyx : X ≠ Y) by freshen_up; clear Hff.
specializes Heq1 Hfyx; specializes¬ Heq2 Hfyx.
∃ Y; splits; simpl...
constructor.
specialize (wfp_guarded_IObis X _ _ Hc). intros Hex.
destruct Hex as [p1´ [q1´ [Hgu1_1 [Hc1 [Hgu2_1 [Hc2 Hio1]]]]]].
∃ (wfp_Par (wfp_subst r X p1´) (wfp_Par (wfp_subst r X (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X (wfp_inst_Abs fp (wfp_Gvar Y))))) l))
(wfp_Par (wfp_subst r X q1´) (wfp_Par (wfp_subst r X (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X (wfp_inst_Abs fp (wfp_Gvar Y))))) l)).
splits...
rewrite Heq1.
etransitivity.
Focus 2. constructor. apply WfCgrPar_assoc2.
apply wfcgr_par... rewrite <- wfp_eq_subst_par.
apply wfcgr_subst...
rewrite Heq2.
etransitivity.
constructor. apply WfCgrPar_assoc1.
apply wfcgr_par... rewrite <- wfp_eq_subst_par.
apply wfcgr_subst... symmetry...
constructor¬.
destruct aq; inverts H3...
∃ (AbsPar2 (wfp_subst r X q) a0). splits...
lets (Y & Hfy) : find_fresh (proc (wfp_Par (wfp_subst r X p) l) :: proc (wfp_Par (wfp_subst r X q) l) :: nil).
rewrite Forall_to_conj_2 in Hfy; inverts Hfy.
∃ Y; splits¬.
constructor. eexists. eexists.
splits. reflexivity. reflexivity.
simpls. constructor...
intros p0 q0 Hr a p0´ p0´´ Ht0´.
inversion Hr as [X p q l r Hgu1 Hgu2 Hio Hre1 Hre2]; subst p0 q0.
inversion Ht0´. destruct ap; inverts H3...
lets (p´ & p´´ & Ht & Heq1 & Heq2) : wfp_guarded_subst_trans_out X Hgu1 H2; subst.
lets (q´ & q´´ & Htq & Hio2 & Hio3) : IObis_out Hio Ht.
∃ (wfp_Par (wfp_subst r X q´) l) (wfp_subst r X q´´). splits...
apply act1_out. apply¬ wfp_trans_subst_out.
constructor.
∃ (wfp_Par (wfp_subst r X p´) l) (wfp_Par (wfp_subst r X q´) l). splits...
constructor¬.
apply wfp_guarded_out with (X := X) in Ht; auto.
apply wfp_guarded_out with (X := X) in Htq; auto.
constructor.
specialize (wfp_guarded_IObis X _ _ Hio3). intros Hex.
destruct Hex as [p1´´ [q1´´ [Hgu1_1 [Hc1 [Hgu2_1 [Hc2 Hio3´]]]]]].
∃ (wfp_Par (wfp_subst r X p1´´) (wfp_subst r X (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X p´´))))
(wfp_Par (wfp_subst r X q1´´) (wfp_subst r X (wfp_prod_repeat (wfp_Gvar X) (size_unguardedX X p´´)))); splits.
rewrite <- wfp_eq_subst_par; apply wfcgr_subst...
rewrite <- wfp_eq_subst_par; apply wfcgr_subst; symmetry...
constructor¬.
destruct aq; inverts H3...
∃ (wfp_Par (wfp_subst r X q) w) p0´´. splits...
constructor.
∃ (wfp_Par (wfp_subst r X p) w) (wfp_Par (wfp_subst r X q) w).
splits... constructor¬.
constructor. ∃ (wfp_Par (wfp_subst r X wfp_Nil) p0´´) (wfp_Par (wfp_subst r X wfp_Nil) p0´´).
splits.
simpl... etransitivity. Focus 2. constructor. apply WfCgrPar_com. auto...
simpl... etransitivity. constructor. apply WfCgrPar_com. auto...
constructor¬.
intros p0 q0 Hr Z p0´ Ht0´.
inversion Hr as [X p q l r Hgu1 Hgu2 Hio Hre1 Hre2]; subst p0 q0.
inverts Ht0´...
destruct ap; inverts H3.
lets (p1 & Ht & Heq) : wfp_guarded_subst_trans_remove Hgu1 H2. subst.
lets (q1 & Htq & Hio2) : IObis_var Hio Ht.
∃ (wfp_Par (wfp_subst r X q1) l). split...
apply act1_rem. apply wfp_guarded_remove_subst; assumption.
constructor.
∃ (wfp_Par (wfp_subst r X p1) l) (wfp_Par (wfp_subst r X q1) l).
splits; constructor; simpls¬.
eapply wfp_guarded_remove. apply Hgu1. apply Ht.
eapply wfp_guarded_remove. apply Hgu2. apply Htq.
destruct aq; inverts H3.
∃ (wfp_Par (wfp_subst r X q) w). split...
constructor.
∃ (wfp_Par (wfp_subst r X p) w) (wfp_Par (wfp_subst r X q) w).
splits; constructor¬.
Qed.
Lemma IObis_subst2 : ∀ X (p r r´ : wfprocess), r≈r´ →(wfp_subst r X p) ≈ (wfp_subst r´ X p).
Proof with automate.
induction p as [p HI] using (measure_induction wfp_size); introv Hio.
destruct_wf p...
apply IObis_congr_send. apply HI...
tests Hneq : (X = X0).
repeat rewrite wfp_gfresh_subst_rewrite...
simpl; unfold Abs; rewrite gfresh_receive; fresh_solve.
simpl; unfold Abs; rewrite gfresh_receive; fresh_solve.
lets Hypr : wfp_eq_subst_abs3 r a p0 Hneq.
lets Hypr´ : wfp_eq_subst_abs3 r´ a p0 Hneq.
lets (Z & Hfz) : find_fresh (Gvar X :: proc r :: proc r´ :: proc p0 :: nil).
rewrite Forall_to_conj_4 in Hfz. destruct Hfz as (Hfzx & Hfzr & Hfzr´ & Hfzp0).
rewrite gfresh_gvar in Hfzx.
specializes¬ Hypr Hfzp0. specializes¬ Hypr´ Hfzp0.
rewrite Hypr, Hypr´. apply IObis_congr_abs.
apply HI...
repeat cases_if×.
apply IObis_congr_par; apply HI...
Qed.
Lemma IObis_subst : ∀ X (p q r r´ : wfprocess),
p≈q → r≈r´ → (wfp_subst r X p) ≈ (wfp_subst r´ X q).
Proof.
introv Hio1 Hio2.
etransitivity.
apply IObis_subst1. apply Hio1.
apply¬ IObis_subst2.
Qed.
Lemma IObis_tau : tau_relation IObis.
Proof.
introv Hio Ht.
apply wfp_decomposition_tau1 in Ht.
destruct Ht as [a [p1 [p´´ [fp [Ht_out [Ht_in Heq]]]]]].
specialize (IObis_out _ _ Hio a p1 p´´ Ht_out). intros Hex.
destruct Hex as [q´ [q´´ [Ht_out´ [Hio2 Hio3]]]].
specialize (IObis_in _ _ Hio2 _ _ Ht_in). intros Hex.
destruct Hex as [fq [Ht_in´ Hio4]].
∃ (wfp_inst_Abs fq q´´). split. eapply wfp_decomposition_tau2.
apply Ht_out´. apply Ht_in´.
rewrite Heq.
lets (X & Hfx) : find_fresh (proc p1 :: proc q´ :: nil).
rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfp1 & Hfq´).
rewrite wfp_inst_subst with (fp:=fp) (p:=p1) (X:=X) (a:=a); auto.
rewrite wfp_inst_subst with (fp:=fq) (p:=q´) (X:=X) (a:=a); auto.
eapply IObis_subst; simpls¬.
Qed.
Lemma IObis_unguardeds_eq : ∀ (p q : wfprocess),
p≈q → unguardeds p = unguardeds q.
Proof.
introv (R & Hio & HRpq).
inverts Hio; destruct H0 as (_ & _ & Hvpq).
assert (HRqp : R q p) by (applys¬ H).
lets Hvqp : Hvpq; specialize (Hvpq p q HRpq); specialize (Hvqp q p HRqp).
lets Hrem : wfp_unguarded_remove_iff.
apply fset_extens; introv Hin; rewrite Hrem in Hin; destruct Hin as (r & Ht).
apply Hvpq in Ht; destruct Ht as (q´ & Ht & _); rewrite Hrem; ∃¬ q´.
apply Hvqp in Ht; destruct Ht as (p´ & Ht & _); rewrite Hrem; ∃¬ p´.
Qed.
Lemma IObis_in_full : in_full_relation IObis.
Proof.
introv Hr Ht.
lets (fq & H´ & Hin) : (IObis_in _ _ Hr _ _ Ht).
lets (Y & Hfy) : find_fresh (proc p :: proc q :: nil);
rewrite Forall_to_conj_2 in Hfy; destruct Hfy as (Hfyp & Hfyq).
specializes¬ Hin Hfyq.
∃ fq; splits¬. introv.
tests Hneq : (X = Y); auto.
rewrite wfp_subst_on_inst_Abs2 with (p := p) (a := a) (Y := Y); auto.
rewrite wfp_subst_on_inst_Abs2 with (p := q) (a := a) (Y := Y) (fp := fq); auto.
applys¬ IObis_subst.
Qed.