Library HOC05WFProcesses
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Definition RelWfP: Type := binary wfprocess.
Fixpoint list_proc (l : list wfprocess) : list process :=
match l with
| nil ⇒ nil
| cons x xs ⇒ cons (proc x) (list_proc xs)
end.
Lemma wfp_list_proc_len : ∀ lp, length (list_proc lp) = length lp.
Proof.
induction lp; auto; simpl; rew_length; nat_math.
Qed.
Fixpoint wfp_pipe (a:chan) (XS: list var) (p : wfprocess) : wfprocess :=
match XS with
| nil ⇒ p
| X :: XS ⇒ (wfp_Abs a X (wfp_pipe a XS p))
end.
Fixpoint wfp_multisubst (l: list (var×wfprocess)) (p:wfprocess) : wfprocess :=
match l with
| nil ⇒ p
| cons x xs ⇒ wfp_subst (snd x) (fst x) (wfp_multisubst xs p)
end.
Notation "[ l ] p" := (wfp_multisubst l p) (at level 60).
Definition wfp_swap X Y (p : wfprocess) :=
mkWfP ({{[X,Y]}}p) (wf_swapping p X Y (wf_cond p)).
Definition wfp_swap_chan m n (p : wfprocess) := mkWfP (|m,n|p) (wf_chan_swap p m n (wf_cond p)).
Definition wfp_prod_repeat (p : wfprocess) n := mkWfP (prod (repeat (proc p) n)) (wf_prod_repeat n p (wf_cond p)).
Fixpoint closed_proc_list_wfp (lr: list wfprocess) : Prop :=
match lr with
| nil ⇒ True
| cons x xs ⇒ closed_process (proc x) ∧ closed_proc_list_wfp xs
end.
Lemma wfp_cpl_forall: ∀ ps, closed_proc_list_wfp ps ↔ Forall (fun p : wfprocess ⇒ closed_process p) ps.
Proof.
intro ps0; induction ps0; simpls.
split; intro; try (applys¬ Forall_nil || auto).
split; intro.
applys× Forall_cons.
inverts× H.
Qed.
Lemma wfp_cpl_cpl : ∀ ps, closed_proc_list_wfp ps ↔ closed_proc_list (list_proc ps).
Proof.
induction ps; simpls×.
Qed.
Lemma wfp_permut_cp_list: ∀ rs ps, permut rs ps →
closed_proc_list_wfp rs → closed_proc_list_wfp ps.
Proof.
introv Hp Hcp.
lets H: wfp_cpl_forall.
apply H. applys Forall_permut.
applys¬ (H rs).
assumption.
Qed.
Lemma wfp_cpl_app_inv: ∀ (l1 l2: list wfprocess),
closed_proc_list_wfp (l1 ++ l2) → closed_proc_list_wfp l1 ∧ closed_proc_list_wfp l2.
Proof.
introv H. apply wfp_cpl_forall in H. apply Forall_app_inv in H.
split; applys× wfp_cpl_forall.
Qed.
Lemma wfp_find_fresh_chan: ∀ (ps: list wfprocess), ∃ m, Forall (fun p : wfprocess ⇒ m###p) ps.
Proof.
introv.
generalize (find_fresh_chan (list_proc ps)).
intros (m & Hm).
∃ m.
set (f := (fun p : process ⇒ m ### p)); fold f in Hm.
set (g := (fun p : wfprocess ⇒ f (proc p))).
assert (g = (fun p : wfprocess ⇒ m ### p)) by fequals.
rewrite <- H; unfold g. clear H g.
induction ps.
apply Forall_nil.
inverts Hm; constructor¬.
Qed.
Lemma wfp_pipe_eq_nil : ∀ a p,
wfp_pipe a nil p = p.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_pipe_to_Abs : ∀ a y ys p,
wfp_pipe a (y :: ys) p = wfp_Abs a y (wfp_pipe a ys p).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_multisubst_to_subst : ∀ x lx p lp q,
wfp_multisubst (combine (x :: lx) (p :: lp)) q = wfp_subst p x (wfp_multisubst (combine lx lp) q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_multisubst_to_subst_tail : ∀ x lx p lp q, length lx = length lp →
wfp_multisubst (combine (lx & x) (lp & p)) q = (wfp_multisubst (combine lx lp) (wfp_subst p x q)).
Proof.
inductions lx; introv Hl; lets Hl´ : Hl; symmetry in Hl; rew_length in Hl; [apply length0 in Hl | apply lengthn in Hl].
subst; simpls¬.
destruct Hl as (b & ys´ & Heq); subst; rename ys´ into ys.
repeat rewrite app_cons; simpl; rewrites¬ IHlx.
Qed.
Fixpoint wfp_out_proc_list (l : list chan): list wfprocess :=
match l with
| nil ⇒ nil
| x::xs ⇒ (wfp_Send x wfp_Nil)::(wfp_out_proc_list xs)
end.
Notation "¬¬ l" := (wfp_out_proc_list l) (at level 60).
Lemma wfp_length_opl: ∀ l, length (¬¬ l) = length l.
Proof.
induction l; simpls¬. rewrite_all length_cons. nat_math.
Qed.
Lemma wfp_cpl_opl: ∀ l, closed_proc_list_wfp (¬¬ l).
Proof.
induction l; simpls¬. split¬. unfolds¬.
Qed.
Lemma wfp_opl_app: ∀ l t, ¬¬ (l ++ t ) = ¬¬ l ++ ¬¬ t.
Proof.
induction l; introv.
simpls¬.
rew_app. simpls. rew_app. rewrite¬ IHl.
Qed.
Lemma wfp_opl_inv: ∀ l, ¬¬l = nil → l = nil.
Proof.
induction l; introv H; simpls¬. inverts H.
Qed.
Lemma wfp_mem_opl_inv: ∀ (p : wfprocess) l, Mem p (¬¬l) → ∃ a, p = wfp_Send a wfp_Nil.
Proof.
induction l; introv Hm; simpls¬.
rewrite Mem_nil_eq in Hm. false.
rewrite Mem_cons_eq in Hm. destruct¬ Hm.
∃¬ a.
Qed.
Lemma wfp_mem_opl: ∀ x l, Mem x l ↔ Mem (wfp_Send x wfp_Nil) (¬¬l).
Proof.
split; induction l; introv H.
rewrite Mem_nil_eq in H. false.
simpl. rewrite Mem_cons_eq in ×. destruct¬ H. left. subst¬.
simpls. rewrite Mem_nil_eq in H. false.
simpls. rewrite Mem_cons_eq in ×. destruct¬ H. left. inverts¬ H.
Qed.
Lemma wfp_nodup_opl: ∀ l, noDup l ↔ noDup (¬¬l).
Proof.
split; induction l; introv H; simpls~;
split*;
introv H1; apply H; applys× wfp_mem_opl.
Qed.
Lemma wfp_rem1_opl: ∀ a l, removeOne (wfp_Send a wfp_Nil) (¬¬l) = ¬¬ (removeOne a l).
Proof.
induction l; simpls¬.
cases_if; cases_if¬. inverts H; intuition.
rewrite¬ IHl.
Qed.
Lemma wfp_permut_opl: ∀ (ps : list wfprocess) ms, permut (¬¬ms) ps →
∃ ns, ps = (¬¬ns) ∧ permut ms ns.
Proof.
induction ps; introv Hp. ∃ (nil:list chan). simpl. split¬.
apply permut_of_nil in Hp. apply wfp_opl_inv in Hp. subst¬.
lets Hm: mem_of_permuts Hp. lets Hm´: Hm. apply wfp_mem_opl_inv in Hm. destruct Hm as (m & H). subst.
apply permut_sym in Hp.
apply permut_rem1_r in Hp. apply permut_sym in Hp.
rewrite wfp_rem1_opl in Hp. edestruct IHps as (ns & He & Hp2). eassumption.
∃ (m::ns).
subst. simpl. split¬.
apply permut_sym. apply permut_rem1_l.
applys¬ wfp_mem_opl.
applys¬ permut_sym.
Qed.
Lemma wfp_opl_base: ∀ l p, ¬¬l = p::nil → ∃ m, p = wfp_Send m wfp_Nil ∧ l = m::nil.
Proof.
induction l; introv H; simpls.
inverts H.
inverts H. apply wfp_opl_inv in H2. subst. ∃ a. split¬.
Qed.
Lemma wfp_opl_app_ex: ∀ l t s, ¬¬l = t ++ s →
∃ m n, ¬¬m = t ∧ ¬¬n = s ∧ l = m ++ n.
Proof.
induction l; introv H.
∃ (nil:list chan) (nil:list chan).
simpls. apply nil_eq_app_inv in H. destruct H. subst. simpls¬.
simpls. lets: (classic (Mem (wfp_Send a wfp_Nil) t)). destruct H0.
assert (∃ t´, t = wfp_Send a wfp_Nil::t´).
clear IHl. induction t.
rewrite Mem_nil_eq in H0. false.
rew_app in H. inverts H. ∃¬ t.
destruct H1 as (t´ & Ht). subst. rew_app in H. inverts H.
destruct (IHl t´ s H2) as (m & n & Hmt & Hns & Hlmn).
∃ (a::m) n. subst. simpls. splits¬.
assert (t = nil).
clear IHl. induction¬ t.
rew_app in H. inverts H. rewrite Mem_cons_eq in H0. rew_logic× in H0.
subst.
assert (∃ s´, s = wfp_Send a wfp_Nil::s´).
clear IHl. induction s.
rewrite Mem_nil_eq in H0. false.
rew_app in H. inverts H. ∃¬ (¬¬l).
destruct H1 as (s´ & Hs). subst. rew_app in H. inversion H.
destruct (IHl nil s´ H2) as (m & n & Hmt & Hns & Hlmn).
∃ (nil:list chan) (a::n). apply wfp_opl_inv in Hmt. subst. simpls. splits¬.
Qed.
Lemma wfp_Forall_cfresh_neq: ∀ a ms,
Forall (fun p : wfprocess ⇒ a ### p) (¬¬ms) → Forall (≠a) (ms).
Proof.
induction ms; introv H.
apply Forall_nil.
inverts H. simpl in H2; rewrite cfresh_send in H2. destruct H2 as (_&H2). applys¬ Forall_cons.
Qed.
Lemma wfp_opl_mem : ∀ x ms, ms ≠ nil → Mem x (¬¬ms) → ∃ m, x = wfp_Send m wfp_Nil.
Proof.
inductions ms; introv Hneq Hm.
false Hneq; auto.
simpls; rewrite Mem_cons_eq in Hm; inverts Hm.
∃¬ a.
destruct ms; simpls.
rewrite× Mem_nil_eq in H.
applys¬ IHms.
introv Heq; inverts Heq.
Qed.
Lemma wfp_opl_mem_combine_iff : ∀ v w (xs : list var) ms, length xs = length ms →
(Mem (v, wfp_Send w wfp_Nil) (combine xs (¬¬ms)) ↔ Mem (v, w) (combine xs (ms))).
Proof.
inductions xs; introv Hl.
simpl; repeat rewrites× Mem_nil_eq.
lets Hl´ : Hl; symmetry in Hl´; rew_length in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & ms´ & Heq); subst; rename ms´ into ms.
simpl; split; intro Hm.
rewrite Mem_cons_eq in Hm; inverts Hm.
inverts H; constructor.
rewrite IHxs in H; try constructor~; rew_length in *; nat_math.
rewrite Mem_cons_eq in Hm; inverts Hm.
inverts H; constructor.
rewrite <- IHxs in H; try constructor~; rew_length in *; nat_math.
Qed.
Lemma wfp_permut_opl_iff : ∀ ms ns, permut ms ns ↔ permut (¬¬ms) (¬¬ns).
Proof.
induction ms using (measure_induction length); destruct ms; introv; split; introv Hp.
apply permut_sym in Hp; apply permut_of_nil in Hp; subst; simpls¬.
simpls; apply permut_sym in Hp; apply permut_of_nil in Hp;
apply wfp_opl_inv in Hp; subst; simpls¬.
lets Hl : Hp; apply permut_len in Hl;
symmetry in Hl; rew_length in Hl; apply lengthn in Hl.
destruct Hl as (b & ns´ & Heq); subst; rename ns´ into ns.
elim (classic (c = b)); intro Hneq; subst.
simpls; rewrite <- permut_cons_iff in *; applys¬ H; rew_length; nat_math.
assert (Hmb : Mem b ms).
cut (Mem b (c :: ms)).
introv Hm; rewrite Mem_cons_eq in Hm; inverts× Hm.
apply permut_mem with (l := (b :: ns)); try apply¬ permut_sym; constructor.
assert (Hmc : Mem c ns).
cut (Mem c (b :: ns)).
introv Hm; rewrite Mem_cons_eq in Hm; inverts× Hm.
apply permut_mem with (l := (c :: ms)); auto; constructor.
apply permut_mem_exists in Hmb; apply permut_mem_exists in Hmc.
destruct Hmb as (ms´ & Hms´); destruct Hmc as (ns´ & Hns´).
assert (Hp´ : permut ms´ ns´).
rewrite (permut_cons_iff ms (b :: ms´)) with (x := c) in Hms´.
rewrite (permut_cons_iff ns (c :: ns´)) with (x := b) in Hns´.
rewrite (permut_cons_iff ms´ ns´) with (x := b).
rewrite (permut_cons_iff (b :: ms´) (b :: ns´)) with (x := c).
apply permut_trans with (l2 := (c :: ms)); try solve [applys¬ permut_sym].
apply permut_flip_first_two.
apply permut_trans with (l2 := (b :: ns)); auto.
rewrite H in Hp´; try (apply permut_len in Hp; apply permut_len in Hms´; rew_length in *; nat_math).
rewrite H in Hms´; try (rew_length; nat_math).
rewrite H in Hns´; try (apply permut_len in Hp; rew_length in *; nat_math).
simpls.
apply permut_trans with (l2 := (wfp_Send c wfp_Nil :: (wfp_Send b wfp_Nil :: ¬¬ms´))).
rewrites¬ permut_cons_iff.
apply permut_trans with (l2 := (wfp_Send b wfp_Nil :: (wfp_Send c wfp_Nil :: ¬¬ns´))).
apply permut_flip_first_two; repeat rewrites¬ <- permut_cons_iff.
rewrite <- permut_cons_iff; applys¬ permut_sym.
lets Hl : Hp; simpl in Hl; apply permut_len in Hl;
symmetry in Hl; rew_length in Hl; apply lengthn in Hl.
destruct Hl as (b & ns´ & Heq); rewrite Heq in ×.
lets Hp´ : Hp; apply wfp_permut_opl in Hp´.
destruct Hp´ as (ns´´ & Heq´´ & Hpp).
rewrite <- Heq in Heq´´.
cut (ns = ns´´).
introv Heqns; subst¬.
clear H ns´ Hp Heq Hpp b; inductions ns.
simpls; symmetry; apply¬ wfp_opl_inv.
destruct ns´´; simpls; inverts Heq´´.
apply IHns in H1; rewrite¬ H1.
Grab Existential Variables.
exact wfp_Nil.
Qed.
Lemma wfp_swap_sym : ∀ p X Y, wfp_swap X Y p = wfp_swap Y X p.
Proof.
introv; rewrite_wfp_equal.
apply swap_sym.
Qed.
Lemma wfp_swap_involutive : ∀ X Y p, wfp_swap X Y (wfp_swap X Y p) = p.
Proof.
introv; rewrite_wfp_equal.
apply swap_involutive.
Qed.
Lemma wfp_eq_swap_send : ∀ X Y a q,
wfp_swap X Y (wfp_Send a q) = wfp_Send a (wfp_swap X Y q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_abs : ∀ p a X Y Z,
wfp_swap X Y (wfp_Abs a Z p) = wfp_Abs a ({{X, Y}}Z) (wfp_swap X Y p).
Proof.
introv.
rewrite_wfp_equal; unfold Abs; simpls.
repeat rewrite <- XHE_GoodF; fold f. fequals.
rewrite subst_on_swap; fequals.
simpl; rewrite¬ swap_gvar_involutive.
Qed.
Lemma wfp_eq_swap_gvar : ∀ X Y Z,
wfp_swap X Y (wfp_Gvar Z) = ifb (X = Z) then (wfp_Gvar Y) else ifb (Y = Z) then (wfp_Gvar X) else (wfp_Gvar Z).
Proof.
introv; rewrite_wfp_equal; cases_if; try cases_if*; subst; simpls;
fequals; unfold swap_gvar; repeat cases_if×.
Qed.
Lemma wfp_eq_swap_par : ∀ X Y p q,
wfp_swap X Y (wfp_Par p q) = wfp_Par (wfp_swap X Y p) (wfp_swap X Y q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_nil : ∀ X Y,
wfp_swap X Y wfp_Nil = wfp_Nil.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_swap_chan_involutive : ∀ m n p, wfp_swap_chan m n (wfp_swap_chan m n p) = p.
Proof.
introv; rewrite_wfp_equal; apply swap_chan_involutive.
Qed.
Lemma wfp_eq_subst_send : ∀ r X a q,
wfp_subst r X (wfp_Send a q) = wfp_Send a (wfp_subst r X q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_subst_gvar : ∀ r X Y,
wfp_subst r X (wfp_Gvar Y) = ifb (X = Y) then r else (wfp_Gvar Y).
Proof.
introv; rewrite_wfp_equal; cases_if; cases_if×.
Qed.
Lemma wfp_eq_subst_par : ∀ r X p q,
wfp_subst r X (wfp_Par p q) = wfp_Par (wfp_subst r X p) (wfp_subst r X q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_subst_nil : ∀ r X,
wfp_subst r X wfp_Nil = wfp_Nil.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_chan_send: ∀ a (p : wfprocess) m n,
wfp_swap_chan m n (wfp_Send a p) = wfp_Send ({{|m, n|}}a) (wfp_swap_chan m n p).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_chan_abs: ∀ (p : wfprocess) a X m n,
wfp_swap_chan m n (wfp_Abs a X p) = wfp_Abs ({{|m, n|}}a) X (wfp_swap_chan m n p).
Proof.
introv; rewrite_wfp_equal.
unfold Abs; simpls; repeat rewrite¬ <- Good_chan_swap; fequals.
rewrite swap_chan_on_subst; simpls¬.
Qed.
Lemma wfp_eq_swap_chan_gvar: ∀ X m n,
wfp_swap_chan m n (wfp_Gvar X) = wfp_Gvar X.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_chan_par: ∀ (p q : wfprocess) m n,
wfp_swap_chan m n (wfp_Par p q) = wfp_Par (wfp_swap_chan m n p) (wfp_swap_chan m n q).
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_eq_swap_chan_nil: ∀ m n,
wfp_swap_chan m n (wfp_Nil) = wfp_Nil.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_fresh_Msubst1 : ∀ xs (rs : list wfprocess) X (p : wfprocess),
X#p → length xs = length rs → closed_proc_list_wfp rs → X#(wfp_multisubst (combine xs rs) p).
Proof with fresh_solve.
induction xs; introv Hf Hls Hcp.
simpls¬.
rewrite length_cons in Hls. symmetry in Hls. lets (y & ys & H): (lengthn rs Hls).
subst. simpls... applys× IHxs.
rew_length in *; nat_math.
unfolds. destruct Hcp. unfolds in H. rewrite H. apply notin_empty.
Qed.
Lemma wfp_gfresh_subst_rewrite : ∀ (X:var) (p q:wfprocess),
X#p → wfp_subst q X p = p.
Proof.
introv Hf; rewrite_wfp_equal.
applys¬ gfresh_subst_rewrite.
Qed.
Lemma wfp_subst_gvar_idem : ∀ X p,
wfp_subst (wfp_Gvar X) X p = p.
Proof.
introv; rewrite_wfp_equal. apply subst_gvar_idem.
Qed.
Lemma wfp_gfresh_subst_is_swap : ∀ (X Y:var) (p : wfprocess),
Y # p → wfp_subst (wfp_Gvar Y) X p = wfp_swap X Y p.
Proof.
introv Hf; rewrite_wfp_equal. apply¬ gfresh_subst_is_swap.
Qed.
Lemma wfp_substs_commute_gg : ∀ (X Y:var) (p q r: wfprocess),
X≠Y → X#r → Y#q → wfp_subst r Y (wfp_subst q X p) = wfp_subst q X (wfp_subst r Y p).
Proof.
introv Hneq Hf1 Hf2.
rewrite_wfp_equal.
applys× substs_commute_gg.
Qed.
Lemma wfp_subst_on_subst : ∀ (X Y:var) (p q r : wfprocess),
X≠Y → X#r → wfp_subst r Y (wfp_subst q X p) =
wfp_subst (wfp_subst r Y q) X (wfp_subst r Y p).
Proof.
introv Hneq Hf; rewrite_wfp_equal.
applys¬ subst_on_subst.
Qed.
Lemma wfp_subst_decomposition_g : ∀ (X Y:var) (p q : wfprocess),
Y#p → wfp_subst q X p = wfp_subst q Y (wfp_subst (wfp_Gvar Y) X p).
Proof with freshen_up.
introv H.
rewrite_wfp_equal. applys× subst_decomposition_g.
Qed.
Lemma wfp_prod_repeat_0 : ∀ p, wfp_prod_repeat p 0 = wfp_Nil.
Proof.
introv; rewrite_wfp_equal.
Qed.
Lemma wfp_prod_repeat_S : ∀ n p, wfp_prod_repeat p (S n) = wfp_Par p (wfp_prod_repeat p n).
Proof.
inductions n; introv; try rewrite_wfp_equal.
Qed.
Ltac rewrite_wfp_subst :=
repeat rewrite wfp_eq_subst_send in *;
repeat rewrite wfp_eq_subst_gvar in *;
repeat rewrite wfp_eq_subst_par in *;
repeat rewrite wfp_eq_subst_nil in ×.
Ltac rewrite_wfp_swap :=
repeat rewrite wfp_eq_swap_send in *;
repeat rewrite wfp_eq_swap_abs in *;
repeat rewrite wfp_eq_swap_gvar in *;
repeat rewrite wfp_eq_swap_par in *;
repeat rewrite wfp_eq_swap_nil in ×.
Ltac rewrite_wfp_swap_chan :=
repeat rewrite wfp_eq_swap_chan_send in *;
repeat rewrite wfp_eq_swap_chan_abs in *;
repeat rewrite wfp_eq_swap_chan_gvar in *;
repeat rewrite wfp_eq_swap_chan_par in *;
repeat rewrite wfp_eq_swap_chan_nil in ×.
Ltac rewrite_wfp_prod :=
repeat rewrite wfp_prod_repeat_0 in *;
repeat rewrite wfp_prod_repeat_S in ×.
Ltac rewrite_wfp_pipe_multi :=
repeat rewrite wfp_pipe_eq_nil in *;
repeat rewrite wfp_pipe_to_Abs in *;
repeat rewrite wfp_multisubst_to_subst in *;
repeat rewrite wfp_multisubst_to_subst_tail in ×.
Fixpoint leave (E:fset var) (l: list (var×wfprocess)) : list (var×wfprocess) :=
match l with
| nil ⇒ nil
| a::l1 ⇒ If ((fst a) \in E) then a :: leave E l1 else leave E l1
end.
Lemma leave_inv: ∀ E l x, Mem x (leave E l) → Mem x l.
Proof.
induction l; introv Hm; simpls¬.
cases_if; rewrite Mem_cons_eq in ×. destruct¬ Hm.
right¬.
Qed.
Lemma leave_inv_r: ∀ E l x, Mem x (snd(split(leave E l))) → Mem x (snd (split l)).
Proof.
induction l; introv Hm.
simpls¬.
simpl in Hm. cases_if; rewrite snd_split_cons in *; rewrite Mem_cons_eq in ×.
destruct¬ Hm.
right¬.
Qed.
Lemma leave_nodup_r: ∀ E l, noDup (snd (split l)) → noDup (snd (split (leave E l))).
Proof.
induction l; introv Hnd.
simpls¬.
simpl leave. cases_if.
rewrite snd_split_cons in ×. simpls. destruct Hnd.
split.
introv H´. apply H0. applys× leave_inv_r.
applys¬ IHl.
rewrite snd_split_cons in Hnd. destruct Hnd. applys¬ IHl.
Qed.
Lemma leave_red_set: ∀ E l t x, length l = length t →
¬Mem x l → leave E (combine l t) = leave (E \- \{x}) (combine l t).
Proof.
induction l; introv Hls Hm.
simpls¬.
lets Hls´: Hls. rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
destruct Hls´ as (b & t´ & Ht). subst. rewrite_all length_cons in Hls.
simpl. rewrite Mem_cons_eq in Hm. rew_logic in Hm. destruct Hm as (Heq & Hm).
repeat cases_if¬.
rewrite¬ <- IHl.
rewrite in_remove in H0. rew_logic in H0. rewrite notin_singleton in H0. destruct× H0.
rewrite in_remove in H0. destruct H0. false.
Qed.
Lemma leave_not_fresh: ∀ (E:fset var) xs ps (p : wfprocess),
length xs = length ps → closed_proc_list_wfp ps → GV p \c E → wfp_multisubst (combine xs ps) p = wfp_multisubst (leave E (combine xs ps)) p.
Proof.
induction xs; introv Hls Hcp Hgv.
simpls¬.
lets Hls´: Hls. rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
destruct Hls´ as (p´ & ps´ & Hps). subst.
simpl. cases_if; simpls.
rewrite× (IHxs ps´ p).
rewrite wfp_gfresh_subst_rewrite. applys× IHxs.
applys× wfp_fresh_Msubst1.
unfolds subset. specializes Hgv a. introv H´. apply H. applys¬ Hgv.
Qed.
Lemma leave_ex: ∀ E l t, length l = length t →
∃ r, (snd (split (leave E (combine l (¬¬t))))) = ¬¬r ∧ (∀ m, Mem m r → Mem m t).
Proof.
induction l; introv Hls.
simpls. ∃ (nil:list chan). split¬. introv Hm. rewrite Mem_nil_eq in Hm. false.
lets Hls´: Hls. rewrite length_cons in Hls´. symmetry in Hls´. apply lengthn in Hls´.
destruct Hls´ as (b & t´ & Ht). subst. rewrite_all length_cons in Hls.
simpl. cases_if.
edestruct (IHl t´) as (r & Hsnd & Hfa). nat_math. ∃ (b::r). split.
rewrite snd_split_cons. simpl. rewrite¬ <- Hsnd.
introv H1. rewrite Mem_cons_eq in ×. destruct¬ H1.
edestruct (IHl t´) as (r & Hsnd & Hfa). nat_math. ∃ r. split¬.
introv H1. rewrite Mem_cons_eq in ×. right¬.
Qed.
Ltac make_wf_from_par p :=
match goal with
| [ H : Par p ?q = ?p´ |- _ ] ⇒ apply (wf_par1 p q); rewrite H; eapply wf_cond
| [ H : Par ?q p = ?p´ |- _ ] ⇒ apply (wf_par2 q p); rewrite H; eapply wf_cond
| [ H : Par ?r (Par p ?q) = ?p´ |- _ ] ⇒ apply (wf_par1 p q); apply (wf_par2 r); rewrite H; eapply wf_cond
| [ H : Par ?r (Par ?q p) = ?p´ |- _ ] ⇒ apply (wf_par2 q p); apply (wf_par2 r); rewrite H; eapply wf_cond
| [ H : Par (Par p ?q) ?r = ?p´ |- _ ] ⇒ apply (wf_par1 p q); apply (wf_par1 (Par p q) r); rewrite H; eapply wf_cond
| [ H : Par (Par ?q p) ?r = ?p´ |- _ ] ⇒ apply (wf_par2 q p); apply (wf_par1 (Par q p) r); rewrite H; eapply wf_cond
end.
Ltac lift_from_par p wfp :=
let H := fresh "H" in
assert (H : wf p) by (make_wf_from_par p); set (wfp := mkWfP p H).
Ltac lift_par p q :=
let H := fresh "H" in
assert (H : p = q) by (rewrite_wfp_equal); rewrite¬ H.
Ltac subst_wfp :=
repeat match goal with
| [H : proc ?p = [Send ?a Nil // ?X](proc ?p1) |- _] ⇒
replace ([Send a Nil // X]p1) with
(proc (wfp_subst (wfp_Send a wfp_Nil) X p1)) in H by auto
end;
repeat match goal with
| [H : proc ?p = [proc ?q // ?X](proc ?r) |- _] ⇒
replace ([proc q // X](proc r)) with
(proc (wfp_subst q X r)) in H by auto
end;
repeat match goal with
| [H : proc ?p = Par (proc ?q) (proc ?r) |- _] ⇒
replace (Par q r) with (proc (wfp_Par q r)) in H by auto
end;
repeat match goal with
| [H : proc ?p = Abs ?f ?a ?X (proc ?q) |- _] ⇒
replace (Abs f a X q) with (proc (wfp_Abs a X q)) in H by auto
end;
repeat replace Nil with (proc wfp_Nil) in × by auto;
repeat match goal with
| [H : proc _ = proc _ |- _ ] ⇒
rewrite <- wfprocess_eq in H; substs×
end.
Lemma wfp_par1_extract : ∀ p0 a p q,
{{wfp_Par p q -- LabIn a ->> AA (AbsPar1 p0 q)}} →
{{ p -- LabIn a ->> AA p0 }}.
Proof with subst_wfp.
introv H. fold (par_ag1 (AA p0) q) in H. inverts H.
destruct ap; inverts¬ H4...
destruct aq; inverts¬ H4.
Qed.
Lemma wfp_par2_extract : ∀ q0 a p q,
{{wfp_Par p q -- LabIn a ->> AA (AbsPar2 p q0)}} →
{{ q -- LabIn a ->> AA q0 }}.
Proof with subst_wfp.
introv H; fold (par_ag2 p (AA q0)) in H; inverts H.
destruct ap; inverts¬ H4.
destruct aq; inverts¬ H4...
Qed.
Ltac wfp_par_extract :=
match goal with
| [ |- context[AA ?a0]] ⇒
match goal with
| [H : context[AbsPar1 a0 _] |- _ ] ⇒ applys× wfp_par1_extract
| [H : context[AbsPar2 _ a0] |- _ ] ⇒ applys× wfp_par2_extract
end
end.
Lemma wfp_subst_lvar : ∀ (p q : wfprocess) X l,
l \notin (E X p) → l \notin (E X q) → [Lvar l // X]p = [Lvar l // X]q → p = q.
Proof with (freshen_up; try solve [solve_wfp_size]).
induction p using (measure_induction wfp_size).
introv Hlp Hlq Heqs.
destruct_wf p; destruct_wf q; try solve [simpls~; try cases_if; inverts Heqs].
simpls; inverts Heqs. fequals×. eapply H; try eassumption...
rename X0 into X´; rename p0 into p´.
rename a0 into b; rename X1 into Y´; rename p into q´.
lets (Z & Hfz) : find_fresh (proc p´ :: proc q´ :: nil);
rewrite Forall_to_conj_2 in Hfz; destruct Hfz as (Hfzp & Hfzq).
lets Heqp : Abs_eq p´ a X´ Z Hfzp.
lets Heqq : Abs_eq q´ b Y´ Z Hfzq.
assert (Hwfsp : wf ([Gvar Z // X´] p´)).
apply¬ wf_subst.
assert (Hwfsq : wf ([Gvar Z // Y´] q´)).
apply¬ wf_subst.
remember (mkWfP ([Gvar Z // X´]p´) Hwfsp) as wfsp.
remember (mkWfP ([Gvar Z // Y´]q´) Hwfsq) as wfsq.
replace (wfp_Abs a X´ p´) with (wfp_Abs a Z wfsp) in × by
(rewrite Heqwfsp; rewrite_wfp_equal).
replace (wfp_Abs b Y´ q´) with (wfp_Abs b Z wfsq) in × by
(rewrite Heqwfsq; rewrite_wfp_equal).
clear Heqwfsp Heqwfsq Hwfsp Hwfsq Hfzp Hfzq Heqp Heqq p´ q´ X´ Y´.
rename wfsp into p´; rename wfsq into q´.
inverts Heqs.
elim (classic (X = Z)); intro Hneq; subst.
assert (Hfzp : Z # ([Lvar (f Z p´) // Z]p´)) by fresh_solve.
assert (Hfzq : Z # ([Lvar (f Z p´) // Z]q´)) by fresh_solve.
rewrite¬ gfresh_subst_rewrite in H3.
rewrite (gfresh_subst_rewrite _ ([Lvar (f Z p´) // Z] q´)) in H3; auto.
fequals. eapply H; try eassumption; try apply f_is_good...
rewrite H2; apply f_is_good.
elim (classic (Z # p´)); intro Hfzp.
assert (Hfzq : Z # q´).
rewrite GoodFresh_iff in ×. fold f in *; rewrite¬ <- H2.
rewrite¬ (gfresh_subst_rewrite Z p´) in H3.
rewrite¬ (gfresh_subst_rewrite Z q´) in H3.
fequals. eapply H; try eassumption...
simpls; repeat cases_if×.
assert (E X p´ = \{})...
apply gfresh_E_empty; fresh_solve.
rewrite¬ H0.
assert (E X p´ = \{}).
apply gfresh_E_empty; fresh_solve.
rewrite¬ H0.
rename f into Hf.
rewrite gfresh_subst_rewrite in Hlp. Focus 2. auto.
unfold notin in *; rewrite in_union in ×. rew_logic in Hlp; jauto.
rewrite gfresh_subst_rewrite in Hlp. Focus 2. auto.
unfold notin in *; rewrite in_union in ×. rew_logic in Hlp; jauto.
simpls; repeat cases_if×.
assert (E X q´ = \{}).
apply gfresh_E_empty; fresh_solve.
rewrite¬ H0.
rewrite gfresh_subst_rewrite in Hlq; [ | auto].
unfold notin in *; rewrite in_union in ×. rew_logic in Hlq; jauto.
assert (E X q´ = \{}).
apply gfresh_E_empty.
symmetry in H3; fresh_solve.
rewrite¬ H0.
rewrite gfresh_subst_rewrite in Hlq; [ | auto].
unfold notin in *; rewrite in_union in ×. rew_logic in Hlp; jauto.
assert (Hfzp1 : f Z p´ ## p´) by eauto.
assert (Hfzq1 : f Z p´ ## q´) by eauto.
elim (classic (X # p´)); elim (classic (X # q´)); intros Hfxq Hfxp.
apply (gfresh_in_subst_p_q X Z q´ (Lvar (f Z p´))) in Hfxq...
apply (gfresh_in_subst_p_q X Z p´ (Lvar (f Z p´))) in Hfxp...
rewrite¬ gfresh_subst_rewrite in H3.
rewrite¬ (gfresh_subst_rewrite X) in H3.
fequals. eapply H; try apply f_is_good; try eassumption...
rewrite H2; apply f_is_good.
simpls; repeat cases_if*;
try solve [apply gfresh_from_subst in f; jauto; false~];
try solve [apply gfresh_from_subst in f0; jauto; false~].
rename f into Hfp; rename n into Hfq.
assert (Hneql: l ≠ f Z p´).
rewrite H2. unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlq. rewrite¬ in_singleton in H0.
assert (Hfzq : ¬ Z # q´).
rewrite GoodFresh_iff in ×. fold f in *; rewrite¬ <- H2.
assert ([Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]p´)) =
[Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]q´))).
rewrite¬ H3.
rewrite substs_commute_gg in H0; auto...
rewrite (substs_commute_lg (f Z p´) X _ (Lvar l)) in H0; auto...
rewrite¬ <- subst_decomposition_l in H0; auto...
rewrite¬ <- subst_decomposition_l in H0; auto...
repeat rewrite subst_gvar_idem in H0.
fequals. eapply H; try eassumption; auto...
assert (E X p´ = \{}).
apply gfresh_E_empty.
symmetry in H3; fresh_solve.
rewrite¬ H1.
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlq.
introv Hyp; apply H4.
rewrite E_subst_inv in Hyp; eassumption.
rewrite H2. apply f_is_good.
fresh_solve.
rewrite¬ <- E_subst_inv; apply f_is_good.
false n; fresh_solve.
simpls; repeat cases_if*;
try solve [apply gfresh_from_subst in f; jauto; false~];
try solve [apply gfresh_from_subst in f0; jauto; false~].
rename f into Hfq; rename n into Hfp.
assert (Hneql: l ≠ f Z p´).
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlp. rewrite¬ in_singleton in H0.
assert (Hfzq : ¬ Z # q´).
rewrite GoodFresh_iff in ×. fold f in *; rewrite¬ <- H2.
assert ([Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]p´)) =
[Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]q´))).
rewrite¬ H3.
rewrite substs_commute_lg in H0...
rewrite (substs_commute_lg (f Z p´) X _ (Lvar l)) in H0...
do 2 rewrite¬ <- subst_decomposition_l in H0; try apply f_is_good.
repeat rewrite subst_gvar_idem in H0.
fequals. eapply H... Focus 3. eassumption.
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlp.
introv Hyp; apply H4.
rewrite E_subst_inv in Hyp; eassumption.
assert (E X q´ = \{}).
apply¬ gfresh_E_empty.
rewrite¬ H1.
rewrite H2. apply f_is_good.
false¬ n0; fresh_solve.
simpls; repeat cases_if*;
try solve [apply gfresh_from_subst in f; jauto; false~];
try solve [apply gfresh_from_subst in f0; jauto; false~].
rename n0 into Hfq; rename n into Hfp.
assert (Hneql: l ≠ f Z p´).
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlp. rewrite¬ in_singleton in H0.
assert (Hfzq : ¬ Z # q´).
rewrite GoodFresh_iff in ×. fold f in *; rewrite¬ <- H2.
assert ([Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]p´)) =
[Gvar Z /// f Z p´]([Lvar l // X]([Lvar (f Z p´) // Z]q´))).
rewrite¬ H3.
rewrite substs_commute_lg in H0...
rewrite (substs_commute_lg (f Z p´) X _ (Lvar l)) in H0...
do 2 rewrite¬ <- subst_decomposition_l in H0; try apply f_is_good.
repeat rewrite subst_gvar_idem in H0.
fequals. eapply H; try eassumption...
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlp.
introv Hyp; apply H4.
rewrite E_subst_inv in Hyp; eassumption.
unfold notin in *; rewrite in_union in ×.
rew_logic in *; inverts Hlq.
introv Hyp; apply H4.
rewrite E_subst_inv in Hyp; eassumption.
rewrite H2; apply f_is_good.
simpls; repeat cases_if; inverts× Heqs.
rewrite <- e. rewrite¬ <- e0.
simpls; inverts Heqs.
unfold notin in *; rewrite in_union in *; rew_logic in ×.
fequals; eapply H; try eassumption; try apply f_is_good; jauto...
Qed.
Lemma wfp_subst_lvar_XY : ∀ X Y, X ≠ Y → ∀ (p q : wfprocess) l,
l \notin (E X p) → l \notin (E Y q) → [Lvar l // X]p = [Lvar l // Y]q → (p = wfp_subst (wfp_Gvar X) Y q ∧ X # q).
Proof with (jauto; freshen_up; try solve_wfp_size).
introv Hneq.
induction p using (measure_induction wfp_size).
introv Hlp Hlq Hsub.
assert (Hsaux : ∀ (p : wfprocess) X l, ¬ l \in E X p → proc p = [Gvar X /// l]([Lvar l // X]p)).
clear; introv Hnl.
rewrite¬ <- subst_decomposition_l.
rewrite¬ subst_gvar_idem.
elim (classic (X # p)); elim (classic (Y # q)); introv Hfy Hfx.
repeat (rewrite gfresh_subst_rewrite in Hsub; auto).
assert (p = q) by (rewrite_wfp_equal); substs.
splits×. rewrite_wfp_equal. rewrite¬ gfresh_subst_rewrite.
rewrite gfresh_subst_rewrite in Hsub; auto.
assert (Hfxq : X # q).
rewrite Hsub in Hfx; clear dependent p.
apply gfresh_from_subst in Hfx...
assert (wf ([Lvar l // Y]q)).
rewrite¬ <- Hsub.
false; clear dependent X. clear dependent p.
rename q into p; rename Y into X. gen X l.
induction p using (measure_induction wfp_size).
introv Hfx Hnl Hwf.
lets Hcp : wf_characterize p.
inverts Hcp as Hcp.
destruct Hcp as (a & p´ & Heq); subst.
simpls. rewrite gfresh_send in Hfx.
specializes¬ H Hfx...
inverts× Hwf.
inverts Hcp as Hcp.
destruct Hcp as (a & Y & p´ & Heq); subst.
simpls. unfold Abs in *; simpls. rewrite gfresh_receive in Hfx.
assert (Hneq : X ≠ Y).
intro Heq; subst; apply Hfx. fresh_solve.
cases_if×. clear n.
unfold notin in *; rewrite in_union in *; rew_logic in ×.
destruct Hnl as (Hnl1 & Hnl2). rewrite in_singleton in Hnl1.
rewrite substs_commute_gg in Hwf...
lets Hwfr : wf_receive Hwf.
assert (Hfy : Y # ([Lvar (f Y p´) // Y]([Lvar l // X]p´))) by
fresh_solve.
specializes Hwfr Hfy; inverts Hwfr; clear H1.
assert ((f Y p´) ## ([Lvar l // X]p´)) by fresh_solve.
rewrite substs_commute_gg in H0...
rewrite substs_commute_lg in H0...
replace ([Gvar Y /// f Y p´]([Lvar (f Y p´) // Y]p´))
with (proc p´) in H0.
apply H in H0...
introv Hf; apply Hfx; fresh_solve.
rewrite <- E_subst_inv in Hnl2; auto.
rewrite¬ <- Hsaux; apply f_is_good.
inverts Hcp as Hcp.
destruct Hcp as (Y & Heq); subst.
simpls; cases_if×. inverts Hwf.
rewrite gfresh_gvar in ×. tauto.
inverts Hcp as Hcp.
destruct Hcp as (p1 & p2 & Heq); subst.
simpls; inverts Hwf.
unfold notin in *; rewrite in_union in *;
rewrite gfresh_par_iff in Hfx; rew_logic in ×.
inverts Hfx; specializes¬ H H0...
simpls. apply Hfx...
rewrite gfresh_subst_rewrite with (X := Y) in Hsub; auto.
rename p into r; rename q into p; rename r into q.
rename X into Z; rename Y into X; rename Z into Y.
rename Hfx into Hfz; rename Hfy into Hfx; rename Hfz into Hfy.
rename Hlp into Hlr; rename Hlq into Hfp; rename Hlr into Hlq.
symmetry in Hsub.
assert (Hfxq : X # q).
elim (classic (X = Y)); intro Hneqv; subst. false×.
rewrite Hsub in Hfx; fresh_solve.
assert (wf ([Lvar l // Y]q)).
rewrite¬ <- Hsub.
false; clear dependent X. clear dependent p.
rename q into p; rename Y into X. gen X l.
induction p using (measure_induction wfp_size).
introv Hfx Hnl Hwf.
lets Hcp : wf_characterize p.
inverts Hcp as Hcp.
destruct Hcp as (a & p´ & Heq); subst.
simpls. rewrite gfresh_send in Hfx.
specializes¬ H Hfx...
inverts× Hwf.
inverts Hcp as Hcp.
destruct Hcp as (a & Y & p´ & Heq); subst.
simpls. unfold Abs in *; simpls. rewrite gfresh_receive in Hfx.
assert (Hneq : X ≠ Y).
intro Heq; subst; apply Hfx; fresh_solve.
cases_if×. clear n.
unfold notin in *; rewrite in_union in *; rew_logic in ×.
destruct Hnl as (Hnl1 & Hnl2). rewrite in_singleton in Hnl1.
rewrite substs_commute_gg in Hwf...
lets Hwfr : wf_receive Hwf.
assert (Hfy : Y # ([Lvar (f Y p´) // Y]([Lvar l // X]p´))) by fresh_solve.
specializes Hwfr Hfy; inverts Hwfr; clear H1.
assert ((f Y p´) ## ([Lvar l // X]p´)) by fresh_solve.
rewrite substs_commute_gg in H0...
rewrite substs_commute_lg in H0...
replace ([Gvar Y /// f Y p´]([Lvar (f Y p´) // Y]p´))
with (proc p´) in H0.
apply H in H0; auto...
introv Hf; apply Hfx; fresh_solve.
rewrite <- E_subst_inv in Hnl2; auto.
rewrite¬ <- Hsaux. apply f_is_good.
inverts Hcp as Hcp.
destruct Hcp as (Y & Heq); subst.
simpls; cases_if×. inverts Hwf.
rewrite gfresh_gvar in ×. tauto.
inverts Hcp as Hcp.
destruct Hcp as (p1 & p2 & Heq); subst.
simpls; inverts Hwf.
unfold notin in *; rewrite in_union in *;
rewrite gfresh_par_iff in Hfx; rew_logic in ×.
inverts Hfx; specializes¬ H H0...
simpls. apply Hfx...
lets Hcp : wf_characterize p; lets Hcq : wf_characterize q.
inverts Hcp as Hcp.
destruct Hcp as (a & p´ & Heq); subst.
inverts Hcq as Hcq.
destruct Hcq as (b & q´ & Heq); subst; simpls...
inverts Hsub; apply H in H2... split...
rewrite wfprocess_eq in *; simpls; fequals×...
inverts Hcq as Hcq.
destruct Hcq as (b & Z & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (Z & Heq); subst; simpls; cases_if; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (q1 & q2 & Heq); subst; simpls; inverts Hsub.
simpls; inverts Hsub.
inverts Hcp as Hcp.
destruct Hcp as (a & X´ & p´ & Heq); subst.
inverts Hcq as Hcq.
destruct Hcq as (b & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (b & Y´ & q´ & Heq); subst; simpls.
unfold Abs in *; simpls; rewrite gfresh_receive in ×.
inverts Hsub; rename b into a; repeat cases_if×.
elim (classic (X = X´)); intro Hneqv1; subst.
false; apply Hfx; fresh_solve.
elim (classic (Y = Y´)); intro Hneqv2; subst.
false; apply Hfy; fresh_solve.
unfold notin in *; rewrite in_union in *; rew_logic in *;
rewrite in_singleton in *; inverts Hlp; inverts Hlq.
split. rewrite_wfp_equal; unfold Abs; simpls; fequals×.
rewrite subst_decomposition_l with (p := [_ // _]q´) (x := l); fresh_solve.
rewrite <- H2. rewrite <- H3.
rewrite¬ substs_commute_gg...
rewrite substs_commute_lg...
rewrite¬ <- Hsaux. rewrite <- E_subst_inv in H1; auto.
assert (X # [Lvar l // Y]([Lvar (f X´ p´) // Y´]q´)).
rewrite <- H3; fresh_solve.
remember ([Lvar (f X´ p´) // Y´]q´) as q´´; fresh_solve.
inverts Hcq as Hcq.
destruct Hcq as (Z & Heq); subst; simpls; cases_if; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (q1 & q2 & Heq); subst; simpls; inverts Hsub.
simpls; inverts Hsub.
inverts Hcp as Hcp.
destruct Hcp as (X´ & Heq); subst.
inverts Hcq as Hcq.
destruct Hcq as (b & q´ & Heq); subst; simpls; cases_if; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (b & Z & q´ & Heq); subst; simpls; cases_if; inverts Hub.
inverts Hcq as Hcq.
destruct Hcq as (Z & Heq); subst; simpls; repeat cases_if; subst.
split.
rewrite_wfp_equal; cases_if×.
rewrite¬ gfresh_gvar.
rewrite gfresh_gvar in Hfx; false×.
inverts Hcq as Hcq.
destruct Hcq as (q1 & q2 & Heq); subst; simpls; cases_if; inverts Hsub.
simpls; cases_if; inverts Hsub.
inverts Hcp as Hcp.
destruct Hcp as (p1 & p2 & Heq); subst.
inverts Hcq as Hcq.
destruct Hcq as (b & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (b & Z & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (Z & Heq); subst; simpls; cases_if; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (q1 & q2 & Heq); subst; simpls.
inverts Hsub.
unfold notin in *; rewrite in_union in *; rew_logic in ×.
inverts Hlp; inverts Hlq.
apply H in H1; auto...
apply H in H2; auto...
inverts H1; inverts H2; splits...
rewrite_wfp_equal.
simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (b & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (b & Z & q´ & Heq); subst; simpls; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (Z & Heq); subst; simpls; cases_if; inverts Hsub.
inverts Hcq as Hcq.
destruct Hcq as (q1 & q2 & Heq); subst; simpls; inverts Hsub.
splits...
rewrite_wfp_equal...
Qed.
Lemma wfp_Abs_eq : ∀ (p : wfprocess) a X Y, Y#p → wfp_Abs a X p = wfp_Abs a Y (wfp_subst (wfp_Gvar Y) X p).
Proof.
introv Hf; rewrite_wfp_equal.
apply¬ Abs_eq.
Qed.
Lemma wfp_Abs_equal : ∀ p q a b X Y,
(wfp_Abs a X p = wfp_Abs b Y q) ↔
a = b ∧ (ifb (X = Y) then (p = q) else (p = wfp_subst (wfp_Gvar X) Y q ∧ X # q)).
Proof.
introv; splits~; introv Hyp.
Focus 2.
cases_if*; inverts Hyp; subst¬.
inverts¬ H0.
symmetry; apply¬ wfp_Abs_eq.
cases_if*; subst.
inverts Hyp.
splits¬. apply wfp_subst_lvar in H2; auto.
apply f_is_good.
rewrite H1; apply f_is_good.
inverts Hyp; split¬.
eapply wfp_subst_lvar_XY; try eassumption.
apply f_is_good.
rewrite H1; apply f_is_good.
Qed.
Lemma wfp_eq_subst_abs1 : ∀ r a X q,
wfp_subst r X (wfp_Abs a X q) = wfp_Abs a X q.
Proof.
introv; rewrite_wfp_equal. unfold Abs; simpl; fequals.
rewrite¬ gfresh_subst_rewrite; fresh_solve.
Qed.
Lemma wfp_eq_subst_abs2 : ∀ (r : wfprocess) a X Y q,
X ≠ Y → Y # r → wfp_subst r X (wfp_Abs a Y q) = wfp_Abs a Y (wfp_subst r X q).
Proof with freshen_up.
introv Hneq Hf; rewrite_wfp_equal.
rewrite¬ substs_commute_gg...
replace (f Y q) with (f Y ([r // X]q)) by (symmetry; apply¬ XHP_GoodF); auto.
Qed.
Lemma wfp_eq_subst_abs3 : ∀ (r : wfprocess) a X Y (q : wfprocess),
X ≠ Y → (∀ Z, Z ≠ X → Z # r → Z # q → wfp_subst r X (wfp_Abs a Y q) = wfp_Abs a Z (wfp_subst r X (wfp_subst (wfp_Gvar Z) Y q))).
Proof.
introv Hneq Hfzx Hfzr Hfzq.
rewrite wfp_Abs_eq with (Y := Z); auto.
rewrite¬ wfp_eq_subst_abs2.
Qed.
Lemma wfp_trans_in_chan_eq : ∀ p a b X fp,
{{wfp_Abs a X p -- LabIn b ->> AA fp}} → a = b.
Proof.
introv Ht; inverts¬ Ht.
Qed.
Lemma wfp_trans_in_abs_eq : ∀ p a X fp,
{{wfp_Abs a X p -- LabIn a ->> AA fp}} →
fp = AbsPure X p ∨ ∃ Y, Y ≠ X ∧ Y # p ∧ fp = AbsPure Y (wfp_subst (wfp_Gvar Y) X p).
Proof.
introv Ht. inverts Ht.
tests : (X = X0).
left; fequals.
apply wfp_subst_lvar in H2; substs~; try apply f_is_good.
rewrite H1; apply f_is_good.
right.
apply wfp_subst_lvar_XY in H2; auto; try apply f_is_good.
∃ X0; splits*; fequals×.
rewrite H1; apply f_is_good.
Qed.
Lemma subst_eq_rewrite : ∀ p q X Y,
(p = [Gvar X // Y] q ∧ X # q) →
(q = [Gvar Y // X] p ∧ Y # p).
Proof.
induction p using (measure_induction size).
destruct p; destruct q; introv (Heq & Hfx); simpls;
try solve [repeat cases_if; inverts× Heq].
inverts Heq; rewrite gfresh_send in ×.
tests Hyp : (X = Y).
repeat rewrite× subst_gvar_idem.
rewrite¬ <- subst_decomposition_g.
rewrite subst_gvar_idem; splits~; fresh_solve.
inverts Heq; rewrite gfresh_receive in ×.
tests Hyp : (X = Y).
repeat rewrite× subst_gvar_idem.
rewrite¬ <- subst_decomposition_g.
rewrite subst_gvar_idem; splits~; fresh_solve.
splits*; fresh_solve.
repeat cases_if*; inverts Heq; splits; subst~;
rewrite gfresh_gvar in *; intuition.
inverts Heq; rewrite gfresh_par_iff in ×.
tests Hyp : (X = Y).
repeat rewrite× subst_gvar_idem.
repeat rewrite× <- subst_decomposition_g.
repeat rewrite subst_gvar_idem; splits~; fresh_solve.
splits~; fresh_solve.
Qed.
Lemma wfp_subst_eq_rewrite : ∀ p q X Y,
(p = wfp_subst (wfp_Gvar X) Y q ∧ X # q) →
(q = wfp_subst (wfp_Gvar Y) X p ∧ Y # p).
Proof.
introv; repeat rewrite wfprocess_eq in *; simpls.
apply subst_eq_rewrite.
Qed.