Library HOC08SubstLemmas
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Lemma swap_name_left : ∀ m n,
{{|m,n|}}m = n.
Proof.
introv. unfolds. cases_if¬.
Qed.
Lemma swap_name_right : ∀ m n,
{{|m,n|}}n = m.
Proof.
introv. unfolds. cases_if¬. cases_if¬.
Qed.
Lemma wfp_swap_chan_equal : ∀ p m, wfp_swap_chan m m p = p.
Proof.
introv; rewrite_wfp_equal.
apply swap_chan_equal.
Qed.
Lemma wfp_swap_equal : ∀ p X, wfp_swap X X p = p.
Proof.
introv; rewrite_wfp_equal.
apply swap_equal.
Qed.
Lemma wfp_swap_chan_on_subst: ∀ m n p q X,
wfp_swap_chan m n (wfp_subst q X p) = wfp_subst (wfp_swap_chan m n q) X (wfp_swap_chan m n p).
Proof.
introv; rewrite_wfp_equal.
apply swap_chan_on_subst.
Qed.
Lemma wfp_swap_on_subst : ∀ (X X´ Y:var) (p q : wfprocess),
wfp_swap X X´(wfp_subst q Y p) = wfp_subst (wfp_swap X X´ q) ({{X,X´}} Y) (wfp_swap X X´ p).
Proof.
introv; rewrite_wfp_equal.
apply swap_on_subst.
Qed.
Lemma wfp_subst_on_swap : ∀ X X´ Y p q, wfp_subst q Y (wfp_swap X X´ p) = wfp_swap X X´ (wfp_subst (wfp_swap X X´ q) ({{X,X´}}Y) p).
Proof.
introv; rewrite_wfp_equal.
apply subst_on_swap.
Qed.
Lemma wfp_gfresh_swap_rewrite : ∀ X X´ (p : wfprocess),
X # p → X´ # p → wfp_swap X X´ p = p.
Proof with freshen_up.
introv; rewrite_wfp_equal.
apply gfresh_swap_rewrite.
Qed.
Lemma wfp_subst_on_subst_same : ∀ X (p q r : wfprocess),
X#r → wfp_subst r X (wfp_subst q X p) =
wfp_subst (wfp_subst r X q) X p.
Proof.
introv Hf; rewrite_wfp_equal.
apply¬ subst_on_subst_same.
Qed.
Lemma wfp_fresh_Msubst_lemma : ∀ Xs ps (p : wfprocess), length Xs = length ps →
closed_proc_list_wfp ps → Forall (fun X ⇒ X#p) Xs → wfp_multisubst (combine Xs ps) p = p.
Proof.
induction Xs; introv Hl Hcp Hf.
simpls¬.
lets Hl´: Hl. rewrite length_cons in Hl. symmetry in Hl. apply lengthn in Hl.
destruct Hl as (p0 & ps´ & Hp). subst. inverts Hf. simpls.
rewrite× wfp_gfresh_subst_rewrite. applys× wfp_fresh_Msubst1.
Qed.
Lemma wfp_fresh_chan_swap: ∀ m n (p : wfprocess), m###p → n###p → wfp_swap_chan m n p = p.
Proof.
induction p using wfp_ind; introv Hf1 Hf2; rewrite_wfp_swap_chan; auto.
rewrite IHp; simpls; fresh_solve. fequals.
unfold swap_name; repeat cases_if*; subst; rewrite cfresh_send in Hf1, Hf2; false×.
rewrite IHp; rewrite wfp_cfresh_Abs in *; jauto. fequals.
unfold swap_name; repeat cases_if*; substs×.
simpls; rewrite cfresh_par_iff in Hf1, Hf2.
rewrite× IHp1; rewrite× IHp2.
Qed.
Lemma wfp_swap_chan_on_subst1: ∀ m n p q X,
(wfp_swap_chan m n (wfp_subst q X p)) = wfp_subst (wfp_swap_chan m n q) X (wfp_swap_chan m n p).
Proof.
introv; rewrite_wfp_equal.
apply swap_chan_on_subst.
Qed.
Lemma wfp_subst_comm_cp: ∀ (p q r : wfprocess), closed_process p → closed_process q →
∀ X Y, X≠Y → wfp_subst p X (wfp_subst q Y r) = wfp_subst q Y (wfp_subst p X r).
Proof.
introv Hc1 Hc2 Hneq. rewrite wfp_subst_on_subst.
rewrite¬ (wfp_gfresh_subst_rewrite X q p).
apply¬ wfp_fresh_cp.
apply¬ sym_not_eq.
apply¬ wfp_fresh_cp.
Qed.
Lemma wfp_subst_on_pipe: ∀ a X XS (p r : wfprocess),
¬Mem X XS → closed_process r → wfp_subst r X (wfp_pipe a XS p) = wfp_pipe a XS (wfp_subst r X p).
Proof with (repeat rewrite_wfp_pipe_multi; jauto).
induction XS; introv Hnm Hcr...
rewrite Mem_cons_eq in Hnm; rew_logic in ×.
rewrite× wfp_eq_subst_abs2. rewrite× IHXS.
apply¬ wfp_fresh_cp.
Qed.
Lemma wfp_mult_sub_commute: ∀ p (XS:list var), noDup XS →
∀ lr, closed_proc_list_wfp lr → length XS = length lr → ∀ X (r : wfprocess),
¬Mem X XS → closed_process r → wfp_subst r X (wfp_multisubst (combine XS lr) p) = wfp_multisubst (combine XS lr) (wfp_subst r X p).
Proof.
induction XS; induction lr; simpls~; introv H0 H1 H2 H3.
false.
clear IHlr.
rewrite× wfp_subst_comm_cp. rewrite× <- IHXS.
introv Hmem. apply H2. constructor¬.
introv Heq. apply H2. rewrite Heq. constructor.
Qed.
Lemma wfp_mult_sub_separate2: ∀ (l1 l2:list (var×wfprocess)) p,
wfp_multisubst (l1 ++ l2) p = wfp_multisubst l1 (wfp_multisubst l2 p).
Proof.
induction l1; introv.
simpls¬.
rew_app; simpls. rewrite¬ IHl1.
Qed.
Lemma wfp_mult_sub_commute1: ∀ (xs : list var) (rs : list wfprocess) (l:list (var×wfprocess)) p, length xs = length rs →
noDup xs → closed_proc_list_wfp rs → l = combine xs rs →
∀ x (r : wfprocess), ¬Mem x xs → closed_process r → wfp_multisubst ((x,r)::nil)(wfp_multisubst l p) = wfp_multisubst l (wfp_multisubst ((x,r)::nil) p).
Proof.
induction xs; induction rs; introv H0 H1 H2 H3 H4 H5; substs; simpls¬.
false.
rewrite_wfp_pipe_multi.
erewrite <- IHxs; repeat rewrite H; eauto; intuition.
simpl; rewrite¬ wfp_subst_comm_cp.
intro H8; apply H4; rewrite H8; constructor.
apply H4. constructor¬.
Qed.
Lemma wfp_mult_sub_commute3: ∀ (l1 l2:(list (var×wfprocess))) p,
noDup (fst (split (l1 ++ l2))) →
closed_proc_list_wfp (snd (split l1)) → closed_proc_list_wfp (snd (split l2)) →
wfp_multisubst l2 (wfp_multisubst l1 p) = wfp_multisubst l1 (wfp_multisubst l2 p).
Proof.
induction l1; introv Hnd Hcp1 Hcp2.
simpls¬.
rewrite <- (app_cons_one a l1). rewrite_all wfp_mult_sub_separate2.
destruct a.
rewrite× <- (wfp_mult_sub_commute1 (fst (split l2)) (snd (split l2)) l2 (wfp_multisubst l1 p)).
rewrite× IHl1.
rew_app in Hnd. autorewrite with rew_split in ×. simpls×.
rew_app in Hnd. autorewrite with rew_split in ×. simpls×.
autorewrite with rew_split; reflexivity.
rewrite fst_split_step in Hnd. applys× nodup_app_inv.
rew_app in Hnd. autorewrite with rew_split in ×. simpls.
rewrite fst_split_step in Hnd. rewrite Mem_app_or_eq in Hnd.
introv H. apply Hnd. right¬.
autorewrite with rew_split in ×. simpls×.
Qed.
Lemma wfp_mult_sub_par: ∀ xs rs p q, length xs = length rs →
wfp_multisubst (combine xs rs) (wfp_Par p q) =
wfp_Par (wfp_multisubst (combine xs rs) p) (wfp_multisubst (combine xs rs) q).
Proof with (rewrite_wfp_subst; jauto).
induction xs; introv Hls.
simpls¬.
lets Hls´: Hls. rewrite length_cons in Hls. symmetry in Hls. apply lengthn in Hls.
destruct Hls as (r & rs´ & Hxs). subst. simpl. rewrite IHxs...
Qed.
Lemma wfp_mult_sub_Abs: ∀ a X xs (rs : list wfprocess) (p : wfprocess), length xs = length rs →
¬Mem X xs → Forall (fun p : wfprocess ⇒ X#p) rs →
wfp_multisubst (combine xs rs) (wfp_Abs a X p) = wfp_Abs a X (wfp_multisubst (combine xs rs) p).
Proof.
induction xs; introv Hls Hm Hfs.
simpls¬.
lets Hls´: Hls. rewrite length_cons in Hls. symmetry in Hls. apply lengthn in Hls.
destruct Hls as (r & rs´ & Hxs). subst. simpls.
rewrite Mem_cons_eq in Hm. rew_logic in Hm. destruct Hm as (Hneq & Hnm).
rewrite_all length_cons in Hls´. inverts Hfs as Hfr Hfrs. rewrite¬ IHxs.
rewrite¬ wfp_eq_subst_abs2.
Qed.
Lemma wfp_subst_on_inst_Abs : ∀ fp (p : wfprocess) X a (Ht : {{p -- LabIn a ->> AA fp}}) (r : wfprocess), closed_process r →
X # p → wfp_inst_Abs fp r = wfp_subst r X (wfp_inst_Abs fp (wfp_Gvar X)).
Proof with (rewrite_wfp_subst; jauto).
induction fp; intros; simpl.
tests : (X = v).
rewrite¬ wfp_subst_gvar_idem.
inverts Ht. rewrite wfp_gfresh_Abs in *; inverts× H0.
rewrites¬ <- wfp_subst_decomposition_g.
destruct ap; inverts H1.
destruct aq; inverts H1.
inverts Ht.
destruct ap; inverts H1.
assert (Hfp0 : X # p0) by (simpls; rewrite gfresh_par_iff in *; jauto).
assert (Hfp : X # w) by (simpls; rewrite gfresh_par_iff in *; jauto)...
fequals.
specialize (IHfp p0 X a H4 r H Hfp0)...
rewrites¬ wfp_gfresh_subst_rewrite.
destruct aq; inverts H1.
inverts Ht.
destruct ap; inverts H1.
destruct aq; inverts H1.
assert (Hfp1 : X # w) by (simpls; rewrite gfresh_par_iff in *; jauto).
assert (Hfp : X # q) by (simpls; rewrite gfresh_par_iff in *; jauto)...
fequals.
rewrites¬ wfp_gfresh_subst_rewrite.
specialize (IHfp q X a H4 r H Hfp)...
Qed.
Lemma wfp_subst_on_inst_Abs2 : ∀ p a X Y fp,
{{p -- LabIn a ->> AA fp}} → Y # p →
(wfp_inst_Abs fp (wfp_Gvar X)) =
(wfp_subst (wfp_Gvar X) Y (wfp_inst_Abs fp (wfp_Gvar Y))).
Proof.
induction p using (measure_induction wfp_size).
destruct_wf p; introv Ht Hf; try solve [inverts Ht].
lets Heq : wfp_trans_in_chan_eq Ht; subst.
lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst; simpl.
tests Hneq : (X = Y).
rewrite¬ wfp_subst_gvar_idem.
rewrite¬ <- wfp_subst_decomposition_g.
rewrite wfp_gfresh_Abs in Hf; inverts× Hf.
destruct Hyp as (Z & Hneq & Hfz & Heq); subst; simpl.
rewrite¬ <- wfp_subst_decomposition_g.
rewrite <- wfp_subst_decomposition_g with (X := X); auto.
tests Hneq2 : (X = Y).
rewrite¬ wfp_subst_gvar_idem.
rewrite¬ <- wfp_subst_decomposition_g.
rewrite wfp_gfresh_Abs in Hf; inverts× Hf.
inverts Ht; subst_wfp.
destruct ap; inverts H4; rename a0 into p1´; simpls;
rewrite gfresh_par_iff in Hf; rewrite_wfp_subst. fequals.
apply (H p1) with (a := a); jauto; try solve_wfp_size.
rewrite× wfp_gfresh_subst_rewrite.
destruct aq; inverts H4; rename a0 into p2´; simpls;
rewrite gfresh_par_iff in Hf; rewrite_wfp_subst. fequals.
rewrite× wfp_gfresh_subst_rewrite.
apply (H p2) with (a := a); jauto; try solve_wfp_size.
Qed.
Lemma wfp_closed_proc_permut : ∀ (l l´: list wfprocess),
closed_proc_list_wfp l → permut l l´ → closed_proc_list_wfp l´.
Proof.
induction l using (measure_induction length); destruct l; introv Hc Hp.
apply permut_sym in Hp; apply permut_of_nil in Hp; rewrite Hp; constructor.
lets Hl : Hp; apply permut_len in Hp.
rew_length in Hp; symmetry in Hp; apply lengthn in Hp.
destruct Hp as (w´ & l´´ & Heq); subst; split.
rewrite wfp_cpl_forall in Hc; rewrite <- Forall_Mem in Hc; specialize (Hc w´); apply Hc.
apply permut_mem with (l := (w´ :: l´´)); try constructor; applys¬ permut_sym.
elim (classic (w = w´)); introv Hneq; subst.
rewrite <- permut_cons_iff in Hl.
applys× (H l); try inverts¬ Hc.
rew_length; nat_math.
assert (Hmwl´´ : Mem w l´´).
cut (Mem w (w´ :: l´´)).
introv Hm; rewrites× Mem_cons_eq in Hm.
apply permut_mem with (l := w :: l); auto; constructor.
assert (Hmw´l : Mem w´ l).
cut (Mem w´ (w :: l)).
introv Hm; rewrites Mem_cons_eq in Hm; inverts× Hm.
apply permut_mem with (l := w´ :: l´´); try applys¬ permut_sym; constructor.
lets H0 : permut_mem_exists Hmwl´´; destruct H0 as (l3 & Hl3).
lets H1 : permut_mem_exists Hmw´l; destruct H1 as (l4 & Hl4).
assert (closed_proc_list_wfp (w´ :: l4)).
applys¬ (H l); inverts¬ Hc; rew_length; nat_math.
applys¬ (H (w :: l3)); try applys¬ permut_sym.
apply permut_len in Hl3; apply permut_len in Hl; rew_length in *; nat_math.
split; inverts¬ Hc.
applys¬ (H l4); inverts¬ H0.
apply permut_len in Hl4; apply permut_len in Hl; rew_length in *; nat_math.
rewrite (permut_cons_iff _ _ w´).
apply permut_trans with l; [applys¬ permut_sym |].
rewrite (permut_cons_iff _ _ w).
apply permut_trans with (w´ :: l´´); auto.
apply permut_flip_first_two; rewrites¬ <- permut_cons_iff.
Qed.
Lemma wfp_Msubst_invariant_permut : ∀ (xl xr : list var) (yl yr : list wfprocess) p,
length xl = length yl →
length xr = length yr →
(noDup xl) →
closed_proc_list_wfp yl →
permut (combine xl yl) (combine xr yr) →
wfp_multisubst (combine xl yl) p = wfp_multisubst (combine xr yr) p.
Proof.
induction xl using (measure_induction length); destruct xl; introv Hll Hrr Hd Hc Hp.
simpls; apply permut_sym in Hp; apply permut_of_nil in Hp;
rewrite Hp; simpls¬.
rename v into axl.
lets Hll´ : Hll; rew_length in Hll´; symmetry in Hll´; apply lengthn in Hll´; destruct Hll´ as (ayl & yl´ & Heq); subst; rename yl´ into yl.
assert (Hleq : length xr = length (axl :: xl)).
apply permut_len in Hp.
rewrite <- (length_combine xr yr Hrr); rewrites¬ <- (length_combine _ (ayl :: yl) Hll).
lets Hleq´ : Hleq; rew_length in Hleq´; apply lengthn in Hleq´; destruct Hleq´ as (axr & xr´ & Heq); subst; rename xr´ into xr.
lets Hrr´ : Hrr; rew_length in Hrr´; symmetry in Hrr´; apply lengthn in Hrr´; destruct Hrr´ as (ayr & yr´ & Heq); subst; rename yr´ into yr.
assert (Hpl : permut (axl :: xl) (axr :: xr)) by (apply permut_inv_l with (r := (ayl :: yl)) (s := (ayr :: yr)); auto).
assert (Hpr : permut (ayl :: yl) (ayr :: yr)) by (apply permut_inv_r with (l := (axl :: xl)) (t := (axr :: xr)); auto).
rename Hd into Hdl; assert (Hdr : noDup (axr :: xr)).
apply permut_nodup with (l := (axl :: xl)); auto.
rename Hc into Hcl; assert (Hcr : closed_proc_list_wfp (ayr :: yr)).
apply wfp_closed_proc_permut with (l := ayl :: yl); auto.
elim (classic (axl = axr)); introv Hneql; subst.
assert (ayl = ayr).
simpls; assert (Hml : Mem (axr, ayl) ((axr, ayl) :: combine xl yl)) by constructor.
lets Hpm : permut_mem; specialize (Hpm _ _ _ (axr, ayl) Hp Hml); clear Hml.
rewrite Mem_cons_eq in Hpm; inverts Hpm.
inverts¬ H0.
destruct Hdr as (Hdr & _); false Hdr.
eapply (mem_comb _ _ _ H0).
subst; simpls.
rewrite (H xl) with (xr := xr) (yr := yr); jauto.
rew_length; nat_math.
rewrite <- permut_cons_iff in Hp; auto.
assert (Hml : Mem (axl, ayl) (combine xr yr)).
simpls; apply permut_mem with (x := (axl, ayl)) in Hp.
rewrite Mem_cons_eq in Hp; inverts¬ Hp; try solve [inverts× H0]. constructor.
assert (Hmr : Mem (axr, ayr) (combine xl yl)).
simpls; apply permut_sym in Hp; apply permut_mem with (x := (axr, ayr)) in Hp.
rewrite Mem_cons_eq in Hp; inverts¬ Hp; try solve [inverts× H0]. constructor.
lets (yr´ & Hyr´) : (permut_mem_exists Hmr).
lets (yl´ & Hyl´) : (permut_mem_exists Hml).
lets (yr´l & yr´r & Hspec_yr´) : split_spec yr´.
assert (Hlr´ : length yr´l = length yr´r).
replace yr´l with (fst (split yr´)) by rewrites¬ <- Hspec_yr´;
replace yr´r with (snd (split yr´)) by rewrites¬ <- Hspec_yr´;
rewrite split_length_l; rewrites¬ split_length_r.
assert (((axr, ayr) :: yr´) = combine (axr :: yr´l) (ayr :: yr´r)).
simpl; replace yr´l with (fst (split yr´)) by rewrites¬ <- Hspec_yr´;
replace yr´r with (snd (split yr´)) by rewrites¬ <- Hspec_yr´;
rewrites¬ <- split_combine_fs.
rewrite H0 in *; clear yr´ Hspec_yr´ H0.
lets (yl´l & yl´r & Hspec_yl´) : split_spec yl´.
assert (Hll´ : length yl´l = length yl´r).
replace yl´l with (fst (split yl´)) by rewrites¬ <- Hspec_yl´;
replace yl´r with (snd (split yl´)) by rewrites¬ <- Hspec_yl´;
rewrite split_length_l; rewrites¬ split_length_r.
assert (((axl, ayl) :: yl´) = combine (axl :: yl´l) (ayl :: yl´r)).
simpl; replace yl´l with (fst (split yl´)) by rewrites¬ <- Hspec_yl´;
replace yl´r with (snd (split yl´)) by rewrites¬ <- Hspec_yl´;
rewrites¬ <- split_combine_fs.
rewrite H0 in *; clear yl´ Hspec_yl´ H0.
lets Hl1 : permut_len Hyr´; lets Hl2 : Hl1.
do 2 rewrites¬ length_combine in Hl1; try (rew_length; nat_math).
do 2 rewrites¬ length_combine in Hl2; try (rew_length; nat_math).
assert (Hpl´ : permut xl (axr :: yr´l)).
apply permut_inv_l with (r := yl) (s := (ayr :: yr´r)); auto; rew_length; nat_math.
assert (Hpr´ : permut yl (ayr :: yr´r)).
apply permut_inv_r with (l := xl) (t := (axr :: yr´l)); auto; rew_length; nat_math.
assert (Hpl´´ : permut xr (axl :: yl´l)).
apply permut_inv_l with (r := yr) (s := (ayl :: yl´r)); auto; rew_length; nat_math.
assert (Hpr´´ : permut yr (ayl :: yl´r)).
apply permut_inv_r with (l := xr) (t := (axl :: yl´l)); auto; rew_length; nat_math.
simpl.
rewrite (H xl) with (xr := (axr :: yr´l)) (yr := (ayr :: yr´r)); try rewrite (H xr) with (xr0 := (axl :: yl´l)) (yr := (ayl :: yl´r)); try (rew_length in *; nat_math); try solve [simpls; jauto].
simpl; rewrite wfp_subst_comm_cp; try solve [simpls; jauto].
rewrite (H yr´l) with (xr := yl´l) (yr := yl´r); simpls; jauto.
apply permut_len in Hpl´; rew_length in *; nat_math.
destruct Hdl as (_ & Hdl).
apply permut_nodup with (t := (axr :: yr´l)) in Hdl; simpls; jauto.
destruct Hcl as (_ & Hcl).
apply wfp_closed_proc_permut with (l´ := (ayr :: yr´r)) in Hcl; simpls; jauto.
rewrite (permut_cons_iff _ _ (axr, ayr)); rewrite (permut_cons_iff _ _ (axl, ayl)).
apply permut_flip_first_two.
apply permut_trans with (l2 := (axl, ayl) :: combine xl yl).
rewrites <- permut_cons_iff; applys¬ permut_sym.
apply permut_trans with (l2 := (axr, ayr) :: combine xr yr); auto.
Grab Existential Variables.
rew_length in *; nat_math.
Qed.