Library HOC17NORbis
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 HOC13Bisimulations.
Require Import HOC15HObis.
Lemma NORbis_sym : Symmetric NORbis.
Proof.
introv H. inversion H as [R HR].
unfold NORbis. ∃ R. split. apply HR.
unfold Normal_bisimulation in HR.
apply HR. apply HR.
Qed.
Lemma NORbisC_sym: Symmetric NORbisC.
Proof.
introv H. destructs H. splits¬. apply¬ NORbis_sym.
Qed.
Lemma NORbis_tau : tau_relation NORbis.
Proof.
introv Hio Ht.
inversion Hio as (R & HR).
assert (∃ (q´ : wfprocess), {{q -- Tau ->> AP q´}} ∧ R p´ q´).
unfold Normal_bisimulation, tau_relation in HR. eapply HR.
applys¬ HR. assumption.
inversion H as (q´ & Hq).
∃ q´. split. apply Hq.
∃ R. split. apply HR. apply Hq.
Qed.
Lemma NORbisC_tau: tau_relation NORbisC.
Proof.
introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
apply NORbis_tau in Hio; auto. destruct (Hio _ Ht) as (q´ & Ht´ & Hio´).
lets Hcp3: cp_trans_tau Hcp1 Ht. lets Hcp4: cp_trans_tau Hcp2 Ht´.
∃ q´. unfolds NORbisC. splits¬.
Qed.
Lemma NORbis_out_normal : out_normal_relation NORbis.
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 Normal_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. applys¬ HR. applys¬ Hq.
Qed.
Lemma NORbisC_out_normal: out_normal_relation NORbisC.
Proof.
introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
apply NORbis_out_normal in Hio; auto. destruct (Hio _ _ _ Ht) as (q´ & q´´ & Ht´ & Hr).
lets (Hcp3 & Hcp3´): cp_trans_out Hcp1 Ht. lets (Hcp4 & Hcp4´): cp_trans_out Hcp2 Ht´.
∃ q´ q´´. splits¬. intros. splits¬.
applys cp_par. split¬. applys¬ cp_abs.
applys cp_par. split¬. applys¬ cp_abs.
Qed.
Lemma NORbis_in_normal : in_normal_relation NORbis.
Proof with automate.
introv Hio Ht. lets Hio´ : Hio.
inversion Hio´ as [R [[Hns [Hnt [Hno Hni]]] Hr]].
lets Hni´ : Hni; specializes Hni´ Ht. apply Hr.
destruct Hni´ as (fq & Htq & Hyp). ∃ fq; splits¬.
introv Hfmp Hfmq; specializes¬ Hyp Hfmq.
∃ R; repeat splits¬.
Qed.
Lemma NORbisC_in_normal: in_normal_relation NORbisC.
Proof with automate.
introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
apply NORbis_in_normal in Hio; auto. destruct (Hio _ _ Ht) as (fq & Ht´ & Hr).
∃ fq; splits~; intros. splits...
applys cp_trans_in. apply Hcp1. apply Ht. unfolds¬.
applys cp_trans_in. apply Hcp2. apply Ht´. unfolds¬.
Qed.
Inductive R_swap : binary wfprocess :=
| Rswap : ∀ (m n: chan) p q, p ≈NOR q → R_swap (wfp_swap_chan m n p) (wfp_swap_chan m n q).
Hint Constructors R_swap.
Lemma NORbis_ch_swap: ∀ (m n: chan) p q, p ≈NOR q → (wfp_swap_chan m n p) ≈NOR (wfp_swap_chan m n q).
Proof with automate.
introv Hbis. destruct Hbis as (Hcp1 & Hcp2 & Hbis). splits.
unfolds¬. simpl; rewrite¬ GV_swap_chan. unfolds¬. simpl; rewrite¬ GV_swap_chan.
∃ R_swap. split¬. clear. splits.
introv Hr. inverts Hr. constructor. apply¬ NORbisC_sym.
introv Hr Ht. inverts Hr.
lets H0: (wfp_trans_swap_chan_tau). lets H0´: H0.
set (wfmnp´ := wfp_swap_chan m n p´).
specialize (H0 m n (wfp_swap_chan m n p0) p´ Ht); simpl in H0; rewrite wfp_swap_chan_involutive in H0.
eapply (NORbisC_tau p0 q0 _ wfmnp´) in H0; eauto. destruct H0 as (q´ & Htq & Hr).
∃ (wfp_swap_chan m n q´). simpl; split¬.
rewrite <- (wfp_swap_chan_involutive m n p´).
constructor¬.
introv Hr Ht. inverts Hr.
apply (wfp_trans_swap_chan_out a m n) in Ht; simpl in Ht.
set (wfmnp´ := wfp_swap_chan m n p´); set (wfmnp´´ := wfp_swap_chan m n p´´).
rewrite wfp_swap_chan_involutive in Ht.
eapply (NORbisC_out_normal p0 q0 H _ wfmnp´ wfmnp´´) in Ht; eauto. destruct Ht as (q´ & q´´ & Htq & Hr).
∃ (wfp_swap_chan m n q´) (wfp_swap_chan m n q´´). splits.
rewrite <- (swap_name_involutive m n a). apply¬ wfp_trans_swap_chan_out.
intros c X Hfc1 Hfc2 Hfv1 Hfv2. rewrite <- (swap_name_involutive m n c) at 2.
rewrite <- wfp_eq_swap_chan_abs. rewrite <- wfp_eq_swap_chan_par.
rewrite <- (wfp_swap_chan_involutive m n (wfp_Par (wfp_Abs c X p´´) p´)).
constructor... applys¬ Hr.
rewrite <- (wfp_swap_chan_involutive m n p0). applys¬ wfp_fresh_chan_cswap.
rewrite <- (wfp_swap_chan_involutive m n q0). applys¬ wfp_fresh_chan_cswap.
applys¬ wfp_fresh_gvar_cswap.
rewrite <- (wfp_swap_chan_involutive m n q´´). applys¬ wfp_fresh_gvar_cswap.
introv Hr Ht; inverts Hr.
lets H´´ : Ht; apply (wfp_trans_swap_chan_in a m n) in Ht. lets Ht´: Ht.
simpl in Ht; rewrite wfp_swap_chan_involutive in Ht. destruct Ht as (ap´ & Ht & Hr).
generalize (NORbisC_in_normal p0 q0 H _ ap´ Ht). intros (fq & Htq & Hrq).
generalize (wfp_trans_swap_chan_in _ m n q0 fq Htq). intros (aq & Htq´ & Hraq).
lets Htq´´ : Htq´. rewrite swap_name_involutive in Htq´´. ∃ aq. splits...
introv Hf1 Hf2.
rewrite <- (wfp_swap_chan_involutive m n (wfp_Send m0 wfp_Nil)).
rewrite <- Hraq.
rewrite (wfp_swap_chan_involutive m n (wfp_Send m0 wfp_Nil)).
rewrite <- (wfp_swap_chan_involutive m n (wfp_inst_Abs fp (wfp_Send m0 wfp_Nil))).
rewrite Hr...
constructor... apply Hrq.
rewrite <- (wfp_swap_chan_involutive m n p0). applys¬ wfp_fresh_chan_cswap.
rewrite <- (wfp_swap_chan_involutive m n q0). applys¬ wfp_fresh_chan_cswap.
constructor. splits¬.
Grab Existential Variables.
auto.
Qed.
Lemma Norbis_ch_chan: ∀ m n X (p q : wfprocess), m###p → m###q → n###p → n###q →
(wfp_subst (wfp_Send m wfp_Nil) X p) ≈NOR (wfp_subst (wfp_Send m wfp_Nil) X q) →
(wfp_subst (wfp_Send n wfp_Nil) X p) ≈NOR (wfp_subst (wfp_Send n wfp_Nil) X q).
Proof with automate.
introv Hf1 Hf2 Hf3 Hf4 Hp. apply (NORbis_ch_swap m n) in Hp.
rewrite_all wfp_swap_chan_on_subst1 in Hp.
replace (wfp_subst (wfp_Send n wfp_Nil) X p) with (wfp_subst (wfp_swap_chan m n (wfp_Send m wfp_Nil)) X (wfp_swap_chan m n p))...
replace (wfp_subst (wfp_Send n wfp_Nil) X q) with (wfp_subst (wfp_swap_chan m n (wfp_Send m wfp_Nil)) X (wfp_swap_chan m n q))...
unfolds swap_name. cases_if; rewrite¬ wfp_fresh_chan_swap.
unfolds swap_name. cases_if; rewrite¬ wfp_fresh_chan_swap.
Qed.
Definition in_normal_relation_ex (R:binary wfprocess) : Prop := ∀ p q,
(R p q) →
∀ a fp, {{p -- LabIn a ->> (AA fp)}} → ∃ fq, {{q--LabIn a->>(AA fq)}} ∧
∃ m, m###p ∧ m###q ∧ (R (wfp_inst_Abs fp (wfp_Send m wfp_Nil)) (wfp_inst_Abs fq (wfp_Send m wfp_Nil))).
Definition Normal_bisimulation_ex (R:binary wfprocess) : Prop :=
(Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation R) ∧ (in_normal_relation_ex R).
Definition NORbis_ex p q : Prop :=
∃ R, (Normal_bisimulation_ex R) ∧ (R p q).
Definition NORbisC_ex (p q : wfprocess) : Prop :=
closed_process p ∧ closed_process q ∧ NORbis_ex p q.
Lemma NORbis_ex_in_normal_ex: in_normal_relation_ex NORbisC_ex.
Proof with automate.
introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
inversion Hio as (R & HR & Hr).
inversion HR as (_ & _ & _ & Hi).
specializes Hi Ht. apply Hr.
destruct Hi as (fq & Htq & m & Hfmp & Hfmq & Hr´).
eexists. splits... ∃ m; splits...
splits¬.
applys¬ (cp_trans_in a p). unfolds¬.
applys¬ (cp_trans_in a q). unfolds¬.
∃ R. splits¬.
Qed.
Lemma in_nor_forall_exists : ∀ R, in_normal_relation R → in_normal_relation_ex R.
Proof.
introv H; introv Hr Ht. specialize (H p q Hr a fp Ht). destruct H as (fq & Ht´ & Hr´).
∃ fq; splits¬.
lets (m & Hf): find_fresh_chan ((proc p)::(proc q)::nil). rewrite Forall_to_conj_2 in Hf.
∃ m. splits×.
Qed.
Inductive R_Swap R : binary wfprocess :=
| Rswr : ∀ p q, R p q → R_Swap R p q
| RswCh : ∀ m n p q, R_Swap R p q → R_Swap R (wfp_swap_chan m n p) (wfp_swap_chan m n q).
Hint Resolve Rswr RswCh.
Lemma NORbis_NORbis_ex : ∀ p q, NORbisC p q ↔ NORbisC_ex p q.
Proof with automate.
introv. split; introv H. destruct H as (Hcp1 & Hcp2 & H). splits¬.
∃ NORbisC. split¬.
splits¬.
apply NORbisC_sym.
apply NORbisC_tau.
apply NORbisC_out_normal.
apply in_nor_forall_exists. apply NORbisC_in_normal. splits¬.
destruct H as (Hcp1 & Hcp2 & H). splits¬. destruct H as (R & HR & HO).
∃ (R_Swap R). split¬. clear p q Hcp1 Hcp2 HO. splits.
introv Hr. induction Hr.
constructor. apply¬ HR.
apply¬ RswCh.
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4). eapply HR2 in H; eauto.
edestruct (H p´ Ht) as (q´ & Htq & Hr).
∃ q´. splits¬.
forwards Ht´: wfp_trans_swap_chan_tau m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
edestruct IHHr as (q´ & Htq & Hr´).
eassumption.
∃ (wfp_swap_chan m n q´). splits.
applys¬ wfp_trans_swap_chan_tau.
erewrite <- wfp_swap_chan_involutive at 1. apply¬ RswCh.
introv Hr. induction Hr; introv Ht.
destruct HR as (HR1 & HR2 & HR3 & HR4). eapply HR3 in H; auto.
edestruct H as (q´ & q´´ & Htq & Hr); try eassumption.
∃ q´ q´´. splits¬.
forwards Ht´: wfp_trans_swap_chan_out m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
edestruct IHHr as (q´ & q´´ & Htq & Hr´).
eassumption.
∃ (wfp_swap_chan m n q´) (wfp_swap_chan m n q´´). splits.
rewrite <- (swap_name_involutive m n a). applys¬ wfp_trans_swap_chan_out.
intros. rewrite <- (wfp_swap_chan_involutive m n) at 1.
rewrite <- (swap_name_involutive m n m0) at 2. rewrite <- wfp_eq_swap_chan_abs.
rewrite <- wfp_eq_swap_chan_par.
apply RswCh...
apply Hr´.
rewrite <- (wfp_swap_chan_involutive m n p). apply¬ wfp_fresh_chan_cswap.
rewrite <- (wfp_swap_chan_involutive m n q). apply¬ wfp_fresh_chan_cswap.
applys¬ wfp_fresh_gvar_cswap.
rewrite <- (wfp_swap_chan_involutive m n q´´). applys¬ wfp_fresh_gvar_cswap.
unfolds.
introv Hr. inductions Hr; introv Ht.
destruct HR as (_&_&_& HR4). eapply HR4 in H; eauto.
edestruct H as (fq & Htq & m & Hf1 & Hf2 & Hrq)...
∃ fq; splits...
intros n Hf3 Hf4.
forwards Hre1: wfp_inst_chan_swap (wfp_Send m wfp_Nil) Hf1 Hf3 Ht...
rewrite swap_name_left in Hre1.
forwards Hre2: wfp_inst_chan_swap (wfp_Send m wfp_Nil) Hf2 Hf4 Htq...
rewrite swap_name_left in Hre2.
rewrite <- Hre1, <- Hre2.
applys¬ RswCh; constructor; eapply Hrq.
rename fp into fp0.
forwards (fp & Ht´ & Heq1): wfp_trans_swap_chan_in a m n Ht.
simpl in Ht´; rewrite wfp_swap_chan_involutive in Ht´.
specialize (IHHr ({{|m, n|}}a) fp Ht´). destruct IHHr as (fq & Htq & Hr´).
forwards (fq0 & Htq´ & Heq2): wfp_trans_swap_chan_in ({{|m, n|}}a) m n Htq.
simpl in Htq´; rewrite swap_name_involutive in Htq´.
∃ fq0; splits...
introv Hf3 Hf4.
specializes Heq1 (wfp_Send m0 wfp_Nil); specializes Heq2 (wfp_Send ({{|m, n|}}m0) wfp_Nil)...
rewrite swap_name_involutive in Heq2.
rewrite <- (wfp_swap_chan_involutive m n (wfp_inst_Abs fp0 _)).
rewrite Heq1; rewrite <- Heq2.
apply RswCh. apply Hr´.
eapply wfp_fresh_chan_cswap in Hf3. simpl in Hf3; rewrite¬ swap_chan_involutive in Hf3.
eapply wfp_fresh_chan_cswap in Hf4. simpl in Hf4; rewrite¬ swap_chan_involutive in Hf4.
Qed.
Lemma left413NOR: ∀ n a fv (p q : wfprocess),
permut fv (to_list (GV p \u GV q)) → n = length fv →
wfp_pipe a fv p ≈NOR wfp_pipe a fv q →
∃ ms, length ms = n ∧ Forall (fun m ⇒ a≠m ∧ m###p ∧ m###q) ms
∧ noDup ms ∧ wfp_multisubst (combine fv (¬¬ms)) p ≈NOR wfp_multisubst (combine fv (¬¬ms)) q.
Proof with automate.
induction n; introv Hfv Hlfv Hbis.
symmetry in Hlfv. apply length_zero_inv in Hlfv. subst fv. ∃ (nil:list chan). splits.
rewrite¬ length_nil.
apply Forall_nil.
simpls¬.
repeat rewrite wfp_pipe_nil_eq in Hbis; simpls¬.
symmetry in Hlfv.
lets Hnd: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv.
eapply permut_nodup in Hnd; eauto. apply permut_sym in Hfv.
lets (y & ys & H1): (lengthn fv Hlfv).
subst fv. apply NORbis_NORbis_ex in Hbis.
eapply NORbis_ex_in_normal_ex in Hbis...
lets Hp : TrIn a y (wfp_pipe a ys p).
specializes Hbis Hp.
destruct Hbis as (fq & Htq & m & Hf1 & Hf2 & Hnor).
edestruct (IHn a ys (wfp_subst (wfp_Send m wfp_Nil) y p) (wfp_subst (wfp_Send m wfp_Nil) y q)) as (ms & Hlms & Hfr & Hnd´ & Hr).
simpl; rewrite_all GV_subst_cp; try unfolds¬. rewrite <- union_remove.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply rem1_to_list_perm. apply permut_sym. apply¬ permut_rem1_r.
rewrite length_cons in Hlfv. nat_math.
lets Hyp : wfp_trans_in_abs_eq Htq; inverts Hyp as Hyp; subst.
simpl in Hnor.
simpl in Hnd. do 2 rewrite× wfp_subst_on_pipe in Hnor; try solve [unfolds~].
apply NORbis_NORbis_ex in Hnor...
destruct Hyp as (Y & Hneqy & Hfy & Heq); subst.
simpl in Hnor.
simpl in Hnd. rewrite¬ <- wfp_subst_decomposition_g in Hnor.
do 2 rewrite× wfp_subst_on_pipe in Hnor; try solve [unfolds~].
apply NORbis_NORbis_ex in Hnor...
∃ (m::ms). splits.
rewrite length_cons. nat_math.
apply Forall_cons. rewrite <- wfp_pipe_to_Abs in ×.
apply wfp_cfresh_pipe_cons in Hf1; apply wfp_cfresh_pipe_cons in Hf2; splits...
clear Hlms Hnd´ Hr. induction ms.
apply Forall_nil.
inverts Hfr. applys¬ Forall_cons. destructs H1. splits.
apply H.
applys× wfp_cfresh_subst_from1.
applys× wfp_cfresh_subst_from1.
clear Hr Hlms. induction ms.
simpls. rewrite Mem_nil_eq. rew_logic¬.
simpl; simpl in Hnd´; splits×.
inverts Hfr. rewrite Mem_cons_eq. rew_logic. split.
destructs H1. apply permut_sym in Hfv. apply mem_of_permuts in Hfv.
rewrite <- from_list_spec in Hfv. rewrite from_to_list in Hfv.
rewrite in_union in Hfv. destruct Hfv.
apply wfp_cfresh_subst_from2 in H0; auto. simpls; rewrite× cfresh_send in H0.
apply wfp_cfresh_subst_from2 in H1; auto. simpls; rewrite× cfresh_send in H1.
applys× IHms.
simpls. rewrite length_cons in Hlfv.
rewrite_all× wfp_mult_sub_commute; try apply wfp_cpl_opl;
try (rewrite wfp_length_opl; nat_math); constructor.
Qed.
Inductive R_r2: binary wfprocess :=
| R_r2_base: ∀ m X (p q : wfprocess), m###p → m###q →
(wfp_subst (wfp_Send m wfp_Nil) X p) ≈NOR (wfp_subst (wfp_Send m wfp_Nil) X q) → ∀ a,
a ≠ m → R_r2 (wfp_Abs a X p) (wfp_Abs a X q)
| R_r2_bis: ∀ p q, p ≈NOR q → R_r2 p q.
Hint Resolve R_r2_bis R_r2_base.
Lemma NORbis_ex_R_r : Normal_bisimulation_ex R_r2.
Proof with automate.
splits.
unfolds. introv H. inverts H.
applys¬ (R_r2_base m). applys¬ NORbisC_sym.
apply R_r2_bis. apply¬ NORbisC_sym.
unfolds. introv Hr Ht. inverts Hr.
inverts Ht.
apply NORbisC_tau in H; auto. destruct (H _ Ht) as (q´ & Ht´ & Hr).
∃ q´. split¬.
unfolds. introv Hr Ht. inverts Hr.
inverts Ht.
apply NORbisC_out_normal in H; auto. destruct (H _ _ _ Ht) as (q´ & q´´ & Ht´ & Hr).
∃ q´ q´´. split¬.
unfolds. introv Hr; introv H. inverts Hr.
lets Heq : wfp_trans_in_chan_eq H; subst.
eexists. splits...
∃ m; splits; try solve [rewrite× wfp_cfresh_Abs].
lets Hyp : wfp_trans_in_abs_eq H; inverts Hyp as Hyp; subst...
destruct Hyp as (Y & Hneq & Hfy & Heq); subst; simpl.
rewrite <- wfp_subst_decomposition_g...
apply NORbisC_in_normal in H0; auto. destruct (H0 _ _ H) as (fq & Ht´ & Hr).
∃ fq; splits...
lets (m & Hf): find_fresh_chan ((proc p)::(proc q)::nil). rewrite Forall_to_conj_2 in Hf.
destruct Hf as (Hf1 & Hf2). specializes Hr m Hf1 Hf2.
Qed.
Lemma NORbis_congr_abs : ∀ (p q : wfprocess),
∀ m X, m###p → m###q → (wfp_subst (wfp_Send m wfp_Nil) X p) ≈NOR (wfp_subst (wfp_Send m wfp_Nil) X q) →
∀ a, a≠m → (wfp_Abs a X p) ≈NOR (wfp_Abs a X q).
Proof.
introv Hf1 Hf2 Hbis Hneq.
assert (closed_process (wfp_Abs a X p)).
destruct Hbis as (Hcp1 & Hcp2 & _); simpls; unfolds closed_process.
simpl; rewrite GV_subst_cp in *; try unfolds¬. assumption.
assert (closed_process (wfp_Abs a X q)).
destruct Hbis as (Hcp1 & Hcp2 & _); simpls; unfolds closed_process.
simpl; rewrite GV_subst_cp in *; try unfolds¬. assumption.
apply NORbis_NORbis_ex. splits¬. ∃ R_r2. split.
apply NORbis_ex_R_r.
applys× (R_r2_base m).
Qed.
Lemma right413NOR: ∀ n a fv (p q : wfprocess),
permut fv (to_list (GV p \u GV q)) → length fv = n →
(∃ ms, n = length ms ∧ Forall (fun m ⇒ a≠m ∧ m###p ∧ m###q) ms
∧ noDup ms ∧ wfp_multisubst (combine fv (¬¬ms)) p ≈NOR wfp_multisubst (combine fv (¬¬ms)) q) →
wfp_pipe a fv p ≈NOR wfp_pipe a fv q.
Proof with automate.
induction n; introv Hfv Hlfv H.
apply length_zero_inv in Hlfv. subst.
destruct H as (ms & Hl & Hf & Hnd & Hr).
symmetry in Hl. apply length_zero_inv in Hl. subst...
lets Hnd: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv.
eapply permut_nodup in Hnd; eauto. apply permut_sym in Hfv.
lets (y & ys & H1): (lengthn fv Hlfv). rewrite H1. rewrite H1 in Hnd, Hfv, Hlfv.
destruct H as (ms & Hlms & Hfr & Hnd´ & Hnor). simpls.
symmetry in Hlms. lets (m & ms´ & H2): (lengthn ms Hlms).
subst.
inverts Hfr.
eapply (NORbis_congr_abs).
applys× wfp_cfresh_pipe.
applys× wfp_cfresh_pipe.
rewrite_all× wfp_subst_on_pipe; try unfolds¬. apply IHn.
simpl; rewrite_all GV_subst_cp; try unfolds¬. rewrite <- union_remove.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply rem1_to_list_perm. apply permut_sym. apply¬ permut_rem1_r.
rewrite length_cons in Hlfv. nat_math.
∃ ms´. splits.
rewrite length_cons in Hlms. nat_math.
clear Hlms Hnor. induction ms´.
apply Forall_nil.
apply Forall_cons. simpl in Hnd´. rewrite Mem_cons_eq in Hnd´.
rew_logic in Hnd´. splits.
inverts× H2.
apply wfp_cfresh_subst_in. inverts× H2.
simpl; rewrite× cfresh_send_nil.
apply wfp_cfresh_subst_in. inverts× H2.
simpl; rewrite× cfresh_send_nil.
apply IHms´.
simpls. rewrite Mem_cons_eq in Hnd´. rew_logic in Hnd´. split×.
inverts¬ H2. inverts¬ Hnd´.
simpl in Hnor. rewrite length_cons in ×. rewrite_all× <- wfp_mult_sub_commute;
try apply wfp_cpl_opl; try (rewrite¬ wfp_length_opl; nat_math) ; try unfolds¬.
apply H1.
Qed.
Lemma pre_lemma413NOR: ∀ n a fv (p q : wfprocess),
permut fv (to_list (GV p \u GV q)) → length fv = n →
(wfp_pipe a fv p ≈NOR wfp_pipe a fv q ↔
∃ ms, length ms = n ∧ Forall (fun m ⇒ a≠m ∧ m###p ∧ m###q) ms
∧ noDup ms ∧ wfp_multisubst (combine fv (¬¬ms)) p ≈NOR wfp_multisubst (combine fv (¬¬ms)) q).
Proof.
introv Hp Hl. split; introv Hbis.
applys× left413NOR.
applys× right413NOR. rewrite <- plus_n_O.
destruct Hbis as (ms & Hms); ∃ ms.
rewrite Hl; intuition.
Qed.
Lemma permute_NOR_pipe : ∀ a xs ys (p q : wfprocess),
permut xs (to_list (GV p \u GV q)) → permut ys (to_list (GV p \u GV q)) →
wfp_pipe a xs p ≈NOR wfp_pipe a xs q → wfp_pipe a ys p ≈NOR wfp_pipe a ys q.
Proof.
introv Hfv1 Hfv2 Hp. applys× pre_lemma413NOR.
remember Hfv1 as Hfve. clear HeqHfve.
lets Hnd1: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv1.
eapply permut_nodup in Hnd1; eauto. apply permut_sym in Hfv1.
lets Hnd2: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv2.
eapply permut_nodup in Hnd2; eauto. apply permut_sym in Hfv2.
apply permut_sym in Hfve. eapply permut_trans in Hfve; eauto. apply permut_sym in Hfve.
apply (pre_lemma413NOR (length xs)) in Hp; auto.
destruct Hp as (ms & Hl & Hf & Hnd & Hbis).
rewrite <- plus_n_O.
asserts Hl´: (length ys = length ms).
apply permut_len in Hfve. rewrite¬ <- Hfve.
lets¬ P´: permuted_subst xs ys (¬¬ms) Hfve.
apply wfp_cpl_opl.
rewrite¬ wfp_length_opl.
destruct P´ as (ps & P´ & H).
lets (ns & Hns & Hp´): wfp_permut_opl ps ms P´. ∃ ns. splits.
apply permut_len in Hp´. rewrite¬ <- Hp´.
applys× Forall_permut.
apply permut_nodup in Hp´; auto.
rewrite Hns in H. rewrite <- (H p). rewrite¬ <- (H q).
Qed.
Inductive R_ch2: binary wfprocess :=
| R_ch2_base: ∀ a b X p q,
(wfp_Abs a X p) ≈NOR (wfp_Abs a X q) → R_ch2 (wfp_Abs b X p) (wfp_Abs b X q)
| R_ch2_bis: ∀ p q, p ≈NOR q → R_ch2 p q.
Hint Resolve R_ch2_bis R_ch2_base.
Lemma NORbis_exR_ch2 : Normal_bisimulation_ex R_ch2.
Proof with automate.
splits.
unfolds. introv H. inverts H.
apply NORbisC_sym in H0. applys× R_ch2_base.
apply R_ch2_bis. apply¬ NORbisC_sym.
unfolds. introv Hr Ht. inverts Hr.
inverts Ht.
apply NORbisC_tau in H; auto. destruct (H _ Ht) as (q´ & Ht´ & Hr).
∃ q´. split¬.
unfolds. introv Hr Ht. inverts Hr.
inverts Ht.
apply NORbisC_out_normal in H; auto. destruct (H _ _ _ Ht) as (q´ & q´´ & Ht´ & Hr).
∃ q´ q´´. split¬.
unfolds. introv Hr Ht. inverts Hr.
lets Heq : wfp_trans_in_chan_eq Ht; subst.
eexists; splits...
apply NORbisC_in_normal in H; auto.
lets Htr : TrIn a0 X p0. specializes H Htr.
destruct H as (fq & Htq & Hypm).
lets (m & Hf): find_fresh_chan ((proc p0)::(proc q0)::(Send a0 Nil)::(Send a Nil)::nil).
rewrite Forall_to_conj_4 in Hf. destruct Hf as (Hfp & Hfq & Hfa0 & Hfa).
rewrite cfresh_send in Hfa0. rewrite cfresh_send in Hfa.
destruct Hfa0 as (_ & Hfa0). destruct Hfa as (_ & Hfa).
∃ m; splits...
rewrite¬ wfp_cfresh_Abs.
rewrite¬ wfp_cfresh_Abs.
assert (Hf1 : m ### wfp_Abs a0 X p0) by rewrite¬ wfp_cfresh_Abs.
assert (Hf2 : m ### wfp_Abs a0 X q0) by rewrite¬ wfp_cfresh_Abs.
specializes¬ Hypm Hf2.
lets Hyp1 : wfp_trans_in_abs_eq Ht; inverts Hyp1 as Hyp1;
lets Hyp2 : wfp_trans_in_abs_eq Htq; inverts Hyp2 as Hyp2; subst; simpls; constructor...
destruct Hyp2 as (Y & Hneqy & Hfy & Heq); subst; simpls.
rewrite¬ <- wfp_subst_decomposition_g in Hypm.
destruct Hyp1 as (Y & Hneqy & Hfy & Heq); subst; simpls.
rewrite¬ <- wfp_subst_decomposition_g.
destruct Hyp1 as (Y & Hneqy & Hfy & Heq1);
destruct Hyp2 as (Z & Hneqz & Hfz & Heq2); subst; simpls.
rewrite <- wfp_subst_decomposition_g in *; auto...
apply NORbisC_in_normal in H; auto. destruct (H _ _ Ht) as (fq & Ht´ & Hr).
∃ fq; splits×.
lets (m & Hf): find_fresh_chan ((proc p)::(proc q)::nil). rewrite Forall_to_conj_2 in Hf.
destruct Hf as (Hf1 & Hf2). specializes Hr m Hf1 Hf2.
Qed.
Lemma change_NOR_channel : ∀ a b xs (p q : wfprocess),
permut xs (to_list (GV p \u GV q)) →
wfp_pipe a xs p ≈NOR wfp_pipe a xs q →
wfp_pipe b xs p ≈NOR wfp_pipe b xs q.
Proof with automate.
induction xs; simpls¬.
introv Hfl H´. lets H: H´. destruct H´ as (Hcp1 & Hcp2 & H´).
apply NORbis_NORbis_ex. splits;
repeat rewrite <- wfp_pipe_to_Abs; try apply wfp_closed_pipe;
try rewrites (permut_from_list Hfl); try rewrite from_to_list;
unfold subset; introv; try rewrite× in_union; simpl.
∃ R_ch2. split.
apply NORbis_exR_ch2.
constructor¬.
lets (m & Hf): find_fresh_chan ((proc p)::proc q::(Send b Nil)::(Send a Nil)::nil).
rewrite Forall_to_conj_4 in Hf. destruct Hf as (Hf1 & Hf2 & Hf3 & Hf4).
rewrite cfresh_send in Hf3. destruct Hf3 as (_&Hf3).
rewrite cfresh_send in Hf4. destruct Hf4 as (_&Hf4).
apply NORbis_congr_abs with (m := m)...
applys× wfp_cfresh_pipe. applys× wfp_cfresh_pipe.
lets Hnd´: (nodup_tolist (GV p \u GV q)). lets Hnd: (permut_sym Hfl).
apply permut_nodup in Hnd; auto. clear Hnd´. simpl in Hnd.
rewrite_all× wfp_subst_on_pipe; try unfolds¬. apply IHxs.
simpl; rewrite_all GV_subst_cp; try unfolds¬. rewrite <- union_remove.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply rem1_to_list_perm. apply permut_sym. apply¬ permut_rem1_r.
rewrite_all× <- wfp_subst_on_pipe; try solve [unfolds~].
apply NORbisC_in_normal in H...
lets H´´ : TrIn a a0 (wfp_pipe a xs p). specializes H H´´.
destruct H as (fq & Htq & Hr).
asserts Hf1´: (m ### wfp_pipe a (a0::xs) p).
applys¬ wfp_cfresh_pipe.
asserts Hf2´: (m ### wfp_pipe a (a0::xs) q).
applys¬ wfp_cfresh_pipe.
specializes Hr m Hf1´ Hf2´...
lets Hyp1 : wfp_trans_in_abs_eq Htq; inverts Hyp1 as Hyp1; subst; simpls¬.
destruct Hyp1 as (Y & Hneqy & Hfy & Heq); subst; simpls.
rewrite¬ <- wfp_subst_decomposition_g in Hr.
Qed.
Lemma NORbisE_equiv: ∀ n (p q : wfprocess) fv,
permut fv (to_list (GV p \u GV q)) → length fv = n →
(p ≈*NOR q ↔ (∃ ms, n = length ms ∧ Forall (fun m ⇒ m###p ∧ m###q) ms
∧ noDup ms ∧ wfp_multisubst (combine fv (¬¬ms)) p ≈NOR wfp_multisubst (combine fv (¬¬ms)) q)).
Proof.
introv Hp Hl. split; introv Hbis.
unfolds in Hbis.
specialize (Hbis 0 fv Hp). apply (pre_lemma413NOR n) in Hbis; auto.
destruct Hbis as (ms & Hls & Hf & Hnd & Hbis). ∃ ms. splits¬.
clear Hnd Hls Hbis. induction ms.
apply Forall_nil.
inverts Hf. applys× Forall_cons.
unfolds. introv Hp´.
destruct Hbis as (ms & Hls & Hf & Hnd & Hbis).
applys¬ (permute_NOR_pipe a fv).
lets (a´ & Hm): (wfp_find_fresh_chan (¬¬ms)).
assert (Hm´ : ¬ Mem a´ ms).
apply wfp_Forall_cfresh_neq in Hm.
rewrite <- Forall_Mem in Hm; specialize (Hm a´); jauto.
applys¬ (change_NOR_channel a´).
applys¬ pre_lemma413NOR. rewrite <- plus_n_O. ∃ ms. splits¬.
nat_math.
clear Hbis Hls Hnd Hm; induction ms.
apply Forall_nil.
inverts Hf. rewrite Mem_cons_eq in Hm´. apply Forall_cons. splits×.
rew_logic¬.
Qed.
Lemma NORbis_in_par: ∀ a X (p p´ q q´ : wfprocess),
a###q´ → X#p → X#q →
(wfp_Par (wfp_Abs a X p) p´) ≈NOR (wfp_Par (wfp_Abs a X q) q´) → wfp_Par p p´ ≈NOR wfp_Par q q´.
Proof with automate.
introv Hf0 Hf1 Hf2 Hbis. apply NORbisC_in_normal in Hbis.
lets Ht : TrAct1 p´ (TrIn a X p). specializes Hbis Ht.
destruct Hbis as (fq & Htq & Hr). inverts Htq.
destruct ap; inverts H3...
lets (m&H´): find_fresh_chan ((Abs f a X p)::(Abs f a X q)::(proc p´)::(proc q´)::nil).
rewrite Forall_to_conj_4 in H´. destruct H´ as (Hfa1 & Hfa2 & Hfp & Hfq).
assert (Hfp´ : m ### Par (Abs f a X p) p´) by (rewrite cfresh_par_iff; intuition).
assert (Hfq´ : m ### Par (Abs f a X q) q´) by (rewrite cfresh_par_iff; intuition).
specializes¬ Hr Hfq´; simpls.
lets Hyp1 : wfp_trans_in_abs_eq H2; inverts Hyp1 as Hyp1; subst; simpls¬.
do 2 rewrite wfp_gfresh_subst_rewrite in Hr; auto.
destruct Hyp1 as (Y & Hneqy & Hfy & Heq); subst; simpls¬.
rewrite¬ <- wfp_subst_decomposition_g in Hr.
do 2 rewrite wfp_gfresh_subst_rewrite in Hr; auto.
destruct aq; inverts H3... false. applys× false_trans_in.
Qed.
Theorem sizeCh_NORbis : ∀ m p q,
p ≈NOR q → sizeCh m p = sizeCh m q.
Proof with automate.
intro m. induction p using (measure_induction wfp_sizeP). introv Hio.
remember (sizeCh m p) as sp. destruct sp.
remember (sizeCh m q) as sq. destruct¬ sq.
assert (Hin: sizeCh m q > 0).
nat_math.
asserts Hch: (CHS q ≠ \{}). apply sizeCh_CHS. ∃¬ m.
apply trans_CHS in Hch.
destruct Hch as [ [a [fq Hq]] |[a [q´ [q´´ Hq]]]] ; apply NORbisC_sym in Hio.
lets (fp & Hp & Hio´): (NORbisC_in_normal q p Hio a fq Hq).
lets (n & Hex2): (find_fresh_chan ((proc p)::(proc q)::(Send m Nil)::nil)). rewrite Forall_to_conj_3 in Hex2.
destruct Hex2 as (Hf1 & Hf2 & Hf3). rewrite cfresh_send in Hf3. destruct Hf3 as (_&Hf3).
specializes Hio´ n Hf2 Hf1.
asserts Hneq2: (a≠m).
apply (sizeCh_neq a m p). rewrite <- Heqsp.
lets Htmp: sizeCh_in_nfr a p fp Hp. nat_math.
lets Hsp: (>> sizeCh_in_neq a m p (wfp_Send n wfp_Nil) fp Hneq2 Hp).
simpl. cases_if¬.
lets Hsq: (>> sizeCh_in_neq a m q (wfp_Send n wfp_Nil) fq Hneq2 Hq).
simpl. cases_if¬.
etransitivity. eassumption.
etransitivity. apply¬ Hsp.
etransitivity.
apply H with (q:= wfp_inst_Abs fq (wfp_Send n wfp_Nil))...
unfold wfp_sizeP; simpl; clear Hio´; apply (sizeP_in a p (wfp_Send n wfp_Nil) fp) in Hp. nat_math. simpls¬.
apply NORbisC_sym. applys¬ Hio´.
etransitivity. symmetry. applys¬ Hsq. auto.
lets (p´ & p´´ & Hp & Hio´): (NORbisC_out_normal q p Hio a q´ q´´ Hq).
lets (n & Hex2): (find_fresh_chan ((proc p)::(proc q)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (Hfnp & Hfnq).
lets (Z & Hex2): (find_fresh ((proc p´´)::(proc q´´)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (HfZp & HfZq).
specializes Hio´ (>> n Z Hfnq Hfnp HfZq HfZp).
asserts Hneq2: (a≠m).
apply (sizeCh_neq a m p). rewrite <- Heqsp.
lets Htmp: sizeCh_out_nfr a p p´ p´´ Hp. nat_math.
lets (_ & Hfnp´ & Hfnp´´) : wfp_cfresh_out Hfnp Hp.
lets (_ & Hfnq´ & Hfnq´´) : wfp_cfresh_out Hfnq Hq.
apply NORbis_in_par in Hio´; auto.
asserts Hsp: (sizeCh m p = sizeCh m (wfp_Par p´´ p´)).
rewrite (sizeCh_out_neq a m p p´ p´´ Hneq2 Hp). simpl. nat_math.
asserts Hsq: (sizeCh m q = sizeCh m (wfp_Par q´´ q´)).
rewrite (sizeCh_out_neq a m q q´ q´´ Hneq2 Hq). simpl. nat_math.
rewrite Heqsp, Heqsq. rewrite Hsp, Hsq. clear Hsp Hsq.
apply H.
unfold wfp_sizeP; simpl. apply sizeP_out in Hp. rewrite Hp. nat_math.
apply¬ NORbisC_sym.
assert (Hin: sizeCh m p > 0).
nat_math.
asserts Hch: (CHS p ≠ \{}). apply sizeCh_CHS. ∃¬ m.
apply trans_CHS in Hch.
rewrite Heqsp. destruct Hch as [ [a [fp Hp]] |[a [p´ [p´´ Hp]]]].
lets (fq & Hq & Hio´): (NORbisC_in_normal p q Hio a fp Hp).
lets (n & Hex): (>> find_fresh_chan ((proc p)::(proc q)::(Send m Nil)::nil)). rewrite Forall_to_conj_3 in Hex.
destruct Hex as (Hf1 & Hf2 & Hf3). rewrite cfresh_send in Hf3. destruct Hf3 as (_&Hf3).
specializes Hio´ n Hf1 Hf2.
lets: nat_comparable. destruct H0. specializes comparable a m.
destruct comparable as (b & dec). destruct b.
apply eq_true_l in dec. rewrite istrue_isTrue in dec. subst.
forwards Hsp: sizeCh_in_eq m p (wfp_Send n wfp_Nil) Hp.
simpl. cases_if¬.
forwards Hsq: sizeCh_in_eq m q (wfp_Send n wfp_Nil) Hq.
simpl. cases_if¬.
rewrite Hsp, Hsq.
rewrite H with (q := wfp_inst_Abs fq (wfp_Send n wfp_Nil))...
unfold wfp_sizeP; simpls; clear Hio´; apply sizeP_in with (m:=(wfp_Send n wfp_Nil)) in Hp...
apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec.
lets Hsp: (>> sizeCh_in_neq a m p (wfp_Send n wfp_Nil) fp dec Hp).
simpl. cases_if¬.
lets Hsq: (>> sizeCh_in_neq a m q (wfp_Send n wfp_Nil) fq dec Hq).
simpl. cases_if¬.
rewrite Hsp, Hsq.
apply H with (q:= wfp_inst_Abs fq (wfp_Send n wfp_Nil)).
unfold wfp_sizeP; simpl; clear Hio´; apply (sizeP_in a p (wfp_Send n wfp_Nil) fp) in Hp. nat_math. simpls¬.
applys¬ Hio´.
lets (q´ & q´´ & Hq & Hio´): (NORbisC_out_normal p q Hio a p´ p´´ Hp).
lets (n & Hex2): (find_fresh_chan ((proc p)::(proc q)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (Hfnp & Hfnq).
lets (Z & Hex2): (find_fresh ((proc p´´)::(proc q´´)::nil)). rewrite Forall_to_conj_2 in Hex2.
destruct Hex2 as (HfZp & HfZq).
specializes Hio´ (>> n Z Hfnp Hfnq HfZp HfZq).
lets (_ & Hfnp´ & Hfnp´´) : wfp_cfresh_out Hfnp Hp.
lets (_ & Hfnq´ & Hfmq´´) : wfp_cfresh_out Hfnq Hq.
apply NORbis_in_par in Hio´; auto.
lets: nat_comparable. destruct H0. specializes comparable a m.
destruct comparable as (b & dec). destruct b.
apply eq_true_l in dec. rewrite istrue_isTrue in dec. subst.
asserts Hsp: (sizeCh m p = sizeCh m (wfp_Par p´´ p´) + 1).
rewrite (sizeCh_out_eq m p p´ p´´ Hp). simpl. nat_math.
asserts Hsq: (sizeCh m q = sizeCh m (wfp_Par q´´ q´) + 1).
rewrite (sizeCh_out_eq m q q´ q´´ Hq). simpl. nat_math.
rewrite Hsp, Hsq. fequals.
apply¬ H.
unfold wfp_sizeP; simpl. apply sizeP_out in Hp. rewrite Hp. nat_math.
apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec.
asserts Hsp: (sizeCh m p = sizeCh m (wfp_Par p´´ p´)).
rewrite (sizeCh_out_neq a m p p´ p´´ dec Hp). simpl. nat_math.
asserts Hsq: (sizeCh m q = sizeCh m (wfp_Par q´´ q´)).
rewrite (sizeCh_out_neq a m q q´ q´´ dec Hq). simpl. nat_math.
rewrite Hsp, Hsq. clear Hsp Hsq.
apply¬ H.
unfold wfp_sizeP; simpl. apply sizeP_out in Hp. rewrite Hp. nat_math.
Qed.
Lemma cfresh_NORbis : ∀ m p q,
p ≈NOR q → m###p → m###q.
Proof.
introv H Hf. rewrite sizeCh_cfresh in ×.
rewrite <- Hf. symmetry. applys¬ sizeCh_NORbis.
Qed.
Definition out_normal_relation_ex (R:binary wfprocess) : Prop :=
∀ p q, (R p q) → ∀ a (p´ p´´ : wfprocess) (H: {{p--LabOut a p´´->>(AP p´)}}), ∃ (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´))).
Lemma out_nor_forall_exists : ∀ R, out_normal_relation R → out_normal_relation_ex R.
Proof.
introv H Hr Ht. specializes H Hr Ht. destruct H as (q´ & q´´ & Ht´ & Hr´).
∃¬ q´ q´´. split¬.
lets (m & Hf): find_fresh_chan ((proc p)::(proc q)::nil). rewrite Forall_to_conj_2 in Hf.
lets (Z & Hf´): find_fresh ((proc p´´)::(proc q´´)::nil). rewrite Forall_to_conj_2 in Hf´.
∃ m Z. splits×.
Qed.
Inductive R_Swap2 R : binary wfprocess :=
| Rr : ∀ p q, R p q → R_Swap2 R p q
| Rsw : ∀ m n p q, R_Swap2 R p q → R_Swap2 R (wfp_swap_chan m n p) (wfp_swap_chan m n q).
Hint Resolve Rr Rsw.
Fixpoint swap_names (l:list chan) (m n: chan) : list chan :=
match l with
| nil ⇒ nil
| a::t ⇒ {{|m, n|}}a :: (swap_names t m n)
end.
Fixpoint swap_channels (l:list wfprocess) (m n: chan) : list wfprocess :=
match l with
| nil ⇒ nil
| a::t ⇒ (wfp_swap_chan m n a) :: (swap_channels t m n)
end.
Lemma length_swap_names: ∀ ms m n, length ms = length (swap_names ms m n).
Proof.
induction ms; introv; simpls¬.
rewrite_all length_cons. specializes IHms m n.
Qed.
Lemma nodup_swap_names: ∀ ms m n, noDup ms ↔ noDup (swap_names ms m n).
Proof.
induction ms; split; introv Hnd; simpls¬.
destruct Hnd as (Hnm & Hnd). split.
clear IHms Hnd. induction ms; simpls¬.
rewrite¬ Mem_nil_eq.
rewrite Mem_cons_eq in ×. rew_logic in ×. destruct Hnm as (Hneq & Hnm). split¬.
introv H. apply Hneq. unfolds swap_name. repeat cases_if¬.
applys¬ IHms.
destruct Hnd as (Hnm & Hnd). split.
clear IHms Hnd. induction ms; simpls¬.
rewrite¬ Mem_nil_eq.
rewrite Mem_cons_eq in ×. rew_logic in ×. destruct Hnm as (Hneq & Hnm). split¬.
applys¬ (IHms m n).
Qed.
Lemma swap_chans_Msubst_comm: ∀ m n ps xs p, length xs = length ps →
wfp_multisubst (combine xs ps) (wfp_swap_chan m n p) = wfp_swap_chan m n (wfp_multisubst (combine xs (swap_channels ps m n)) p).
Proof.
induction ps; introv Hls; simpl.
rewrite length_nil in Hls. apply length0 in Hls. subst. simpls¬.
lets Hls´: Hls. rewrite length_cons in Hls. apply lengthn in Hls.
destruct Hls as (X & xs´ & Hxs). subst. simpl. rewrite wfp_swap_chan_on_subst1.
rewrite wfp_swap_chan_involutive. rewrite¬ IHps.
Qed.
Lemma swap_chans_names: ∀ ms m n, swap_channels (¬¬ swap_names ms m n) m n = (¬¬ ms).
Proof.
induction ms; introv; simpls¬.
replace (wfp_swap_chan m n (wfp_Send ({{|m, n|}}a) wfp_Nil)) with (wfp_Send a wfp_Nil).
rewrite¬ IHms.
automate; rewrite¬ swap_name_involutive.
Qed.
Lemma NORbisE_ch_swap: ∀ m n p q, p ≈*NOR q → (wfp_swap_chan m n p) ≈*NOR (wfp_swap_chan m n q).
Proof.
introv H.
assert (∃ xs, permut xs (to_list (GV p \u GV q))).
∃¬ (to_list (GV p \u GV q)).
destruct H0 as (xs & Hp).
eapply (NORbisE_equiv (length xs) _ _ xs) in H; eauto.
destruct H as (ms & Hls & Hfs & Hnd & Hnor).
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
simpl; rewrite_all¬ GV_swap_chan.
∃ (swap_names ms m n). splits.
rewrite¬ <- length_swap_names.
clear Hnd Hnor Hls. induction ms; simpls.
apply Forall_nil.
inverts Hfs. apply Forall_cons. destruct H1 as (Hf1 & Hf2). split.
apply¬ wfp_fresh_chan_cswap.
apply¬ wfp_fresh_chan_cswap.
apply¬ IHms.
applys¬ nodup_swap_names.
rewrite_all swap_chans_Msubst_comm. rewrite_all swap_chans_names.
applys¬ NORbis_ch_swap.
rewrite wfp_length_opl. rewrite¬ <- length_swap_names.
rewrite wfp_length_opl. rewrite¬ <- length_swap_names.
Qed.
Lemma NORbisE_ONE_ON: out_normal_relation_ex NORbisE → out_normal_relation NORbisE.
Proof with automate.
introv H Hbis Ht. specializes H Hbis Ht.
destruct H as (q´ & q´´ & Htq & m & X & Hfmp & Hfmq & HfXp2 & HfXq2 & Hbis1).
∃ q´ q´´. split¬. intros n Y Hfnp Hfnq HfYp2 HfYq2.
rewrite <- (wfp_swap_chan_involutive m n) at 1.
rewrite <- (wfp_swap_chan_involutive m n).
apply NORbisE_ch_swap.
repeat rewrite wfp_swap_chan_par.
lets (_ & Hfmp1 & Hfmp2): (wfp_cfresh_out a m p p´ p´´ Hfmp Ht).
lets (_ & Hfmq1 & Hfmq2): (wfp_cfresh_out a m q q´ q´´ Hfmq Htq).
lets (_ & Hfnp1 & Hfnp2): (wfp_cfresh_out a n p p´ p´´ Hfnp Ht).
lets (_ & Hfnq1 & Hfnq2): (wfp_cfresh_out a n q q´ q´´ Hfnq Htq)...
rewrite swap_name_right. repeat rewrite¬ wfp_fresh_chan_swap.
assert (X # p´´ ∧ Y # p´´ ∧ X # q´´ ∧ Y # q´´).
lets Hgvp : GV_trans_out Ht; lets Hgvq : GV_trans_out Htq; splits¬.
destruct H as (Hf1 & Hf2 & Hf3 & Hf4).
replace (wfp_Abs m Y p´´) with (wfp_Abs m X p´´).
replace (wfp_Abs m Y q´´) with (wfp_Abs m X q´´).
auto.
rewrite wfp_Abs_eq with (Y := Y); auto.
rewrite¬ wfp_gfresh_subst_rewrite.
rewrite wfp_Abs_eq with (Y := Y); auto.
rewrite¬ wfp_gfresh_subst_rewrite.
Qed.