Library HOC18ONORbis
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 HOC17NORbis.
Lemma ONORbis_refl : Reflexive ONORbis.
Proof.
introv; ∃ R_refl; splits¬.
clear x; splits; introv Hr.
inverts Hr; constructor.
introv Ht; inverts Hr; ∃¬ p´.
introv Ht; inverts Hr; ∃¬ p´ p´´.
introv Ht; inverts Hr; ∃¬ fp; splits¬.
introv Ht; inverts Hr; ∃ p´; splits¬.
Qed.
Lemma ONORbis_sym : Symmetric ONORbis.
Proof.
introv H. inversion H as [R HR].
unfold ONORbis. ∃ R. split. apply HR.
unfold OpenNormal_bisimulation in HR.
apply HR. apply HR.
Qed.
Lemma ONORbis_tau : tau_relation ONORbis.
Proof.
introv Hio Ht.
inversion Hio as (R & HR).
assert (∃ (q´ : wfprocess), {{q -- Tau ->> AP q´}} ∧ R p´ q´).
unfold OpenNormal_bisimulation, tau_relation in HR. eapply HR.
apply HR.
assumption.
inversion H as (q´ & Hq).
∃ q´. split. apply Hq.
∃ R. split. apply HR. apply Hq.
Qed.
Lemma ONORbis_out_normal : out_normal_relation ONORbis.
Proof.
introv Hio Ht.
inversion Hio as [R HR].
assert (∃ (q´ q´´ : wfprocess), ({{q--LabOut a q´´->>(AP q´)}} ∧ (∀ m X, m ### p → m ### q →
X # p´´ → X # q´´ → R (wfp_Par (wfp_Abs m X p´´) p´) (wfp_Par (wfp_Abs m X q´´) q´)))).
unfold OpenNormal_bisimulation, out_normal_relation in HR. applys¬ HR. apply HR.
inversion H as [q´ Hex]. inversion Hex as [q´´ Hq].
∃ q´ q´´. split. apply Hq.
∃ R. split. apply HR. applys¬ Hq.
Qed.
Lemma ONORbis_out_normal_ex : out_normal_relation_ex ONORbis.
Proof.
introv Hio Ht.
inversion Hio as [R HR].
lets (q´ & q´´ & Htq & Hrq) : ONORbis_out_normal Hio Ht.
∃ q´ q´´; splits¬.
lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil); rewrite Forall_to_conj_2 in Hfm.
lets (X & Hfx) : find_fresh (proc p´´ :: proc q´´ :: nil); rewrite Forall_to_conj_2 in Hfx.
∃ m X; splits×.
Qed.
Lemma ONORbis_in : in_relation ONORbis.
Proof.
introv Hio Ht.
inversion Hio as [R HR].
assert (∃ 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)))).
unfold OpenNormal_bisimulation, in_normal_relation in HR. applys¬ HR. apply HR.
inversion H as (fq & Ht´ & Hq).
∃ fq; splits¬.
intros X Hf1 Hf2. ∃× R.
Qed.
Lemma ONORbis_var : var_relation ONORbis.
Proof.
introv Hio Ht.
inversion Hio as [R [HR Hr]].
assert (∃ (q´ : wfprocess), {{q--LabRem X->>(AP q´)}} ∧ (R p´ q´)).
eapply HR. apply Hr. apply Ht.
destruct H as [q´ Hq].
∃ q´. split. apply Hq. ∃ R. intuition.
Qed.
Fixpoint sizeO (p : process) : nat :=
match p with
| Send _ p ⇒ S (sizeO p)
| Receive _ _ p ⇒ (sizeO p)
| Lvar _ ⇒ 0
| Gvar _ ⇒ 0
| Par p q ⇒ ((sizeO p) + (sizeO q))
| Nil ⇒ 0
end.
Definition wfp_sizeO (p : wfprocess) : nat := sizeO (proc p).
Lemma sizeO_subst : ∀ X p q,
sizeO q = 0 → sizeO p = sizeO ([q // X]p).
Proof.
introv H.
inductions p; simpls ; try cases_if ; simpls¬.
Qed.
Lemma sizeO_in : ∀ a p (m : wfprocess) fp,
sizeO m = 0 → {{p -- LabIn a ->> (AA fp)}} → sizeO p = sizeO (wfp_inst_Abs fp m).
Proof.
introv H Ht.
inductions Ht; simpls¬. repeat rewrite¬ <- sizeO_subst.
destruct fp; destruct ap; inverts x.
simpl. erewrite× IHHt.
destruct fp; destruct aq; inverts x.
simpl. erewrite× IHHt.
Qed.
Lemma sizeO_out : ∀ a p p´ p´´,
{{p -- LabOut a p´´ ->> (AP p´)}} → sizeO p = sizeO p´ + sizeO p´´ + 1.
Proof.
introv Ht.
inductions Ht; simpls¬. nat_math.
destruct ap; inverts x.
simpl. erewrite× IHHt. nat_math.
destruct aq; inverts x.
simpl. erewrite× IHHt. nat_math.
Qed.
Lemma sizeO_remove : ∀ X p p´,
{{p -- LabRem X ->> (AP p´)}} → sizeO p = (sizeO p´).
Proof.
introv Ht.
inductions Ht ; simpls×.
destruct ap; inverts x. simpl.
rewrite× (IHHt w).
destruct aq; inverts x. simpl.
rewrite× (IHHt w).
Qed.
Definition wfp_sizeP_out (p : wfprocess) : nat :=
wfp_sizeP p + wfp_sizeO p.
Theorem sizeX_ONORbis : ∀ X p q,
p ≈ONOR q → sizeX X p = sizeX X q.
Proof.
intro X. induction p using (measure_induction wfp_sizeP_out). introv Hon.
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 ONORbis_sym in Hon.
lets (p´ & Hp & Hon´): (ONORbis_var q p Hon X q´ Hq). apply sizeX_remove in Hp. nat_math.
lets (fp & Hp & Hon´): (ONORbis_in q p Hon 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)).
unfold wfp_sizeP_out; unfold wfp_sizeP, wfp_sizeO; simpl.
lets Hp´ : Hp; apply (sizeP_in a p (wfp_Gvar Z) fp) in Hp´; simpl in Hp´; auto.
lets Hp´´ : Hp; apply (sizeO_in a p (wfp_Gvar Z) fp) in Hp´´; simpl in Hp´´; auto.
nat_math.
apply ONORbis_sym. apply¬ Hon´.
etransitivity. symmetry. applys¬ Hsq. simpl. cases_if¬. auto.
lets (p´ & p´´ & Hp & Hon´): (>> ONORbis_out_normal q p Hon a q´ q´´ Hq).
lets Hsp: (>> sizeX_out a X p p´ p´´ Hp).
lets Hsq: (>> sizeX_out a X q q´ q´´ Hq).
lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil); rewrite Forall_to_conj_2 in Hfm.
lets (Y & Hfy) : find_fresh (proc p´´ :: proc q´´ :: (Gvar X) :: nil); rewrite Forall_to_conj_3 in Hfy.
inverts Hfm as Hfmp Hfmq; inverts Hfy as Hfyp Hfyq; inverts Hfyq as Hfyq Hfyx.
specializes¬ Hon´ Hfyp.
etransitivity. eassumption.
etransitivity. apply Hsp.
transitivity (sizeX X q´ + sizeX X q´´).
replace (sizeX X p´ + sizeX X p´´) with (sizeX X (wfp_Par (wfp_Abs m Y p´´) p´)).
replace (sizeX X q´ + sizeX X q´´) with (sizeX X (wfp_Par (wfp_Abs m Y q´´) q´)).
apply ONORbis_sym in Hon´. applys¬ H.
unfold wfp_sizeP_out;
unfold wfp_sizeP, wfp_sizeO; simpl.
rewrite (sizeP_out _ _ _ _ Hp); rewrite (sizeO_out _ _ _ _ Hp).
rewrite¬ sizeP_subst; rewrite¬ <- sizeO_subst; nat_math.
simpls; rewrite¬ (sizeX_subst2_cp X Y q´´ (Lvar (f Y q´´))).
nat_math.
rewrite gfresh_gvar in Hfyx; auto.
unfold closed_process; simpls¬.
simpls; rewrite¬ (sizeX_subst2_cp X Y p´´ (Lvar (f Y p´´))).
nat_math.
rewrite gfresh_gvar in Hfyx; auto.
unfold closed_process; simpls¬.
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´): (>> ONORbis_var p q Hon 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_sizeP_out, wfp_sizeP, wfp_sizeO; simpls.
lets Hp´ : Hp; apply sizeP_remove in Hp; apply sizeO_remove in Hp´; nat_math.
lets (fq & Hq & Hio´): (ONORbis_in p q Hon 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.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpls.
lets Hp´ : Hp; lets Hp´´ : Hp.
apply sizeP_in with (m:=(wfp_Gvar Z)) in Hp´; apply sizeO_in with (m := (wfp_Gvar Z)) in Hp´´; auto; nat_math.
lets (q´ & q´´ & Hq & Hon´): (>> ONORbis_out_normal p q Hon a p´ p´´ Hp).
lets Hsp: (>> sizeX_out a X p p´ p´´ Hp).
lets Hsq: (>> sizeX_out a X q q´ q´´ Hq).
lets (m & Hfm) : find_fresh_chan (proc p :: proc q :: nil); rewrite Forall_to_conj_2 in Hfm.
lets (Y & Hfy) : find_fresh (proc p´´ :: proc q´´ :: (Gvar X) :: nil); rewrite Forall_to_conj_3 in Hfy.
inverts Hfm as Hfmp Hfmq; inverts Hfy as Hfyp Hfyq; inverts Hfyq as Hfyq Hfyx.
etransitivity. eassumption.
symmetry. etransitivity. eassumption. symmetry.
replace (sizeX X p´ + sizeX X p´´) with (sizeX X (wfp_Par (wfp_Abs m Y p´´) p´)).
replace (sizeX X q´ + sizeX X q´´) with (sizeX X (wfp_Par (wfp_Abs m Y q´´) q´)).
applys¬ H.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
rewrite (sizeP_out _ _ _ _ Hp); rewrite (sizeO_out _ _ _ _ Hp).
rewrite¬ sizeP_subst; rewrite¬ <- sizeO_subst; nat_math.
simpls; rewrite¬ (sizeX_subst2_cp X Y q´´ (Lvar (f Y q´´))).
nat_math.
rewrite gfresh_gvar in Hfyx; auto.
unfold closed_process; simpls¬.
simpls; rewrite¬ (sizeX_subst2_cp X Y p´´ (Lvar (f Y p´´))).
nat_math.
rewrite gfresh_gvar in Hfyx; auto.
unfold closed_process; simpls¬.
Qed.
Lemma gfresh_ONORbis : ∀ X p q,
p ≈ONOR q → X#p → X#q.
Proof.
introv Hio Hf.
apply sizeX_gfresh. apply sizeX_gfresh in Hf.
rewrite <- Hf. symmetry. apply¬ sizeX_ONORbis.
Qed.
Theorem sizeCh_ONORbis : ∀ m p q,
p ≈ONOR q → sizeCh m p = sizeCh m q.
Proof.
intro m. induction p using (measure_induction wfp_sizeP_out). introv Hon.
remember (sizeCh m p) as sp. destruct sp.
remember (sizeCh m q) as sq. destruct¬ sq.
assert (Hchq : CHS q ≠ \{}) by (rewrite <- sizeCh_CHS; ∃ m; nat_math).
apply trans_CHS in Hchq.
apply ONORbis_sym in Hon; rewrite Heqsp; destruct Hchq as [[a [fq Htq]] |[a [q´ [q´´ Htq]]]].
lets (fp & Htp & Hon´): (ONORbis_in q p Hon a fq Htq).
lets (Z & Hex2): (find_fresh ((proc p)::(proc q)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (Hf1 & Hf2).
elim (classic (a = m)); introv Hneq; subst.
lets× Hsp: (>> sizeCh_in_eq m p (wfp_Gvar Z) fp Htp).
lets× Hsq: (>> sizeCh_in_eq m q (wfp_Gvar Z) fq Htq).
etransitivity. eassumption.
replace (S sq) with (sizeCh m (wfp_inst_Abs fq (wfp_Gvar Z)) + 1).
cut (sizeCh m (wfp_inst_Abs fp (wfp_Gvar Z)) = sizeCh m (wfp_inst_Abs fq (wfp_Gvar Z))); try nat_math.
rewrite <- Hsq; nat_math.
lets× Hsp: (>> sizeCh_in_neq m p (wfp_Gvar Z) fp Htp).
lets× Hsq: (>> sizeCh_in_neq m q (wfp_Gvar Z) fq Htq).
etransitivity. eassumption.
etransitivity. apply H with (q := wfp_inst_Abs fq (wfp_Gvar Z)).
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
lets Hp´ : Htp; apply (sizeP_in a p (wfp_Gvar Z) fp) in Hp´; simpl in Hp´; auto.
lets Hp´´ : Htp; apply (sizeO_in a p (wfp_Gvar Z) fp) in Hp´´; simpl in Hp´´; auto; nat_math.
apply ONORbis_sym. apply¬ Hon´.
etransitivity. symmetry. applys¬ Hsq. auto.
lets (p´ & p´´ & Htp & Hon´): (>> ONORbis_out_normal q p Hon a q´ q´´ Htq).
lets (n & Hfn) : find_fresh_chan (proc p :: proc q :: (Send m wfp_Nil) :: nil); rewrite Forall_to_conj_3 in Hfn.
lets (Y & Hfy) : find_fresh (proc p´´ :: proc q´´ :: nil); rewrite Forall_to_conj_2 in Hfy.
inverts Hfn as Hfnp (Hfnq & Hneqmn); inverts Hfy as Hfyp Hfyq.
assert (Hneqna : n ≠ a) by (intro Heqna; subst; apply false_trans_out with (p´ := (AP p´)) (p´´ := p´´) in Hfnp; intuition).
specializes¬ Hon´ Hfyp; clear Hfnp Hfnq Hfyp Hfyq.
elim (classic (a = m)); introv Hneq; subst.
lets Hsp: (>> sizeCh_out_eq m p p´ p´´ Htp).
lets Hsq: (>> sizeCh_out_eq m q q´ q´´ Htq).
etransitivity. eassumption.
rewrite Heqsq; rewrite Hsq.
replace (sizeCh m p´ + sizeCh m p´´) with (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´)).
replace (sizeCh m q´ + sizeCh m q´´) with (sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)).
cut (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´) = sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)); try nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
unfold fresh_chan in Hneqmn; simpls.
unfold notin in Hneqmn; rewrite in_union in Hneqmn; rew_logic in Hneqmn.
destruct Hneqmn as (Hneqmn & _); rewrite in_singleton in Hneqmn.
lets× Hsp: (>> sizeCh_out_neq m p p´ p´´ Htp).
lets× Hsq: (>> sizeCh_out_neq m q q´ q´´ Htq).
etransitivity. eassumption.
rewrite Heqsq; rewrite Hsq.
replace (sizeCh m p´ + sizeCh m p´´) with (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´)).
replace (sizeCh m q´ + sizeCh m q´´) with (sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)).
applys¬ H.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
rewrite (sizeP_out _ _ _ _ Htp); rewrite (sizeO_out _ _ _ _ Htp).
rewrite¬ sizeP_subst; rewrite¬ <- sizeO_subst; nat_math.
applys¬ ONORbis_sym.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
assert (Hchq : CHS p ≠ \{}) by (rewrite <- sizeCh_CHS; ∃ m; nat_math).
apply trans_CHS in Hchq.
rewrite Heqsp; destruct Hchq as [[a [fp Htp]] |[a [p´ [p´´ Htp]]]].
lets (fq & Htq & Hon´): (ONORbis_in p q Hon a fp Htp).
lets (Z & Hex2): (find_fresh ((proc p)::(proc q)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (Hf1 & Hf2).
elim (classic (a = m)); introv Hneq; subst.
lets× Hsp: (>> sizeCh_in_eq m p (wfp_Gvar Z) fp Htp).
lets× Hsq: (>> sizeCh_in_eq m q (wfp_Gvar Z) fq Htq).
etransitivity. eassumption. rewrite Hsq.
cut (sizeCh m (wfp_inst_Abs fp (wfp_Gvar Z)) = sizeCh m (wfp_inst_Abs fq (wfp_Gvar Z))); try nat_math.
applys¬ H.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
lets Hp´ : Htp; apply (sizeP_in m p (wfp_Gvar Z) fp) in Hp´; simpl in Hp´; auto.
lets Hp´´ : Htp; apply (sizeO_in m p (wfp_Gvar Z) fp) in Hp´´; simpl in Hp´´; auto; nat_math.
lets× Hsp: (>> sizeCh_in_neq m p (wfp_Gvar Z) fp Htp).
lets× Hsq: (>> sizeCh_in_neq m q (wfp_Gvar Z) fq Htq).
rewrite Hsp; rewrite Hsq.
etransitivity. apply H with (q := wfp_inst_Abs fq (wfp_Gvar Z)).
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
lets Hp´ : Htp; apply (sizeP_in a p (wfp_Gvar Z) fp) in Hp´; simpl in Hp´; auto.
lets Hp´´ : Htp; apply (sizeO_in a p (wfp_Gvar Z) fp) in Hp´´; simpl in Hp´´; auto; nat_math.
apply¬ Hon´.
etransitivity. symmetry. applys¬ Hsq. auto.
lets (q´ & q´´ & Htq & Hon´): (>> ONORbis_out_normal p q Hon a p´ p´´ Htp).
lets (n & Hfn) : find_fresh_chan (proc p :: proc q :: (Send m wfp_Nil) :: nil); rewrite Forall_to_conj_3 in Hfn.
lets (Y & Hfy) : find_fresh (proc p´´ :: proc q´´ :: nil); rewrite Forall_to_conj_2 in Hfy.
inverts Hfn as Hfnp (Hfnq & Hneqmn); inverts Hfy as Hfyp Hfyq.
assert (Hneqna : n ≠ a) by (intro Heqna; subst; apply false_trans_out with (p´ := (AP p´)) (p´´ := p´´) in Hfnp; intuition).
specializes¬ Hon´ Hfyq; clear Hfnp Hfnq Hfyp Hfyq.
elim (classic (a = m)); introv Hneq; subst.
lets Hsp: (>> sizeCh_out_eq m p p´ p´´ Htp).
lets Hsq: (>> sizeCh_out_eq m q q´ q´´ Htq).
etransitivity. eassumption.
rewrite Hsq.
replace (sizeCh m p´ + sizeCh m p´´) with (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´)).
replace (sizeCh m q´ + sizeCh m q´´) with (sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)).
cut (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´) = sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)); try nat_math.
apply¬ H.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
rewrite (sizeP_out _ _ _ _ Htp); rewrite (sizeO_out _ _ _ _ Htp).
rewrite¬ sizeP_subst; rewrite¬ <- sizeO_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
unfold fresh_chan in Hneqmn; simpls.
unfold notin in Hneqmn; rewrite in_union in Hneqmn; rew_logic in Hneqmn.
destruct Hneqmn as (Hneqmn & _); rewrite in_singleton in Hneqmn.
lets× Hsp: (>> sizeCh_out_neq m p p´ p´´ Htp).
lets× Hsq: (>> sizeCh_out_neq m q q´ q´´ Htq).
etransitivity. eassumption.
rewrite Hsq.
replace (sizeCh m p´ + sizeCh m p´´) with (sizeCh m (wfp_Par (wfp_Abs n Y p´´) p´)).
replace (sizeCh m q´ + sizeCh m q´´) with (sizeCh m (wfp_Par (wfp_Abs n Y q´´) q´)).
applys¬ H.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpl.
rewrite (sizeP_out _ _ _ _ Htp); rewrite (sizeO_out _ _ _ _ Htp).
rewrite¬ sizeP_subst; rewrite¬ <- sizeO_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
simpls; cases_if*; rewrite× <- sizeCh_subst; nat_math.
Qed.
Lemma cfresh_ONORbis : ∀ m p q,
p ≈ONOR q → m ### p → m ### q.
Proof.
introv Hio Hf.
rewrite sizeCh_cfresh in ×.
rewrite <- Hf. symmetry. apply¬ sizeCh_ONORbis.
Qed.
Definition OpenNormal_bisimulation_ex (R : RelWfP) : Prop :=
(Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation_ex R) ∧ (in_relation_ex R) ∧ (var_relation R).
Definition ONORbis_ex p q : Prop :=
∃ R, (OpenNormal_bisimulation_ex R) ∧ (R p q).
Inductive R_Swap_All R : binary wfprocess :=
| Rbase : ∀ p q, R p q → R_Swap_All R p q
| RswapX : ∀ X Y p q, R_Swap_All R p q → R_Swap_All R (wfp_swap X Y p) (wfp_swap X Y q)
| Rswapm : ∀ m n p q, R_Swap_All R p q → R_Swap_All R (wfp_swap_chan m n p) (wfp_swap_chan m n q).
Hint Resolve Rbase RswapX Rswapm.
Lemma ONOR_ONOR_ex : ∀ p q, ONORbis p q ↔ ONORbis_ex p q.
Proof with automate.
introv; split; intro Hyp.
∃ ONORbis; splits¬.
splits.
apply ONORbis_sym.
apply ONORbis_tau.
apply out_nor_forall_exists; apply ONORbis_out_normal.
apply in_forall_exists; apply ONORbis_in.
apply ONORbis_var.
destruct Hyp as (R & HR & Hr).
∃ (R_Swap_All R); split¬.
clear p q Hr; splits.
introv Hr. induction Hr.
constructor. apply¬ HR.
apply¬ RswapX.
apply¬ Rswapm.
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). eapply HR2 in H; auto.
edestruct H as (q´ & Htq & Hr1); try eassumption.
∃ q´. splits¬.
forwards Ht´: wfp_trans_swap_tau X Y Ht; simpl in Ht´.
rewrite wfp_swap_involutive in Ht´.
edestruct (IHHr (wfp_swap X Y p´)) as (q´ & Htq & Hr1). assumption.
∃ (wfp_swap X Y q´). splits.
applys¬ wfp_trans_swap_tau.
erewrite <- wfp_swap_involutive at 1; auto.
forwards Ht´: wfp_trans_swap_chan_tau m n Ht; simpl in Ht´.
rewrite wfp_swap_chan_involutive in Ht´.
edestruct (IHHr (wfp_swap_chan m n p´)) as (q´ & Htq & Hr1). assumption.
∃ (wfp_swap_chan m n q´). splits.
applys¬ wfp_trans_swap_chan_tau.
erewrite <- wfp_swap_chan_involutive at 1; auto.
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). eapply HR3 in H; auto.
edestruct (H a p´ p´´ Ht) as (q´ & q´´ & Htq & n & Y & Hfnp & Hfnq & Hfyp & Hfyq & Hr); clear H.
∃ q´ q´´; splits¬.
introv Hfmp Hfmq Hfxp Hfxq.
lets (Hfsmp´ & Hfsmp´´) : wfp_cswap_fresh_trans_out Hfmp Hfnp Ht;
lets (Hfsmq´ & Hfsmq´´) : wfp_cswap_fresh_trans_out Hfmq Hfnq Htq.
elim (classic (m = n)); elim (classic (X = Y)); intros Hneqxy Hneqmn; substs¬.
clear Hfmp Hfmq.
assert (Heqp : wfp_Abs n Y p´´ = wfp_Abs n X p´´).
rewrite wfp_Abs_eq with (Y := X); auto.
rewrites¬ wfp_gfresh_subst_rewrite.
assert (Heqq : wfp_Abs n Y q´´ = wfp_Abs n X q´´).
rewrite wfp_Abs_eq with (Y := X); auto.
rewrites¬ wfp_gfresh_subst_rewrite.
rewrite <- Heqp, <- Heqq; constructor¬.
clear Hfxp Hfxq.
apply (Rbase R) in Hr.
apply (Rswapm R m n) in Hr.
replace (wfp_swap_chan m n (wfp_Par (wfp_Abs n Y p´´) p´)) with
(wfp_Par (wfp_Abs m Y p´´) p´) in Hr.
replace (wfp_swap_chan m n (wfp_Par (wfp_Abs n Y q´´) q´)) with
(wfp_Par (wfp_Abs m Y q´´) q´) in Hr; auto...
unfold swap_name; repeat cases_if×. rewrite Hfsmq´, Hfsmq´´; auto.
simpl... unfold swap_name; repeat cases_if*; rewrite Hfsmp´, Hfsmp´´; auto.
apply (Rbase R) in Hr.
assert (Heqp : wfp_Abs m X p´´ = wfp_Abs m Y p´´).
rewrite wfp_Abs_eq with (Y := Y); auto.
rewrites¬ wfp_gfresh_subst_rewrite.
assert (Heqq : wfp_Abs m X q´´ = wfp_Abs m Y q´´).
rewrite wfp_Abs_eq with (Y := Y); auto.
rewrites¬ wfp_gfresh_subst_rewrite.
rewrite Heqp, Heqq.
apply (Rswapm R m n) in Hr.
replace (wfp_swap_chan m n (wfp_Par (wfp_Abs n Y p´´) p´)) with
(wfp_Par (wfp_Abs m Y p´´) p´) in Hr.
replace (wfp_swap_chan m n (wfp_Par (wfp_Abs n Y q´´) q´)) with
(wfp_Par (wfp_Abs m Y q´´) q´) in Hr; auto...
unfold swap_name; repeat cases_if*; rewrite Hfsmq´, Hfsmq´´; auto.
simpl... unfold swap_name; repeat cases_if*; rewrite Hfsmp´, Hfsmp´´; auto.
forwards Ht´: wfp_trans_swap_out X Y Ht; lets Ht´´ : Ht´; simpl in Ht´, 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). assumption. clear IHHr.
∃ (wfp_swap X Y q´) (wfp_swap X Y q´´); splits.
applys¬ wfp_trans_swap_out.
intros m Z Hfmp Hfmq; rewrite <- wfp_cfresh_swap_inv in ×.
introv Hfzp Hfzq.
assert (Heqabs : ∀ X Y r, (wfp_Abs m Y (wfp_swap X Y r)) = wfp_swap X Y (wfp_Abs m X r)).
introv; rewrite wfp_eq_swap_abs; unfold swap_gvar; cases_if×.
assert (Heqabs´ : ∀ X Y r, (wfp_Abs m X (wfp_swap X Y r)) = wfp_swap X Y (wfp_Abs m Y r)).
introv; rewrite wfp_eq_swap_abs; unfold swap_gvar; repeat cases_if*;
subst; fequals.
elim (classic (Z = Y)); elim (classic (Z = X)); introv Heqx Heqy; subst.
subst Y; repeat rewrite wfp_swap_equal in *; repeat rewrite swap_equal in *; applys¬ Hr1.
specializes Hr1 m X; rewrite Heqabs in *; rewrite Heqabs´ in ×.
rewrite <- wfp_eq_swap_par in ×.
erewrite <- wfp_swap_involutive at 1; apply¬ RswapX; applys¬ Hr1.
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hfzp.
rewrite <- swap_gvar_right with (X´ := Y). auto.
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hfzq.
rewrite <- swap_gvar_right with (X´ := Y); simpls; rewrite¬ swap_involutive in Hfzq.
specializes Hr1 m Y; rewrite Heqabs in *; rewrite Heqabs´ in ×.
rewrite <- wfp_eq_swap_par in ×.
erewrite <- wfp_swap_involutive at 1; apply¬ RswapX; applys¬ Hr1.
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hfzp.
rewrite <- swap_gvar_left with (X := X); auto.
apply gfresh_swap_inv with (X := X) (X´ := Y) in Hfzq.
rewrite <- swap_gvar_left with (X := X); simpls; rewrite¬ swap_involutive in Hfzq.
assert (Heqabsq´´ : ∀ r : wfprocess, (wfp_Abs m Z (wfp_swap X Y r)) = wfp_swap X Y (wfp_Abs m Z r)).
assert (Heq : {{X, Y}}Z = Z).
unfold swap_gvar; repeat cases_if×.
introv; rewrite wfp_eq_swap_abs. rewrite¬ Heq.
specializes Hr1 m Z; rewrite Heqabsq´´ in ×.
rewrite <- wfp_eq_swap_par in ×.
erewrite <- wfp_swap_involutive at 1; apply¬ RswapX; applys¬ Hr1;
replace Z with ({{X, Y}}Z) by (unfold swap_gvar; repeat cases_if*).
applys¬ gfresh_swap_inv.
rewrite <- (swap_involutive X Y q´´).
applys¬ gfresh_swap_inv.
forwards Ht´: wfp_trans_swap_chan_out m n Ht; lets Ht´´ : Ht´; simpl in Ht´, Ht´´.
rewrite wfp_swap_chan_involutive in Ht´´.
edestruct (IHHr ({{|m, n|}}a) (wfp_swap_chan m n p´) (wfp_swap_chan m n p´´)) as (q´ & q´´ & Htq & Hr1). assumption. clear IHHr.
∃ (wfp_swap_chan m n q´) (wfp_swap_chan m n q´´); splits.
replace a with ({{|m, n|}}({{|m, n|}}a)) by (unfold swap_name; repeat cases_if*; rewrite <- e0; rewrite¬ <- e).
applys¬ wfp_trans_swap_chan_out.
intros c Z Hfcp Hfcq Hfzp Hfzq. simpl in Hfzq, Hr1. rewrite <- fresh_gvar_swap_chan in ×.
assert (Heqabs : ∀ m n X r, (wfp_Abs m X (wfp_swap_chan m n r)) = wfp_swap_chan m n (wfp_Abs n X r)).
introv; rewrite wfp_eq_swap_chan_abs.
unfold swap_name; repeat cases_if*; substs¬.
assert (Heqabs´ : ∀ m n X r, (wfp_Abs n X (wfp_swap_chan m n r)) = wfp_swap_chan m n (wfp_Abs m X r)).
introv; rewrite wfp_eq_swap_chan_abs.
unfold swap_name; repeat cases_if*; substs¬.
elim (classic (c = m)); elim (classic (c = n)); introv Heqm Heqn; subst.
subst n; repeat rewrite wfp_swap_chan_equal in *; repeat rewrite swap_chan_equal in *; applys¬ Hr1.
specializes Hr1 n Z; rewrite Heqabs in *; rewrite Heqabs´ in ×.
rewrite <- wfp_eq_swap_chan_par in ×.
erewrite <- wfp_swap_chan_involutive at 1; apply¬ Rswapm; applys¬ Hr1.
apply wfp_fresh_chan_cswap with (m := m) (n := n) in Hfcp.
unfold swap_name in Hfcp; repeat cases_if*; rewrite¬ wfp_swap_chan_involutive in Hfcp.
apply wfp_fresh_chan_cswap with (m := m) (n := n) in Hfcq.
unfold swap_name in Hfcq; repeat cases_if*; rewrite¬ wfp_swap_chan_involutive in Hfcq.
applys¬ wfp_fresh_gvar_cswap.
specializes Hr1 m Z; rewrite Heqabs in *; rewrite Heqabs´ in ×.
rewrite <- wfp_eq_swap_chan_par in ×.
erewrite <- wfp_swap_chan_involutive at 1; apply¬ Rswapm; applys¬ Hr1.
apply wfp_fresh_chan_cswap with (m := m) (n := n) in Hfcp.
unfold swap_name in Hfcp; repeat cases_if*; rewrite¬ wfp_swap_chan_involutive in Hfcp.
apply wfp_fresh_chan_cswap with (m := m) (n := n) in Hfcq.
unfold swap_name in Hfcq; repeat cases_if*; rewrite¬ wfp_swap_chan_involutive in Hfcq.
applys¬ wfp_fresh_gvar_cswap.
assert (Heqabsq´´ : ∀ X r, (wfp_Abs c X (wfp_swap_chan m n r)) = wfp_swap_chan m n (wfp_Abs c X r)).
assert (Heq : {{|m, n|}}c = c).
unfold swap_name; repeat cases_if×.
introv; rewrite wfp_eq_swap_chan_abs. rewrite¬ Heq.
assert (Heqc : {{|m, n|}}c = c) by (unfold swap_name; repeat cases_if*).
apply wfp_fresh_chan_cswap with (m := m) (n := n) in Hfcp; apply (wfp_fresh_chan_cswap) with (m := m) (n := n) in Hfcq.
rewrite wfp_swap_chan_involutive in *; rewrite Heqc in ×.
apply wfp_fresh_gvar_cswap with (m := m) (n := n) in Hfzp.
specialize (Hr1 c Z Hfcp Hfcq Hfzp Hfzq); rewrite Heqabsq´´ in ×.
rewrite <- wfp_eq_swap_chan_par in ×.
erewrite <- wfp_swap_chan_involutive at 1; apply¬ Rswapm; applys¬ Hr1;
replace Z with ({{X, Y}}Z) by (unfold swap_gvar; repeat cases_if*).
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). eapply HR4 in H; auto.
edestruct (H a fp Ht) as (fq & Htq & Z & Hf1 & Hf2 & Hrq).
∃ fq; splits¬.
introv Hf3 Hf4.
forwards Hre1: wfp_inst_swap (wfp_Gvar Z) Hf1 Hf3 Ht.
simpl in Hre1... cases_if×.
forwards Hre2: wfp_inst_swap (wfp_Gvar Z) Hf2 Hf4 Htq.
simpl in Hre2... cases_if×.
rewrite <- Hre1, <- Hre2. apply¬ RswapX.
rename fp into fp0.
forwards (fp & Ht´ & Heq1): wfp_trans_swap_in a X Y Ht.
simpl in Ht´; rewrite wfp_swap_involutive in Ht´.
specialize (IHHr a fp Ht´). destruct IHHr as (fq & Htq & Hr´).
forwards (fq0 & Htq´ & Heq2): wfp_trans_swap_in a X Y Htq.
∃ fq0. splits¬.
introv Hf3 Hf4.
rewrite <- (wfp_swap_involutive X Y).
assert (Hre1: wfp_inst_Abs fp0 (wfp_Gvar X0) = wfp_swap X Y (wfp_inst_Abs fp (wfp_swap X Y (wfp_Gvar X0)))).
rewrite <- Heq1. symmetry. apply wfp_swap_involutive.
assert (Hre2: wfp_inst_Abs fq0 (wfp_Gvar X0) = wfp_swap X Y (wfp_inst_Abs fq (wfp_swap X Y (wfp_Gvar X0)))).
rewrite Heq2. rewrite¬ wfp_swap_involutive.
rewrite Hre1, Hre2.
eapply gfresh_swap_inv in Hf3; simpls; rewrite swap_involutive in Hf3.
eapply gfresh_swap_inv in Hf4; simpls; rewrite swap_involutive in Hf4.
apply RswapX. rewrite wfp_swap_involutive.
assert (Haux : ∀ X Y Z, wfp_swap X Y (wfp_Gvar Z) = wfp_Gvar ({{X, Y}}Z)) by (introv; rewrite_wfp_swap; unfold swap_gvar; repeat cases_if*).
rewrite Haux; apply (Hr´ ({{X, Y}}X0) Hf3 Hf4).
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 _ fp Ht´). destruct IHHr as (fq & Htq & Hr´).
forwards (fq0 & Htq´ & Heq2): wfp_trans_swap_chan_in ({{|m, n|}}a) m n Htq.
rewrite swap_name_involutive in Htq´.
∃ fq0; splits¬.
introv Hf3 Hf4.
apply (wfp_fresh_gvar_cswap) with (m := m) (n := n) in Hf3; rewrite wfp_swap_chan_involutive in Hf3.
apply (wfp_fresh_gvar_cswap) with (m := m) (n := n) in Hf4; rewrite wfp_swap_chan_involutive in Hf4.
specializes Hr´ Hf3 Hf4.
rewrite <- wfp_eq_swap_chan_gvar with (m := m) (n := n) at 2; rewrite <- Heq2.
specializes Heq1 (wfp_Gvar X). rewrite <- wfp_swap_chan_involutive with (m := m) (n := n) (p := wfp_inst_Abs fp0 _). rewrite Heq1...
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). eapply HR5 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¬ RswapX.
forwards Ht´: wfp_trans_swap_chan_rem m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
edestruct (IHHr _ (wfp_swap_chan m n p´) Ht´) as (q´ & Htq & Hr´).
∃ (wfp_swap_chan m n q´). split.
apply¬ wfp_trans_swap_chan_rem.
erewrite <- wfp_swap_chan_involutive at 1. apply¬ Rswapm.
Qed.
Inductive R_trans_on : binary wfprocess :=
| Rtrans_on : ∀ p q r, p ≈ONOR q → q ≈ONOR r → R_trans_on p r.
Lemma ONORbis_trans : Transitive ONORbis.
Proof.
intros p q r Hio1 Hio2.
rewrite (ONOR_ONOR_ex).
∃ R_trans_on. split×.
clear p q r Hio1 Hio2. splits.
introv Hr; inverts Hr; econstructor; applys× ONORbis_sym.
introv Hr Ht; inverts Hr.
lets (q0´ & Htq0´ & Honq0´) : ONORbis_tau H Ht.
lets (q´ & Htq´ & Honq´ ) : ONORbis_tau H0 Htq0´.
∃ q´; splits¬.
econstructor; eassumption.
introv Hr Ht; inverts Hr.
lets (q0´ & q0´´ & Htq0 & Htonq0) : ONORbis_out_normal H Ht.
lets (q´ & q´´ & Htq & Htonq ) : ONORbis_out_normal H0 Htq0.
∃ q´ q´´; splits¬.
lets (m & Hfm) : find_fresh_chan (proc p :: proc q0 :: proc q :: nil); rewrite Forall_to_conj_3 in Hfm.
lets (X & HfX) : find_fresh (proc p :: proc q0 :: proc q :: nil); rewrite Forall_to_conj_3 in HfX.
destruct Hfm as (Hfmp & Hfmq0 & Hfmq); destruct HfX as (Hfxp & Hfxq0 & Hfxq).
assert (Hfxp´´ : X # p´´).
lets Hgv : GV_trans_out Ht.
intros Hin; apply Hfxp.
rewrite Hgv; rewrite¬ in_union.
assert (Hfxq0´´ : X # q0´´).
lets Hgv : GV_trans_out Htq0.
intros Hin; apply Hfxq0.
rewrite Hgv; rewrite¬ in_union.
assert (Hfxq´´ : X # q´´).
lets Hgv : GV_trans_out Htq.
intros Hin; apply Hfxq.
rewrite Hgv; rewrite¬ in_union.
∃ m X; splits×. econstructor.
applys× Htonq0. applys× Htonq.
unfold in_relation. introv Hr Ht. inverts Hr.
lets (fq0 & Ht2 & Hq0): (ONORbis_in p q0 H a fp Ht).
lets (fq & Htq & Hq): (ONORbis_in q0 q H0 a fq0 Ht2).
∃ fq; splits×.
lets (X & HfX) : find_fresh (proc p :: proc q0 :: proc q :: nil); rewrite Forall_to_conj_3 in HfX.
∃ X; splits×.
econstructor; [apply× Hq0 | apply× Hq]; jauto.
unfold var_relation. introv Hr; introv Ht. inverts Hr.
lets (q0´ & Ht2 & Hq0): (ONORbis_var p q0 H X p´ Ht).
lets (q´ & Htq´ & Hq): (>> ONORbis_var q0 q H0 X q0´ Ht2).
∃ q´. split*; econstructor; eassumption.
econstructor; eassumption.
Qed.
Instance ONORbis_is_eq_rel : Equivalence ONORbis.
Proof.
split. apply ONORbis_refl. apply ONORbis_sym. apply ONORbis_trans.
Qed.
Hint Resolve ONORbis_refl ONORbis_sym ONORbis_trans.
Ltac resolve_up_to := applys× up_to_eq.
Lemma R_ONORbis_up_to_up_to_R_ONORbis_ex : ∀ Re R,
Transitive Re → OpenNormal_bisimulation Re →
OpenNormal_bisimulation_up_to Re R → OpenNormal_bisimulation_ex (up_to Re R).
Proof.
introv HTrRe HRe HR.
inversion HRe as (HRe1 & HRe2 & HRe3 & HRe4 & HRe5).
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). 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).
lets (p1´ & Htp1´ & Hrep1´) : HRe2 Hre1 Ht.
lets (q1´ & Htq1´ & Hreq1´) : HR2 Htp1´. apply Hr1.
lets (q´ & Htq & Hrq) : HRe2 Htq1´. apply Hre2.
∃ q´; splits×.
inverts Hreq1´; destruct H as (pp & qq & H).
constructor; ∃ pp qq; splits; jauto.
introv Hr Ht; inverts Hr.
destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
lets (p1´ & p1´´ & Htp1 & Hrep1) : HRe3 Hre1 Ht.
lets (q1´ & q1´´ & Htq1 & Hreq1) : HR3 Htp1. apply Hr1.
lets (q´ & q´´ & Htq & Hrq) : HRe3 Htq1. apply Hre2.
∃ q´ q´´; splits×.
lets (m & Hfm) : find_fresh_chan (proc p :: proc p1 :: proc q1 :: proc q :: nil); rewrite Forall_to_conj_4 in Hfm.
lets (X & HfX) : find_fresh (proc p :: proc p1 :: proc q1 :: proc q :: nil); rewrite Forall_to_conj_4 in HfX.
destruct Hfm as (Hfmp & Hfmp1 & Hfmq1 & Hfmq); destruct HfX as (Hfxp & Hfxp1 & Hfxq1 & Hfxq).
assert (Hfxp´´ : X # p´´).
lets Hgv : GV_trans_out Ht.
intros Hin; apply Hfxp.
rewrite Hgv; rewrite¬ in_union.
assert (Hfxp1´´ : X # p1´´).
lets Hgv : GV_trans_out Htp1.
intros Hin; apply Hfxp1.
rewrite Hgv; rewrite¬ in_union.
assert (Hfxq1´´ : X # q1´´).
lets Hgv : GV_trans_out Htq1.
intros Hin; apply Hfxq1.
rewrite Hgv; rewrite¬ in_union.
assert (Hfxq´´ : X # q´´).
lets Hgv : GV_trans_out Htq.
intros Hin; apply Hfxq.
rewrite Hgv; rewrite¬ in_union.
∃ m X; splits×.
specializes¬ Hreq1 Hfxq1´´. specializes¬ Hrq Hfxq´´.
inverts Hreq1; destruct H as (pp & qq & H).
constructor; ∃ pp qq; splits×.
introv Hr; introv H. inverts Hr.
destruct H0 as (p1 & q1 & Hre1 & Hre2 & Hr1).
generalize (HRe4 p p1 Hre1 a fp H); intro HRe2´; destruct HRe2´ as (fp1 & Ht1 & Hre1´).
specialize (HR4 p1 q1 Hr1 a fp1 Ht1). destruct HR4 as (fq1 & Ht2 & Hr2).
specialize (HRe4 q1 q Hre2 a fq1 Ht2). destruct HRe4 as (fq & Ht3 & Hre2´).
∃ fq. splits¬.
lets (X & HfX) : find_fresh (proc p :: proc p1 :: proc q1 :: proc q :: nil); rewrite Forall_to_conj_4 in HfX.
destruct HfX as (Hfxp & Hfxp1 & Hfxq1 & Hfxq).
∃ X; splits×.
specializes¬ Hr2 Hfxq1. inverts Hr2. destruct H0 as (p1´ & q1´ & Hre1´´ & Hre2´´& Hr1´).
specializes¬ Hre1´ Hfxp1; specializes¬ Hre2´ Hfxq.
constructor. ∃ p1´ q1´. split×.
introv Hr; introv Ht. inverts Hr. destruct H as (p1 & q1 & Hre1 & Hre2 & Hr1).
forwards¬ HRe4´: HRe5 Hre1 Ht. destruct HRe4´ as (p1´ & Ht1 & Hre1´).
specializes HR5 Hr1 Ht1. destruct HR5 as (q1´ & Ht2 & Hre2´).
specializes HRe5 Hre2 Ht2. destruct HRe5 as (q´ & Ht3 & Hre3).
∃ q´. split¬.
inverts Hre2´. destruct H as (p3´ & q3´ & Hre10 & Hre11 & Hr10).
constructor. ∃ p3´ q3´. splits×.
Qed.
Lemma ONORbis_up_to_ONORbis : ∀ Re,
OpenNormal_bisimulation Re →
Equivalence Re → ∀ p q, (ONORbis_up_to Re p q ↔ ONORbis p q).
Proof.
introv HEqRe HRe. introv; split; intros Hon; destruct Hon as (R & HR & Hr).
rewrite ONOR_ONOR_ex.
∃ (up_to Re R). split.
applys× R_ONORbis_up_to_up_to_R_ONORbis_ex.
applys× up_to_eq.
∃ R. split¬. clear p q Hr.
destruct HR as (HR1 & HR2 & HR3 & HR4 & HR5). splits¬.
introv Hr Ht. forwards¬ (q´ & Ht´ & Hr´) : HR2 p q Ht.
∃ q´; split¬. applys× up_to_eq.
introv Hr Ht; forwards¬ (q´ & q´´ & Ht´ & Hr´) : HR3 p q Ht.
∃ q´ q´´; splits~; intros; applys× up_to_eq.
introv Hr Ht. forwards¬ (fq & Ht´ & Hf): HR4 p q Hr a fp.
∃ fq. splits¬. introv Hf1 Hf2; applys× up_to_eq.
introv Hr; introv Ht. forwards¬ (q´ & Ht´ & Hr´): HR5 Hr Ht.
∃ q´. split¬. applys× up_to_eq.
Qed.
Lemma ONORbis_up_to_cgr_ONORbis : ∀ p q, (ONORbis_up_to wfcgr p q ↔ ONORbis p q).
Proof.
apply ONORbis_up_to_ONORbis; eauto with congr_bisim.
Qed.
Fixpoint iter_abs_par (ms : list chan) (xs : list var) (pks : list wfprocess) (p : wfprocess) :=
match ms, xs, pks with
| nil, nil, nil ⇒ p
| cons m ms, cons X xs, cons pk pks ⇒ (wfp_Par (wfp_Abs m X pk) (iter_abs_par ms xs pks p))
| _, _, _ ⇒ wfp_Nil
end.
Fixpoint iter_abs_par_abs (ms : list chan) (xs : list var) (pks : list wfprocess) (fp : abstraction) :=
match ms, xs, pks with
| nil, nil, nil ⇒ fp
| cons m ms, cons X xs, cons pk pks ⇒ (AbsPar2 (wfp_Abs m X pk) (iter_abs_par_abs ms xs pks fp))
| _, _, _ ⇒ fp
end.
Lemma fresh_iter_abs_par : ∀ (X : var) (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n → (X # iter_abs_par ms xs pks p → X # p).
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks Hf.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls¬.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
rewrite gfresh_par_iff in Hf. applys× (IHn ms xs pks).
Qed.
Lemma cfresh_iter_abs_par : ∀ (m : chan) (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n →
(m ### iter_abs_par ms xs pks p ↔ Forall (fun m´ ⇒ m ≠ m´) ms ∧ Forall (fun (p : wfprocess) ⇒ m ### p) pks ∧ m ### p).
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst;
simpls; splits; intro Hyp; jauto; splits~; apply Forall_nil.
rename m into M.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpl iter_abs_par; splits; intro Hyp.
rewrite wfp_cfresh_par_iff in Hyp; inverts Hyp as (HfM1 & HfM2).
rewrite wfp_cfresh_Abs in H0.
simpls; rewrite IHn in H1; jauto; destruct H1 as (H1 & H2 & H3).
splits*; apply× Forall_cons; intuition.
destruct Hyp as (H1 & H2 & H3); inverts H1; inverts H2.
rewrite wfp_cfresh_par_iff; splits¬.
rewrite wfp_cfresh_Abs; splits¬.
rewrite× IHn. inverts¬ Hndms.
Qed.
Lemma trans_iter_abs_par_tau :
∀ (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n →
Forall (fun m ⇒ m ### p) ms →
Forall (fun (pk : wfprocess) ⇒ Forall (fun m ⇒ m ### pk) ms) pks →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs pks) →
∀ (ip´ : wfprocess), {{iter_abs_par ms xs pks p -- Tau ->> AP ip´}} →
∃ (p´ : wfprocess), {{p -- Tau ->> AP p´}} ∧ ip´ = iter_abs_par ms xs pks p´.
Proof with automate.
inductions n; introv Hndms Hlms Hlxs Hlpks Hfmsp Hfmspks Hfxspks Hit.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls; ∃× ip´.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
inverts Hit; subst_wfp; try solve [inverts H2]...
destruct aq; inverts H3.
apply IHn in H2;
try solve [rew_length in *; nat_math];
try solve [inverts× Hfmsp];
try solve [inverts× Hfxspks].
destruct H2 as (p´´ & Htp´´ & Heq); subst; ∃ p´´; splits¬.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmspks; introv Hm.
assert (Hm´ : Mem x0 (pk :: pks)) by constructor~; specializes Hfmspks Hm´.
inverts¬ Hfmspks.
assert (Hfm : m ### iter_abs_par ms xs pks p).
rewrite cfresh_iter_abs_par with (n := n); jauto; splits.
rewrite <- Forall_Mem; introv Hm Heq; subst; intuition.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmspks.
introv Hm; assert (Hm´ : Mem x0 (pk :: pks)) by constructor~; specializes Hfmspks Hm´; inverts¬ Hfmspks.
inverts¬ Hfmsp.
apply false_trans_out with (p´ := (AP q´)) (p´´ := q´´) in Hfm; intuition.
inverts× H2.
Qed.
Lemma trans_iter_abs_par_out :
∀ (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n →
Forall (fun m ⇒ m ### p) ms →
Forall (fun (pk : wfprocess) ⇒ Forall (fun m ⇒ m ### pk) ms) pks →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs pks) →
∀ (ip´ p´´ : wfprocess) (a : chan), {{iter_abs_par ms xs pks p -- LabOut a p´´ ->> AP ip´}} →
∃ (p´ : wfprocess), {{p -- LabOut a p´´ ->> AP p´}} ∧ ip´ = iter_abs_par ms xs pks p´.
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks Hfmsp Hfmspks Hfxspks Hit.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls~; ∃× ip´.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
inverts Hit; subst_wfp; try solve [inverts H2].
lets (q´ & Heq) : wfp_agent_out H2; subst.
apply IHn in H2;
try solve [rew_length in *; nat_math];
try solve [inverts× Hfmsp];
try solve [inverts× Hfxspks].
destruct H2 as (p´ & Htp´´ & Heq); subst; ∃ p´; splits¬.
simpl in H3; inverts¬ H3.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmspks; introv Hm.
assert (Hm´ : Mem x0 (pk :: pks)) by constructor~; specializes Hfmspks Hm´.
inverts¬ Hfmspks.
Qed.
Lemma trans_iter_abs_par_in :
∀ (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n →
Forall (fun m ⇒ m ### p) ms →
Forall (fun (pk : wfprocess) ⇒ Forall (fun m ⇒ m ### pk) ms) pks →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs pks) →
∀ (fp´ : abstraction) (a : chan),
Forall (fun m ⇒ m ≠ a) ms →
{{iter_abs_par ms xs pks p -- LabIn a ->> AA fp´}} →
∃ (fp : abstraction), {{p -- LabIn a ->> AA fp}} ∧ fp´ = iter_abs_par_abs ms xs pks fp.
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks Hfmsp Hfmspks Hfxspks Hneqa Hit.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls; ∃× fp´.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
inverts Hit; subst_wfp; try solve [inverts H2].
inverts H2; inverts× Hneqa.
lets (q´ & Heq) : wfp_agent_in H2; subst.
apply IHn in H2;
try solve [rew_length in *; nat_math];
try solve [inverts× Hfmsp];
try solve [inverts× Hfxspks].
destruct H2 as (p´´ & Htp´´ & Heq); subst; ∃ p´´; splits¬.
simpl in H3; inverts¬ H3.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmspks; introv Hm.
assert (Hm´ : Mem x0 (pk :: pks)) by constructor~; specializes Hfmspks Hm´.
inverts¬ Hfmspks.
inverts¬ Hneqa.
Qed.
Lemma trans_iter_abs_par_inst_abs :
∀ (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess)
(a : chan) (fp : abstraction),
noDup ms →
length ms = n → length xs = n → length pks = n →
Forall (fun m ⇒ m ≠ a) ms →
∀ (Htp : {{p -- LabIn a ->> AA fp}}),
{{iter_abs_par ms xs pks p -- LabIn a ->> AA (iter_abs_par_abs ms xs pks fp)}} ∧
∀ (X : var),
iter_abs_par ms xs pks (wfp_inst_Abs fp (wfp_Gvar X)) =
wfp_inst_Abs (iter_abs_par_abs ms xs pks fp) (wfp_Gvar X).
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks Hmsneq Ht.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst×.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
splits; simpls.
apply act2_in. applys× IHn. inverts¬ Hmsneq.
introv; fequals. applys× IHn. inverts¬ Hmsneq.
Qed.
Lemma trans_iter_abs_par_rem :
∀ (p : wfprocess) (n : nat) (ms : list chan) (xs : list var) (pks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n →
Forall (fun m ⇒ m ### p) ms →
Forall (fun (pk : wfprocess) ⇒ Forall (fun m ⇒ m ### pk) ms) pks →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs pks) →
∀ (ip´ : wfprocess) (X : var), {{iter_abs_par ms xs pks p -- LabRem X ->> AP ip´}} →
∃ (p´ : wfprocess), {{p -- LabRem X ->> AP p´}} ∧ ip´ = iter_abs_par ms xs pks p´.
Proof.
inductions n; introv Hndms Hlms Hlxs Hlpks Hfmsp Hfmspks Hfxspks Hit.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls; ∃× ip´.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
inverts Hit; subst_wfp; try solve [inverts H2].
lets (q´ & Heq) : wfp_agent_rem H2; subst.
apply IHn in H2;
try solve [rew_length in *; nat_math];
try solve [inverts× Hfmsp];
try solve [inverts× Hfxspks].
destruct H2 as (p´´ & Htp´´ & Heq); subst; ∃ p´´; splits¬.
inverts× H3.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmspks; introv Hm.
assert (Hm´ : Mem x0 (pk :: pks)) by constructor~; specializes Hfmspks Hm´.
inverts¬ Hfmspks.
Qed.
Lemma iter_abs_par_congr : ∀ n ms xs pks p p´,
noDup ms →
length ms = n → length xs = n → length pks = n →
(wfp_Par p (iter_abs_par ms xs pks p´)) ≡* (iter_abs_par ms xs pks (wfp_Par p p´)).
Proof.
inductions n; introv Hnd Hlms Hlxs Hlpks.
apply length0 in Hlms; apply length0 in Hlxs; apply length0 in Hlpks; subst; simpls; repeat constructor×.
lets Hlms´ : Hlms; apply lengthn in Hlms´; destruct Hlms´ as (m & ms´ & Heq); subst; rename ms´ into ms.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
simpls.
destruct Hnd as (_ & Hnd).
assert (Heql1 : length ms = n) by auto.
assert (Heql2 : length xs = n) by auto.
assert (Heql3 : length pks = n) by auto.
specializes IHn p p´ Hnd.
specializes IHn Heql1 Heql2 Heql3.
etransitivity. constructor. apply WfCgrPar_assoc1.
apply transitivity with (y := wfp_Par (wfp_Par (wfp_Abs m x pk) p) (iter_abs_par ms xs pks p´)).
applys× wfcgr_par; [constructor; apply WfCgrPar_com | reflexivity].
etransitivity. constructor. apply WfCgrPar_assoc2.
applys× wfcgr_par. reflexivity.
Qed.
Lemma iter_abs_par_fiddle : ∀ n ms xs pks p p´,
noDup ms →
length ms = n → length xs = n → length pks = n →
wfp_Par p (iter_abs_par ms xs pks p´) ≈ONOR (iter_abs_par ms xs pks (wfp_Par p p´)).
Proof.
introv Hnd Hlms Hlxs Hlpks.
∃ wfcgr; splits¬.
apply congr_ONORbisimulation.
applys¬ (iter_abs_par_congr n).
Qed.
Inductive RON : RelWfP :=
| RON_Main : ∀ (p q : wfprocess) (n : nat), n > 0 →
∀ (ms : list chan) (xs : list var) (pks : list wfprocess) (qks : list wfprocess),
noDup ms →
length ms = n → length xs = n → length pks = n → length qks = n →
Forall (fun m ⇒ m ### p) ms →
Forall (fun m ⇒ m ### q) ms →
Forall (fun (pk : wfprocess) ⇒ Forall (fun m ⇒ m ### pk) ms) pks →
Forall (fun (qk : wfprocess) ⇒ Forall (fun m ⇒ m ### qk) ms) qks →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs pks) →
Forall (fun (t : (var × wfprocess)) ⇒ fst(t) # snd(t)) (combine xs qks) →
(iter_abs_par ms xs pks p) ≈ONOR (iter_abs_par ms xs qks q) →
RON p q.
Lemma ONOR_RON : OpenNormal_bisimulation_ex RON.
Proof with automate.
splits.
introv Hr; inverts Hr.
eapply (RON_Main y x (length ms) _ ms xs qks pks); auto; applys¬ ONORbis_sym.
introv Hr Htp.
inverts Hr as Hndms Hlge Hlxs Hlpks Hlqks Hfmsp Hfmsq Hfmspks; intros Hfmsqks Hfxspks Hfxsqks HONiter.
assert (Hti : {{iter_abs_par ms xs pks p -- Tau ->> AP (iter_abs_par ms xs pks p´)}}).
clear HONiter Hfxsqks Hfxspks Hfmsqks Hfmspks Hfmsq Hfmsp Hlqks.
generalize dependent pks; generalize dependent xs; generalize dependent ms.
inductions ms; intros.
rew_length in *; nat_math.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
destruct ms.
assert (Heqxs : xs = nil) by (apply length0; rew_length in *; nat_math).
assert (Heqpks : pks = nil) by (apply length0; rew_length in *; nat_math).
subst; simpl...
remember (c :: ms) as ns. simpl. apply act2_tau.
eapply IHms.
simpl in Hndms; jauto.
rewrite Heqns; rew_length; nat_math.
rew_length in *; nat_math.
rew_length in *; nat_math.
lets (R & HONR & Hr) : HONiter.
lets (_ & Htau & _) : HONR.
lets (iq´ & Hti´ & Hr´) : Htau Hr Hti.
lets Hti´´ : Hti´; apply trans_iter_abs_par_tau with (n := length ms) in Hti´´; jauto.
destruct Hti´´ as (q´ & Htq & Heq); subst.
∃ q´; splits¬.
apply RON_Main with (n := length ms) (ms := ms) (xs := xs) (pks := pks) (qks := qks); jauto.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsp.
introv Hm; specializes Hfmsp Hm.
eapply wfp_cfresh_tau. apply Hfmsp. auto.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsq.
introv Hm; specializes Hfmsq Hm.
eapply wfp_cfresh_tau. apply Hfmsq. auto.
∃¬ R.
introv Hr Htp.
inverts Hr as Hndms Hlge Hlxs Hlpks Hlqks Hfmsp Hfmsq Hfmspks; intros Hfmsqks Hfxspks Hfxsqks HONiter.
assert (Htiq : {{iter_abs_par ms xs pks p -- LabOut a p´´ ->> AP (iter_abs_par ms xs pks p´)}}).
clear HONiter Hfxsqks Hfxspks Hfmsqks Hfmspks Hfmsq Hfmsp Hlqks.
generalize dependent pks; generalize dependent xs; generalize dependent ms.
inductions ms; intros.
rew_length in *; nat_math.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
destruct ms.
assert (Heqxs : xs = nil) by (apply length0; rew_length in *; nat_math).
assert (Heqpks : pks = nil) by (apply length0; rew_length in *; nat_math).
subst; simpl...
remember (c :: ms) as ns; simpl; apply act2_out.
eapply IHms.
simpl in Hndms; jauto.
rewrite Heqns; rew_length; nat_math.
rew_length in *; nat_math.
rew_length in *; nat_math.
lets (R & HONR & Hr) : HONiter.
lets (_ & _ & Hout & _) : HONR.
lets Hout_norm : Hout; apply out_nor_forall_exists in Hout.
lets (iq´ & q´´ & Htiq´ & m & X & Hf1 & Hf2 & Hf3 & Hf4 & Hr´) : Hout Hr Htiq.
lets Htiq´´ : Htiq´; apply trans_iter_abs_par_out with (n := length ms) in Htiq´´; jauto.
destruct Htiq´´ as (q´ & Htq & Heq); subst.
∃ q´ q´´; splits~; ∃ m X.
apply cfresh_iter_abs_par with (n := length ms) in Hf1; auto;
destruct Hf1 as (Hffp1 & Hffp2 & Hf1).
apply cfresh_iter_abs_par with (n := length ms) in Hf2; auto;
destruct Hf2 as (Hffq3 & Hffq4 & Hf2).
splits~; jauto.
assert (Hon : (wfp_Par (wfp_Abs m X p´´) (iter_abs_par ms xs pks p´)) ≈ONOR
(wfp_Par (wfp_Abs m X q´´) (iter_abs_par ms xs qks q´))) by ∃¬ R.
clear dependent R.
apply RON_Main with (n := length ms) (ms := ms) (xs := xs) (pks := pks) (qks := qks); jauto.
rewrite <- Forall_Mem in *; introv Hm.
specializes Hffp1 Hm; specializes Hfmsp Hm.
eapply wfp_cfresh_out in Hfmsp. Focus 2. apply Htp.
rewrite wfp_cfresh_par_iff; splits×.
rewrite wfp_cfresh_Abs; splits×.
rewrite <- Forall_Mem in *; introv Hm.
specializes Hffp1 Hm; specializes Hfmsq Hm.
eapply wfp_cfresh_out in Hfmsq. Focus 2. apply Htq.
rewrite wfp_cfresh_par_iff; splits×.
rewrite wfp_cfresh_Abs; splits×.
etransitivity. apply ONORbis_sym. eapply iter_abs_par_fiddle; try eassumption; auto.
etransitivity. Focus 2. eapply iter_abs_par_fiddle; try eassumption; auto.
auto.
introv Hr; intros a fp Htp.
inverts Hr as Hndms Hlge Hlxs Hlpks Hlqks Hfmsp Hfmsq Hfmspks; intros Hfmsqks Hfxspks Hfxsqks HONiter.
assert (Hti : {{iter_abs_par ms xs pks p -- LabIn a ->> AA (iter_abs_par_abs ms xs pks fp)}}).
clear HONiter Hfxsqks Hfxspks Hfmsqks Hfmspks Hfmsq Hfmsp Hlqks.
generalize dependent pks; generalize dependent xs; generalize dependent ms.
inductions ms; intros.
rew_length in *; nat_math.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
destruct ms.
assert (Heqxs : xs = nil) by (apply length0; rew_length in *; nat_math).
assert (Heqpks : pks = nil) by (apply length0; rew_length in *; nat_math).
subst; simpl...
remember (c :: ms) as ns; simpl; apply act2_in.
eapply IHms.
simpl in Hndms; jauto.
rewrite Heqns; rew_length; nat_math.
rew_length in *; nat_math.
rew_length in *; nat_math.
lets (R & HONR & Hr) : HONiter.
lets (_ & _ & _ & Hin & _) : HONR.
apply in_forall_exists in Hin.
lets (ifq & Htfq & X & Hfx1 & Hfx2 & Hr´) : (Hin _ _ Hr _ _ Hti).
assert (Hfmms : Forall (fun m ⇒ m ≠ a) ms).
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsp.
introv Hm; specializes Hfmsp Hm.
introv Heq; subst; gen Htp.
applys¬ false_trans_in.
lets Htfq´ : Htfq; apply trans_iter_abs_par_in with (n := length ms) in Htfq´; jauto.
destruct Htfq´ as (fq & Htq & Heq); subst.
∃ fq; splits¬. ∃ X; splits.
apply fresh_iter_abs_par with (n := length ms) in Hfx1; jauto.
apply fresh_iter_abs_par with (n := length ms) in Hfx2; jauto.
apply RON_Main with (n := length ms) (ms := ms) (xs := xs) (pks := pks) (qks := qks); jauto.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsp.
introv Hm; specializes Hfmsp Hm.
eapply wfp_cfresh_in. apply Hfmsp. apply Htp. apply cfresh_gvar.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsq.
introv Hm; specializes Hfmsq Hm.
eapply wfp_cfresh_in. apply Hfmsq. apply Htq. apply cfresh_gvar.
lets (_ & Hyp) : trans_iter_abs_par_inst_abs pks Htp; try eassumption; auto.
rewrite Hyp.
lets (_ & Hyp´) : trans_iter_abs_par_inst_abs qks Htq; try eassumption; auto.
rewrite Hyp´.
∃ R; splits~; apply Hr´.
introv Hr; introv Htp.
inverts Hr as Hndms Hlge Hlxs Hlpks Hlqks Hfmsp Hfmsq Hfmspks; intros Hfmsqks Hfxspks Hfxsqks HONiter.
assert (Hti : {{iter_abs_par ms xs pks p -- LabRem X ->> AP (iter_abs_par ms xs pks p´)}}).
clear HONiter Hfxsqks Hfxspks Hfmsqks Hfmspks Hfmsq Hfmsp Hlqks.
generalize dependent pks; generalize dependent xs; generalize dependent ms.
inductions ms; intros.
rew_length in *; nat_math.
lets Hlxs´ : Hlxs; apply lengthn in Hlxs´; destruct Hlxs´ as (x & xs´ & Heq); subst; rename xs´ into xs.
lets Hlpks´ : Hlpks; apply lengthn in Hlpks´; destruct Hlpks´ as (pk & pks´ & Heq); subst; rename pks´ into pks.
destruct ms.
assert (Heqxs : xs = nil) by (apply length0; rew_length in *; nat_math).
assert (Heqpks : pks = nil) by (apply length0; rew_length in *; nat_math).
subst; simpl...
remember (c :: ms) as ns; simpl; apply act2_rem.
eapply IHms.
simpl in Hndms; jauto.
rewrite Heqns; rew_length; nat_math.
rew_length in *; nat_math.
rew_length in *; nat_math.
lets (R & HONR & Hr) : HONiter.
lets (_ & _ & _ & _ & Hvar) : HONR.
lets (iq´ & Hti´ & Hr´) : Hvar Hr Hti.
lets Hti´´ : Hti´; apply trans_iter_abs_par_rem with (n := length ms) in Hti´´; jauto.
destruct Hti´´ as (q´ & Htq & Heq); subst.
∃ q´; splits¬.
apply RON_Main with (n := length ms) (ms := ms) (xs := xs) (pks := pks) (qks := qks); jauto.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsp.
introv Hm; specializes Hfmsp Hm.
eapply wfp_cfresh_rem. apply Hfmsp. apply Htp.
rewrite <- Forall_Mem; rewrite <- Forall_Mem in Hfmsq.
introv Hm; specializes Hfmsq Hm.
eapply wfp_cfresh_rem. apply Hfmsq. apply Htq.
∃¬ R.
Grab Existential Variables.
auto.
Qed.
Lemma lemma415a : ∀ (p p´ q q´ : wfprocess), ∀ m X,
m ### p → m ### q →
m ### p´ → m ### q´ →
X # p´ → X # q´ →
(wfp_Par (wfp_Abs m X p´) p) ≈ONOR (wfp_Par (wfp_Abs m X q´) q) →
p ≈ONOR q.
Proof.
introv Hfmp Hfmq Hfmp´ Hfmq´ Hfxp´ Hfxq´ Hon.
rewrite ONOR_ONOR_ex.
∃ RON; splits¬.
apply ONOR_RON.
eapply (RON_Main p q 1 _ (m :: nil) (X :: nil) (p´ :: nil) (q´ :: nil));
try solve [rew_length; nat_math]; simpls~;
repeat rewrite¬ Forall_to_conj_1; splits¬.
intro Hm; inverts Hm.
Grab Existential Variables.
nat_math.
Qed.
Lemma sizeP_0_congr_nil : ∀ (p : wfprocess),
sizeP p = 0 → p ≡* wfp_Nil.
Proof.
induction p using wfp_ind_gen; introv Hs;
simpls; try solve [nat_math]; try reflexivity.
assert (Hsp1 : sizeP p1 = 0) by nat_math; assert (Hsp2 : sizeP p2 = 0) by nat_math.
specialize (IHp1 Hsp1); specialize (IHp2 Hsp2); clear Hs Hsp1 Hsp2.
inductions IHp1. rename x into p.
etransitivity. Focus 2. constructor. apply WfCgrPar_nil2.
applys× wfcgr_par; constructor¬.
etransitivity. Focus 2. constructor. apply WfCgrPar_nil2.
applys× wfcgr_par.
etransitivity; eassumption.
Qed.
Lemma wfp_sizeP_out_S_tr : ∀ (p : wfprocess),
wfp_sizeP_out 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; constructor.
branch 2. ∃ a. eexists. econstructor.
branch 1. ∃ X wfp_Nil; constructor.
assert (Hsize : wfp_sizeP_out p1 > 0 ∨ wfp_sizeP_out p2 > 0).
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO in *; simpls; nat_math.
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_out in Ht; simpls; unfold wfp_sizeO in Ht; simpls; nat_math.
introv Ht; unfold wfp_sizeP_out, 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 lemma415b : ∀ (p p´ q q´ : wfprocess), ∀ m X,
m ### p → m ### q →
m ### p´ → m ### q´ →
X # p´ → X # q´ →
(wfp_Par (wfp_Abs m X p´) p) ≈ONOR (wfp_Par (wfp_Abs m X q´) q) →
p´ ≈ONOR q´.
Proof with automate.
induction p using (measure_induction wfp_sizeP_out).
introv Hfmp Hfmq Hfmp´ Hfmq´ Hfxp´ Hfxq´ Hon.
lets H415a : lemma415a Hon; try eassumption.
elim (classic (wfp_sizeP_out p = 0)); introv Hneq.
clear H.
assert (Hnotp : ¬ wfp_sizeP_out p > 0) by nat_math.
rewrite wfp_sizeP_out_S_tr in Hnotp; rew_logic in Hnotp.
unfold wfp_sizeP_out in Hneq.
assert (HsizePp : wfp_sizeP p = 0) by nat_math.
assert (HsizeOp : wfp_sizeO p = 0) by nat_math.
unfold wfp_sizeP in HsizePp; apply sizeP_0_congr_nil in HsizePp.
assert (HqNil : q ≡* wfp_Nil).
apply sizeP_0_congr_nil.
cut (¬ wfp_sizeP_out q > 0).
introv Hn; unfold wfp_sizeP_out, wfp_sizeP in Hn; nat_math.
rewrite wfp_sizeP_out_S_tr; intro Hex.
inverts Hnotp as HnR [HnI HnO]; symmetry in H415a.
inverts Hex.
destruct H as (Y & qY & Htq).
lets (pY & Htp & _) : ONORbis_var H415a Htq.
specialize (HnR Y); rew_logic in HnR; specialize (HnR pY); auto.
inverts H.
destruct H0 as (a & fq & Htq).
lets Hin : ONORbis_in H415a. specialize (Hin _ _ Htq).
destruct Hin as (fp & Htp & _).
specialize (HnI a); rew_logic in HnI; specialize (HnI fp); auto.
destruct H0 as (a & q´´ & q´´´ & Htq).
lets (p´´ & p´´´ & Htp & _) : ONORbis_out_normal H415a Htq.
specialize (HnO a); rew_logic in HnO; specialize (HnO p´´); rew_logic in HnO; specialize (HnO p´´´); auto.
assert (HnoPQ : wfp_Abs m X p´ ≈ONOR wfp_Abs m X q´).
apply transitivity with (wfp_Par (wfp_Abs m X p´) wfp_Nil).
∃ wfcgr; splits; try apply congr_ONORbisimulation; repeat constructor.
apply transitivity with (wfp_Par (wfp_Abs m X q´) wfp_Nil).
Focus 2. ∃ wfcgr; splits; try apply congr_ONORbisimulation; repeat constructor.
apply transitivity with (wfp_Par (wfp_Abs m X p´) p).
∃ wfcgr; splits; try apply congr_ONORbisimulation.
applys× wfcgr_par; reflexivity.
apply transitivity with (wfp_Par (wfp_Abs m X q´) q); auto.
∃ wfcgr; splits; try apply congr_ONORbisimulation.
applys× wfcgr_par; try reflexivity; symmetry; auto.
clear dependent p; clear dependent q.
assert (∃ afp, {{wfp_Abs m X p´ -- LabIn m ->> AA afp}}).
eexists. simpls; constructor.
destruct H as (afp & Htap).
lets Hin : ONORbis_in HnoPQ. specialize (Hin _ _ Htap).
destruct Hin as (afq & Htaq & Hr).
lets (Y & Hy) : find_fresh ((proc (wfp_Abs m X p´)) :: (proc (wfp_Abs m X q´) :: nil)). rewrite Forall_to_conj_2 in Hy.
destruct Hy as (Hy1 & Hy2); specialize (Hr _ Hy1 Hy2).
replace (wfp_inst_Abs afp (wfp_Gvar Y)) with p´ in Hr.
replace (wfp_inst_Abs afq (wfp_Gvar Y)) with q´ in Hr; auto.
apply wfp_trans_in_abs_eq in Htaq; inverts Htaq as Htaq;
[ | destruct Htaq as (Z & Hneqz & Hfz & Heq); subst];
rewrite wfp_gfresh_Abs in *; simpl; inverts Hy1; inverts× Hy2;
try solve [try rewrite¬ <- wfp_subst_decomposition_g;
rewrite¬ wfp_subst_gvar_idem];
try solve [try rewrite¬ <- wfp_subst_decomposition_g;
rewrite¬ wfp_gfresh_subst_rewrite].
apply wfp_trans_in_abs_eq in Htap; inverts Htap as Htap;
[ | destruct Htap as (Z & Hneqz & Hfz & Heq); subst];
rewrite wfp_gfresh_Abs in *; simpl; inverts Hy1; inverts× Hy2;
try solve [try rewrite¬ <- wfp_subst_decomposition_g;
rewrite¬ wfp_subst_gvar_idem];
try solve [try rewrite¬ <- wfp_subst_decomposition_g;
rewrite¬ wfp_gfresh_subst_rewrite].
assert (Hotp : wfp_sizeP_out p > 0) by nat_math; clear Hneq.
rewrite wfp_sizeP_out_S_tr in Hotp.
inverts Hotp.
lets (Y & pY & Htp) : H0; clear H0.
assert (wfp_sizeP_out pY < wfp_sizeP_out p).
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO.
lets Hprs : sizeP_remove Htp; lets Hpro : sizeO_remove Htp; nat_math.
assert (Htparp : {{wfp_Par (wfp_Abs m X p´) p -- LabRem Y ->> AP (wfp_Par (wfp_Abs m X p´) pY)}})...
lets (ap´ & Htap & Hrap) : ONORbis_var Hon Htparp.
inverts Htap; subst_wfp.
inverts H4.
destruct aq; inverts H5.
assert ({{wfp_Par (wfp_Abs m X q´) q -- LabRem Y ->> AP (wfp_Par (wfp_Abs m X q´) w)}}) by (apply¬ act2_rem).
apply (H _ H0 p´ w q´ m X); auto.
eapply wfp_cfresh_rem. apply Hfmp. apply Htp.
eapply wfp_cfresh_rem. apply Hfmq. apply H4.
inverts H0.
destruct H1 as (a & fp & Htp).
assert (Htppar : {{wfp_Par (wfp_Abs m X p´) p -- LabIn a ->> AA (AbsPar2 (wfp_Abs m X p´) fp)}}) by (applys¬ act2_in).
lets Hin : ONORbis_in Hon. specialize (Hin _ _ Htppar).
destruct Hin as (fqpar & Htqpar & Hrpar).
inverts Htqpar...
inverts H3. false. eapply false_trans_in. apply Hfmp. apply Htp.
destruct aq; inverts H4.
lets (Y & HY) : find_fresh ((proc (wfp_Par (wfp_Abs m X p´) p)) :: (proc (wfp_Par (wfp_Abs m X q´) q)) :: nil); rewrite Forall_to_conj_2 in HY.
destruct HY as (HY0 & HY1). specialize (Hrpar Y HY0 HY1); simpls.
eapply (H _ _ p´ _ q´ m X); auto.
Focus 3. apply Hrpar.
simpls; eapply wfp_cfresh_in. Focus 2. apply Htp.
auto. apply cfresh_gvar.
simpls; eapply wfp_cfresh_in. Focus 2. apply H3.
auto. apply cfresh_gvar.
lets (a & pr´ & pr´´ & Htp) : H1; clear H1.
assert (Htparp : {{wfp_Par (wfp_Abs m X p´) p -- LabOut a pr´´ ->> AP (wfp_Par (wfp_Abs m X p´) pr´)}}) by (applys¬ act2_out).
lets (qq´ & aq´´ & Htap & Hrap) : ONORbis_out_normal Hon Htparp.
lets (n & Hn) : find_fresh_chan ((proc (wfp_Par (wfp_Abs m X p´) p)) :: (proc (wfp_Par (wfp_Abs m X q´) q)) :: nil).
lets (Z & Hz) : find_fresh (proc pr´´ :: proc aq´´ :: nil).
rewrite Forall_to_conj_2 in ×.
inverts Hn; inverts Hz.
assert (Hneqnm : n ≠ m).
introv Heq; subst.
rewrite wfp_cfresh_par_iff in H0; destruct H0 as (H0 & _).
rewrite wfp_cfresh_Abs in H0; jauto.
specializes Hrap H3; try eassumption; clear H0 H1 H2 H3.
inverts Htap...
inverts H3.
destruct aq; inverts H4.
replace (wfp_Par (wfp_Abs m X p´) pr´) with (iter_abs_par (m :: nil) (X :: nil) (p´ :: nil) pr´) in Hrap by auto.
replace (wfp_Par (wfp_Abs m X q´) w) with (iter_abs_par (m :: nil) (X :: nil) (q´ :: nil) w) in Hrap by auto.
assert (Hsize : wfp_sizeP_out (wfp_Par (wfp_Abs n Z pr´´) pr´) < wfp_sizeP_out p).
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpls.
rewrite× sizeP_subst; rewrite× <- sizeO_subst.
lets HP : sizeP_out Htp. lets HO : sizeO_out Htp. nat_math.
specialize (H _ Hsize p´ (wfp_Par (wfp_Abs n Z aq´´) w)).
specialize (H q´ m X).
lets Hfoutp : wfp_cfresh_out Hfmp Htp.
lets Hfoutq : wfp_cfresh_out Hfmq H3.
specializes¬ H Hfxq´;
try rewrite wfp_cfresh_par_iff; try splits*;
try rewrite wfp_cfresh_Abs; try splits×.
apply H; clear H.
lets Hf1 : (iter_abs_par_fiddle 1 (m :: nil) (X :: nil) (p´ :: nil) (wfp_Abs n Z pr´´) pr´);
lets Hf2 : (iter_abs_par_fiddle 1 (m :: nil) (X :: nil) (q´ :: nil) (wfp_Abs n Z aq´´) w); simpls.
etransitivity. symmetry. applys× Hf1.
splits¬. intro Hm; inverts Hm.
etransitivity. apply Hrap.
applys× Hf2.
splits¬. intro Hm; inverts Hm.
Grab Existential Variables.
unfold wfp_sizeP_out, wfp_sizeP, wfp_sizeO; simpls.
erewrite (sizeP_in a p (wfp_Gvar Y) _ _ Htp).
erewrite (sizeO_in a p (wfp_Gvar Y) _ _ Htp).
nat_math.
Grab Existential Variables.
auto. auto.
Qed.
Lemma lemma415: ∀ (p p´ q q´ : wfprocess), ∀ m X,
m ### p → m ### q →
m ### p´ → m ### q´ →
X # p´ → X # q´ →
(wfp_Par (wfp_Abs m X p´) p) ≈ONOR (wfp_Par (wfp_Abs m X q´) q) →
p ≈ONOR q ∧ p´ ≈ONOR q´.
Proof.
intros; splits.
applys¬ (lemma415a p p´ q q´ m X).
applys¬ (lemma415b p p´ q q´ m X).
Qed.