Library HOC09GVLemmas
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC08SubstLemmas.
Lemma GV_swap: ∀ X Y p, GV p = \{} ↔ GV ({{[X,Y]}}p) = \{}.
Proof.
split; introv Hcp; induction p; simpls*; try applys¬ IHp.
apply singleton_absurd in Hcp. false.
apply union_empty in Hcp. destruct Hcp.
rewrite¬ IHp1. rewrite¬ IHp2. rewrite¬ union_empty_l.
apply singleton_absurd in Hcp. false.
apply union_empty in Hcp. destruct Hcp.
rewrite¬ IHp1. rewrite¬ IHp2. rewrite¬ union_empty_l.
Qed.
Lemma GV_swap_chan: ∀ (m n: chan) p, GV (|m,n|p) = GV p.
Proof.
induction p; introv; simpls¬.
rewrite IHp1. rewrite¬ IHp2.
Qed.
Lemma fresh_gvar_swap_chan : ∀ p m n X, X # p ↔ X # (|m, n|p).
Proof.
inductions p; introv; split; intros Hyp; unfolds fresh_gvar; simpls;
unfold notin in *; try rewrite in_union in *; rew_logic in *; auto;
repeat rewrite GV_swap_chan in *; auto.
Qed.
Lemma GV_subst_cp: ∀ p q X, closed_process q → GV ([q//X]p) = (GV p) \- \{X}.
Proof.
induction p; introv Hcp; simpls¬.
rewrite¬ remove_from_empty.
cases_if.
rewrite e. rewrite remove_same. apply Hcp.
simpl. rewrite¬ remove_while_notin.
rewrite¬ IHp1. rewrite¬ IHp2. rewrite¬ union_remove.
rewrite¬ remove_from_empty.
Qed.
Lemma wfp_GV_Msubst_cp: ∀ xs rs p, closed_proc_list_wfp rs → length xs = length rs →
GV ([combine xs rs]p) = (GV p) \- from_list xs.
Proof.
induction xs; introv Hcp Hls.
simpl. rewrite from_list_nil. rewrite¬ remove_empty.
lets Hls´: Hls. rewrite length_cons in Hls´.
symmetry in Hls´. apply lengthn in Hls´. destruct Hls´ as (Y & YS´ & HYS).
subst. simpls. rewrite× GV_subst_cp.
rewrite from_list_cons. rewrite union_comm. rewrite remove_union.
rewrite× IHxs.
Qed.
Lemma wfp_Msubst_subst_subset :
∀ (xs xs´ : list var) (ms ms´ : list chan) (p : wfprocess),
length xs = length ms → noDup xs →
length xs´ = length ms´ → noDup xs´ →
(∀ v w, v \in GV p → (Mem (v, w) (combine xs (¬¬ms)) ↔ Mem (v, w) (combine xs´ (¬¬ms´)))) →
wfp_multisubst (combine xs (¬¬ms)) p = wfp_multisubst (combine xs´ (¬¬ms´)) p.
Proof.
induction xs using (measure_induction length); destruct xs; introv Hlxs Hndxs Hlxs´ Hndxs´ Hsubset.
simpls; clear H Hndxs Hlxs ms.
generalize Hsubset; generalize Hndxs´; generalize Hlxs´; generalize ms´; clear.
induction xs´.
simpls¬.
introv Hlxs´ Hndxs´ Hsubset.
lets Hlxs´´ : Hlxs´; symmetry in Hlxs´´; apply lengthn in Hlxs´´; destruct Hlxs´´ as (w & ms´´ & Heq); subst; rename ms´´ into ms; simpls.
elim (classic (a \in GV p)); intro Hyp.
specialize (Hsubset a (wfp_Send w wfp_Nil) Hyp).
rewrite Mem_nil_eq in Hsubset; false; rewrite Hsubset; constructor.
rewrite wfp_gfresh_subst_rewrite.
applys× IHxs´.
introv Hin; specialize (Hsubset v w0 Hin); rewrite Mem_nil_eq in *; rewrite Hsubset.
split; intro Hm.
rewrite Mem_cons_eq in Hm; inverts¬ Hm.
inverts× H.
constructor¬.
unfold fresh_gvar.
rewrite wfp_GV_Msubst_cp; try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl.
unfold notin; rewrite in_remove; rew_logic; left; auto.
lets Hlxs´´ : Hlxs; symmetry in Hlxs´´; apply lengthn in Hlxs´´; destruct Hlxs´´ as (w & ms´´ & Heq); subst; rename ms´´ into ms; simpls.
elim (classic (v \in GV p)); intro Hyp.
assert (Mem (v, wfp_Send w wfp_Nil) (combine xs´ (¬¬ms´))).
rewrite¬ <- Hsubset; constructor¬.
destruct xs´.
simpls~; rewrite× Mem_nil_eq in H0.
lets Hlxs´´ : Hlxs´; symmetry in Hlxs´´; apply lengthn in Hlxs´´; destruct Hlxs´´ as (w0 & ms´´ & Heq); subst; rename ms´´ into ms´; simpls.
rewrite Mem_cons_eq in H0; inverts H0.
inverts H1.
rewrite (H xs) with (xs´ := xs´) (ms´ := ms´); jauto.
rew_length; nat_math.
introv Hing; specialize (Hsubset v w Hing).
elim (classic ((v, w) = (v0, wfp_Send w0 wfp_Nil))); introv Hneq; [inverts Hneq; subst | ].
split; introv Hin.
apply mem_comb in Hin; try rewrite¬ wfp_length_opl; false×.
apply mem_comb in Hin; try rewrite¬ wfp_length_opl; false×.
repeat rewrite× Mem_cons_eq in Hsubset.
elim (classic (v0 \in GV p)); introv Hin.
elim (classic (v = v0)); intro Hneq; subst.
assert (Heq : w = w0).
specialize (Hsubset v0 (wfp_Send w0 wfp_Nil) Hyp).
destruct Hsubset as (_ & Hs1).
assert (H2 : Mem (v0, wfp_Send w0 wfp_Nil) ((v0, wfp_Send w0 wfp_Nil) :: combine xs´ (¬¬ms´))) by constructor~; apply Hs1 in H2.
rewrite Mem_cons_eq in H2; inverts H2.
inverts¬ H0.
apply mem_comb in H0; try rewrite¬ wfp_length_opl; false×. subst; rewrite (H xs) with (xs´ := xs´) (ms´ := ms´); jauto.
rew_length; nat_math.
introv Hing; specialize (Hsubset v w Hing).
elim (classic ((v, w) = (v0, wfp_Send w0 wfp_Nil))); introv Hneq; [inverts Hneq; subst | ].
split; introv Hin´.
apply mem_comb in Hin´; try rewrite¬ wfp_length_opl; false×.
apply mem_comb in Hin´; try rewrite¬ wfp_length_opl; false×.
repeat rewrite× Mem_cons_eq in Hsubset.
assert (Hm : Mem (v, wfp_Send w wfp_Nil) (combine xs´ (¬¬ms´))).
specialize (Hsubset v (wfp_Send w wfp_Nil) Hyp).
destruct Hsubset as (Hs1 & _).
assert (Hm : Mem (v, wfp_Send w wfp_Nil) ((v, wfp_Send w wfp_Nil) :: combine xs (¬¬ms))) by constructor; apply Hs1 in Hm.
rewrite Mem_cons_eq in Hm; inverts¬ Hm.
apply permut_mem_exists in Hm; destruct Hm as (l´ & Hpl´).
rewrite split_combine_fs in Hpl´; rewrite fst_split_cons in Hpl´; rewrite snd_split_cons in Hpl´.
rewrite× (wfp_Msubst_invariant_permut xs´ (fst (v, wfp_Send w wfp_Nil) :: fst (split l´)) (¬¬ms´) (snd (v, wfp_Send w wfp_Nil) :: snd (split l´))); try (rewrite¬ wfp_length_opl); try apply wfp_cpl_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r).
assert (Hm´ : Mem (v0, wfp_Send w0 wfp_Nil) (combine xs (¬¬ms))).
specialize (Hsubset v0 (wfp_Send w0 wfp_Nil) Hin).
destruct Hsubset as (_ & Hs1).
assert (Hm´ : Mem (v0, wfp_Send w0 wfp_Nil) ((v0, wfp_Send w0 wfp_Nil) :: combine xs´ (¬¬ms´))) by constructor; apply Hs1 in Hm´.
rewrite Mem_cons_eq in Hm´; inverts¬ Hm´; inverts× H0.
apply permut_mem_exists in Hm´; destruct Hm´ as (l & Hpl).
rewrite split_combine_fs in Hpl; rewrite fst_split_cons in Hpl; rewrite snd_split_cons in Hpl.
rewrite× (wfp_Msubst_invariant_permut xs (fst (v0, wfp_Send w0 wfp_Nil) :: fst (split l)) (¬¬ms) (snd (v0, wfp_Send w0 wfp_Nil) :: snd (split l))); try (rewrite¬ wfp_length_opl); try apply wfp_cpl_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r).
simpl; rewrites¬ wfp_subst_comm_cp; try solve [unfold closed_process; simpls~].
lets Hps : Hpl; apply permut_inv_r in Hps; try rewrite¬ wfp_length_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r).
lets Heq´ : (wfp_permut_opl _ _ Hps); destruct Heq´ as (ns & Heq1 & Hpns).
assert (Hex : ∃ ns, snd (split l) = ¬¬ns).
destruct ns; simpls; inverts Heq1; ∃¬ ns.
destruct Hex as (ns´ & Heq); rewrite Heq in ×.
lets Hps´ : Hpl´; apply permut_inv_r in Hps´; try rewrite¬ wfp_length_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r).
lets Heq´ : (wfp_permut_opl _ _ Hps´); destruct Heq´ as (os & Heq´1 & Hpns´).
assert (Hex : ∃ os´, snd (split l´) = ¬¬os´).
destruct os; simpls; inverts Heq´1; ∃¬ os.
destruct Hex as (os´ & Heq´); rewrite Heq´ in *; simpls.
rewrite (H (fst (split l))) with (xs´ := fst (split l´)) (ms´ := os´); auto.
rewrite split_length_l.
assert (Haux : length l = length ns´) by (rewrite <- wfp_length_opl; rewrite <- Heq; rewrites¬ split_length_r); rewrite Haux; clear Haux.
assert (Haux : length (wfp_Send w0 wfp_Nil :: ¬¬ns´) = length (¬¬ns)) by rewrite¬ Heq1; rew_length in Haux; repeat rewrite wfp_length_opl in Haux.
apply permut_len in Hpns; rew_length in *; nat_math.
rewrite split_length_l.
rewrite <- wfp_length_opl; rewrite <- Heq; rewrites¬ split_length_r.
replace ((v0, wfp_Send w0 wfp_Nil) :: combine (fst (split l)) (¬¬ns´)) with (combine (v0 :: fst (split l)) (wfp_Send w0 wfp_Nil :: (¬¬ns´))) in Hpl by auto.
apply permut_inv_l in Hpl; try rewrite¬ wfp_length_opl.
apply permut_nodup in Hpl; simpl in Hpl; jauto.
rew_length; rewrite <- Heq; rewrite split_length_l; rewrite¬ split_length_r.
rewrite split_length_l.
rewrite <- wfp_length_opl; rewrite <- Heq´; rewrites¬ split_length_r.
replace ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´)) with (combine (v :: fst (split l´)) (wfp_Send w wfp_Nil :: (¬¬os´))) in Hpl´ by auto.
apply permut_inv_l in Hpl´; try rewrite¬ wfp_length_opl.
apply permut_nodup in Hpl´; simpl in Hpl´; jauto.
rew_length; rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r.
introv Hinv1; specialize (Hsubset v1 w1 Hinv1); split; introv Hmem.
assert (Hnv1v : v1 ≠ v).
introv Hypeq; subst.
assert (Mem (v, w1) ((v0, wfp_Send w0 wfp_Nil) :: combine (fst (split l)) (¬¬ns´))) by constructor¬.
apply permut_sym in Hpl; apply (permut_mem Hpl) in H0.
apply mem_comb in H0; try rewrite¬ wfp_length_opl; jauto.
assert (Hnv1v0 : v1 ≠ v0).
introv Hypeq; subst.
replace ((v0, wfp_Send w0 wfp_Nil) :: combine (fst (split l)) (¬¬ns´)) with (combine (v0 :: fst (split l)) (wfp_Send w0 wfp_Nil :: (¬¬ns´))) in Hpl by auto.
apply permut_inv_l in Hpl; try rewrite¬ wfp_length_opl; try (rew_length; rewrite <- Heq; rewrite split_length_l; rewrite¬ split_length_r).
assert (noDup (v0 :: fst (split l))) by (apply permut_nodup with (l := xs); jauto).
simpl in H0; apply mem_comb in Hmem; jauto.
rewrite <- Heq; rewrite split_length_l; rewrite¬ split_length_r.
assert (Hmv1 : Mem (v1, w1) ((v0, wfp_Send w0 wfp_Nil) :: combine xs´ (¬¬ms´))).
rewrite <- Hsubset; constructor.
apply permut_sym in Hpl; apply (permut_mem Hpl); constructor¬.
rewrite Mem_cons_eq in Hmv1; inverts Hmv1.
inverts× H0.
apply (permut_mem Hpl´) in H0.
rewrite Mem_cons_eq in H0; inverts¬ H0.
inverts× H2.
assert (Hnv1v0 : v1 ≠ v0).
introv Hypeq; subst.
assert (Mem (v0, w1) ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´))) by constructor¬.
apply permut_sym in Hpl´; apply (permut_mem Hpl´) in H0.
apply mem_comb in H0; try rewrite¬ wfp_length_opl; jauto.
assert (Hnv1v : v1 ≠ v).
intro Hypeq; subst.
replace ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´)) with (combine (v :: fst (split l´)) (wfp_Send w wfp_Nil :: (¬¬os´))) in Hpl´ by auto.
apply permut_inv_l in Hpl´; try rewrite¬ wfp_length_opl; try (rew_length; rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r).
assert (noDup (v :: fst (split l´))) by (apply permut_nodup with (l := xs´); jauto).
simpl in H0; apply mem_comb in Hmem; jauto.
rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r.
assert (Hmv1 : Mem (v1, w1) ((v, wfp_Send w wfp_Nil) :: combine xs (¬¬ms))).
rewrite Hsubset; constructor.
apply permut_sym in Hpl´; apply (permut_mem Hpl´); constructor¬.
rewrite Mem_cons_eq in Hmv1; inverts Hmv1.
inverts× H0.
apply (permut_mem Hpl) in H0.
rewrite Mem_cons_eq in H0; inverts¬ H0.
inverts× H2.
assert (Hneq : v ≠ v0) by (intro Heq; substs*).
rewrites¬ (wfp_gfresh_subst_rewrite v0).
assert (Hm : Mem (v, wfp_Send w wfp_Nil) (combine xs´ (¬¬ms´))).
specialize (Hsubset v (wfp_Send w wfp_Nil) Hyp).
destruct Hsubset as (Hs1 & _).
assert (Hm : Mem (v, wfp_Send w wfp_Nil) ((v, wfp_Send w wfp_Nil) :: combine xs (¬¬ms))) by constructor; apply Hs1 in Hm.
rewrite Mem_cons_eq in Hm; inverts¬ Hm.
apply permut_mem_exists in Hm; destruct Hm as (l´ & Hpl´).
rewrite split_combine_fs in Hpl´; rewrite fst_split_cons in Hpl´; rewrite snd_split_cons in Hpl´.
rewrite× (wfp_Msubst_invariant_permut xs´ (fst (v, wfp_Send w wfp_Nil) :: fst (split l´)) (¬¬ms´) (snd (v, wfp_Send w wfp_Nil) :: snd (split l´))); try (rewrite¬ wfp_length_opl); try apply wfp_cpl_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r); simpl.
lets Hps´ : Hpl´; apply permut_inv_r in Hps´; try rewrite¬ wfp_length_opl; try (rew_length; rewrite split_length_l; rewrites¬ split_length_r).
lets Heq´ : (wfp_permut_opl _ _ Hps´); destruct Heq´ as (os & Heq´1 & Hpns´).
assert (Hex : ∃ os´, snd (split l´) = ¬¬os´).
destruct os; simpls; inverts Heq´1; ∃¬ os.
destruct Hex as (os´ & Heq´); rewrite Heq´ in *; simpls.
rewrite (H xs) with (xs´ := fst (split l´)) (ms´ := os´); jauto.
rew_length; nat_math.
rewrite split_length_l.
rewrite <- wfp_length_opl; rewrite <- Heq´; rewrites¬ split_length_r.
replace ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´)) with (combine (v :: fst (split l´)) (wfp_Send w wfp_Nil :: (¬¬os´))) in Hpl´ by auto.
apply permut_inv_l in Hpl´; try rewrite¬ wfp_length_opl.
apply permut_nodup in Hpl´; simpl in Hpl´; jauto.
rew_length; rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r.
introv Hinv1; specialize (Hsubset v1 w1 Hinv1); split; introv Hmem.
assert (Hnv1v : v1 ≠ v).
intro Hypeq; subst.
replace ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´)) with (combine (v :: fst (split l´)) (wfp_Send w wfp_Nil :: (¬¬os´))) in Hpl´ by auto.
apply permut_inv_l in Hpl´; try rewrite¬ wfp_length_opl; try (rew_length; rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r).
assert (noDup (v :: fst (split l´))) by (apply permut_nodup with (l := xs´); jauto).
simpl in H0; apply mem_comb in Hmem; try rewrite¬ wfp_length_opl; jauto.
assert (Hmv1 : Mem (v1, w1) ((v0, wfp_Send w0 wfp_Nil) :: combine xs´ (¬¬ms´))).
rewrite <- Hsubset; constructor¬.
rewrite Mem_cons_eq in Hmv1; inverts Hmv1.
inverts× H0.
apply (permut_mem Hpl´) in H0; auto.
rewrite Mem_cons_eq in H0; inverts¬ H0.
inverts× H2.
assert (Hnv1v0 : v1 ≠ v0).
introv Hypeq; subst.
assert (Hmv1 : Mem (v0, w1) ((v, wfp_Send w wfp_Nil) :: combine xs´ (¬¬ms´))).
constructor; apply permut_sym in Hpl´; apply (permut_mem Hpl´); constructor¬.
rewrite Mem_cons_eq in Hmv1; inverts¬ Hmv1.
assert (Hnv1v : v1 ≠ v).
introv Hypeq; subst.
replace ((v, wfp_Send w wfp_Nil) :: combine (fst (split l´)) (¬¬os´)) with (combine (v :: fst (split l´)) (wfp_Send w wfp_Nil :: (¬¬os´))) in Hpl´ by auto.
apply permut_inv_l in Hpl´; try rewrite¬ wfp_length_opl; try (rew_length; rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r).
assert (noDup (v :: fst (split l´))) by (apply permut_nodup with (l := xs´); jauto).
simpl in H0; apply mem_comb in Hmem; jauto.
rewrite <- Heq´; rewrite split_length_l; rewrite¬ split_length_r.
cut (Mem (v1, w1) ((v, wfp_Send w wfp_Nil) :: combine xs (¬¬ms))).
intro Hm; rewrite Mem_cons_eq in Hm; inverts¬ Hm.
inverts× H0.
rewrite Hsubset; constructor.
apply permut_sym in Hpl´; apply (permut_mem Hpl´); constructor¬. unfold fresh_gvar; rewrite wfp_GV_Msubst_cp; try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl.
unfold notin; rewrite in_remove; rew_logic; left; auto.
rewrite wfp_gfresh_subst_rewrite.
applys× H.
rew_length; nat_math.
introv Hin; specialize (Hsubset v0 w0 Hin); rewrite <- Hsubset.
split; intro Hm.
constructor¬.
rewrite Mem_cons_eq in Hm; inverts¬ Hm.
inverts× H0.
unfold fresh_gvar.
rewrite wfp_GV_Msubst_cp; try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl.
unfold notin; rewrite in_remove; rew_logic; left; auto.
Qed.
Lemma GV_trans_in_const:
∀ (a : chan) p (fp : abstraction),
{{p -- LabIn a ->> (AA fp)}} → const_abs fp →
∀ (q : wfprocess), GV (wfp_inst_Abs fp q) = GV p.
Proof.
introv Ht Hc. inductions Ht; introv.
simpl. inverts Hc. do 2 rewrite¬ gfresh_subst_rewrite.
destruct ap; inverts x. inverts Hc. simpl. rewrite¬ IHHt.
destruct aq; inverts x. inverts Hc. simpl. rewrite¬ IHHt.
Qed.
Lemma GV_trans_in:
∀ (a : chan) p (fp : abstraction),
{{p -- LabIn a ->> (AA fp)}} → ¬const_abs fp →
∀ (q : wfprocess), GV (wfp_inst_Abs fp q) = GV p \u GV q.
Proof.
introv Ht Hc. inductions Ht; introv.
simpl. rewrite (GV_subst_cp _ (Lvar (f X p))). apply GV_subst.
introv Hf; apply Hc; constructor¬.
unfold closed_process; simpls¬.
destruct ap; inverts x. simpl. rewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
destruct aq; inverts x. simpl. rewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
Qed.
Lemma GV_trans_in_sub: ∀ a p fp,
{{p--LabIn a->>(AA fp)}} → ∀ q, GV p \c GV (wfp_inst_Abs fp q).
Proof.
introv Ht. destruct (const_abs_decidable fp) as (b&dec).
destruct b; rewrite isTrue_def in dec; cases_if; clear dec; introv.
lets Hgv: (GV_trans_in_const a p fp Ht H q). rewrite Hgv. apply subset_refl.
lets Hgv: (GV_trans_in a p fp Ht H q). rewrite Hgv. apply subset_union_weak_l.
Qed.
Lemma GV_trans_out: ∀ a p p´ p´´,
{{p--LabOut a p´´->>AP p´}} → GV p = GV p´ \u GV p´´.
Proof.
introv Ht; inductions Ht; simpls.
rewrite¬ union_empty_l.
destruct ap; inverts x. simpls. erewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
destruct aq; inverts x. simpls. erewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
Qed.
Lemma GV_trans_rem1: ∀ (X : var) p p´,
{{p--LabRem X->>AP p´}} → X \in GV p.
Proof.
introv Ht; inductions Ht; simpls.
rewrite¬ in_singleton.
destruct ap; inverts x. simpl. rewrite in_union. left×.
destruct aq; inverts x. simpl. rewrite in_union. right×.
Qed.
Lemma GV_trans_rem2: ∀ X p p´, {{p--LabRem X->>AP p´}} → GV p = GV p´ \u \{X}.
Proof.
introv Ht; inductions Ht; simpls.
rewrite¬ union_empty_l.
destruct ap; inverts x. simpl. erewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
destruct aq; inverts x. simpl. erewrite¬ IHHt.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite¬ union_comm.
Qed.
Lemma GV_trans_tau: ∀ p p´, {{p--Tau->>AP p´}} → GV p´ \c GV p.
Proof.
introv Ht; inductions Ht; simpls.
destruct ap; inverts x. simpls. applys¬ subset_union_2. apply subset_refl.
destruct aq; inverts x. simpls. applys¬ subset_union_2. apply subset_refl.
apply GV_trans_out in Ht1.
destruct (const_abs_decidable fq) as (b & dec). destruct b; rewrite isTrue_def in dec; cases_if; clear dec.
rewrite¬ (GV_trans_in_const a q). rewrite Ht1.
apply subset_union_2. apply subset_union_weak_l. apply subset_refl.
rewrite¬ (GV_trans_in a q). rewrite Ht1.
rewrite union_comm_assoc. rewrite union_comm. apply subset_refl.
apply GV_trans_out in Ht2.
destruct (const_abs_decidable fp) as (b & dec). destruct b; rewrite isTrue_def in dec; cases_if; clear dec.
rewrite¬ (GV_trans_in_const a p). rewrite Ht2.
apply subset_union_2. apply subset_refl. apply subset_union_weak_l.
rewrite¬ (GV_trans_in a p). rewrite Ht2.
rewrite union_comm_assoc. rewrite union_comm. apply subset_refl.
Qed.
Lemma cp_par: ∀ p q, closed_process (Par p q) ↔ closed_process p ∧ closed_process q.
Proof.
split; introv Hcp; unfolds closed_process; simpls.
apply union_empty in Hcp. assumption.
destruct Hcp. rewrite H, H0. rewrite¬ union_empty_l.
Qed.
Lemma cp_abs: ∀ f a X p, closed_process p → closed_process (Abs f a X p).
Proof.
introv Hcp; unfolds closed_process; simpls. rewrite GV_subst_cp.
rewrite Hcp. rewrite¬ remove_from_empty.
unfolds¬.
Qed.
Lemma cp_trans_in: ∀ a (p : wfprocess) fp, closed_process p →
{{p--LabIn a->>(AA fp)}} → ∀ (q : wfprocess), closed_process q → closed_process (wfp_inst_Abs fp q).
Proof.
introv Hcpp Ht Hcpq. destruct (const_abs_decidable fp) as (b & dec). destruct b.
rewrite isTrue_def in dec. cases_if. clear dec.
unfolds closed_process. rewrite <- Hcpp. applys× GV_trans_in_const.
rewrite isTrue_def in dec. cases_if. clear dec.
unfolds closed_process. rewrite <- Hcpp. rewrite <- union_empty_r.
rewrite <- Hcpq. applys× GV_trans_in.
Qed.
Lemma cp_trans_out: ∀ a (p p´ : wfprocess) p´´, closed_process p →
{{p--LabOut a p´´->>AP p´}} → closed_process p´ ∧ closed_process p´´.
Proof.
introv Hcp Ht. unfolds closed_process. apply union_empty.
rewrite <- Hcp. symmetry. applys× GV_trans_out.
Qed.
Lemma cp_trans_tau: ∀ (p : wfprocess) p´, closed_process p →
{{p--Tau->>AP p´}} → closed_process p´.
Proof.
introv Hcp Ht. unfolds closed_process.
apply GV_trans_tau in Ht. rewrite Hcp in Ht. apply subset_of_empty in Ht.
assumption.
Qed.
Lemma wfp_GV_Abs : ∀ a X p, GV (wfp_Abs a X p) = GV p \- \{X}.
Proof.
introv; simpls.
tests : (X # p).
rewrite¬ gfresh_subst_rewrite.
unfold fresh_gvar in C.
rewrite¬ remove_while_notin.
rewrite¬ GV_subst; simpls; rewrite¬ union_empty_r.
Qed.
Lemma wfp_GV_pipe_ch: ∀ a b xs p, GV (wfp_pipe a xs p) = GV (wfp_pipe b xs p).
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. induction xs...
repeat rewrite wfp_GV_Abs. rewrite¬ IHxs.
Qed.
Lemma wfp_GV_pipe_send: ∀ a c xs p, GV (wfp_pipe a xs p) = GV (wfp_pipe a xs (wfp_Send c p)).
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. induction xs...
repeat rewrite wfp_GV_Abs. rewrite¬ IHxs.
Qed.
Lemma wfp_GV_pipe_abs1: ∀ a b xs X p, ¬Mem X xs → GV (wfp_pipe a xs p) \- \{X} = GV (wfp_pipe b xs (wfp_Abs a X p)).
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. inductions xs; introv Hnm...
rewrite¬ wfp_GV_Abs.
rewrite Mem_cons_eq in Hnm; rew_logic in Hnm.
repeat rewrite wfp_GV_Abs.
rewrite× <- IHxs.
repeat rewrite <- remove_union. rewrite¬ union_comm.
Qed.
Lemma wfp_GV_pipe_abs2: ∀ a b xs X p, Mem X xs → GV (wfp_pipe a xs p) = GV (wfp_pipe a xs (wfp_Abs b X p)).
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. inductions xs; introv Hnm...
rewrite× Mem_nil_eq in Hnm.
repeat rewrite wfp_GV_Abs.
tests : (Mem X xs).
rewrite¬ <- IHxs.
rewrite¬ <- wfp_GV_pipe_abs1.
inverts× Hnm.
assert (Hn : a0 \notin (GV (wfp_pipe b xs p) \- \{a0})).
unfold notin; rewrite in_remove; rew_logic; right.
rewrite× notin_singleton.
rewrite¬ (remove_while_notin Hn).
rewrite wfp_GV_pipe_ch with (b := b); auto.
Qed.
Lemma wfp_GV_pipe_gvar1: ∀ a X xs, ¬Mem X xs → GV (wfp_pipe a xs (wfp_Gvar X)) = \{X}.
Proof with (rewrite_wfp_pipe_multi; jauto).
introv Hnm; induction xs...
rewrite Mem_cons_eq in Hnm; rew_logic in Hnm.
rewrite wfp_GV_Abs. rewrite× IHxs.
apply remove_while_notin. rewrite× notin_singleton.
Qed.
Lemma wfp_GV_pipe_gvar2: ∀ a X xs,
Mem X xs → GV (wfp_pipe a xs (wfp_Gvar X)) = \{}.
Proof with (rewrite_wfp_pipe_multi; jauto).
introv Hnm. induction xs; try rename a0 into Y...
rewrite× Mem_nil_eq in Hnm.
rewrite Mem_cons_eq in Hnm; inverts× Hnm.
rewrite wfp_GV_Abs.
tests : (Mem Y xs).
rewrite¬ IHxs; rewrite¬ remove_while_notin.
rewrite¬ wfp_GV_pipe_gvar1.
rewrite¬ remove_same.
rewrite wfp_GV_Abs. rewrite× IHxs.
rewrite¬ remove_while_notin.
Qed.
Lemma wfp_GV_pipe_par: ∀ a xs p1 p2,
GV (wfp_pipe a xs (wfp_Par p1 p2)) = GV (wfp_pipe a xs p1) \u GV (wfp_pipe a xs p2).
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. induction xs...
repeat rewrite wfp_GV_Abs. rewrite¬ IHxs.
rewrite¬ <- remove_union_distr.
Qed.
Lemma wfp_GV_pipe_nil: ∀ a xs, GV (wfp_pipe a xs wfp_Nil) = \{}.
Proof with (rewrite_wfp_pipe_multi; jauto).
introv. inductions xs...
rewrite wfp_GV_Abs. rewrite IHxs.
apply remove_from_empty.
Qed.
Lemma wfp_closed_pipe: ∀ (p : wfprocess) a xs,
(GV p) \c from_list xs → closed_process (wfp_pipe a xs p).
Proof with (rewrite_wfp_pipe_multi; jauto).
induction p using wfp_ind; introv H; unfold closed_process in ×...
rewrite <- wfp_GV_pipe_send. apply¬ IHp.
tests : (Mem X xs).
rewrite¬ <- wfp_GV_pipe_abs2.
applys× IHp.
unfolds subset. introv Hyp; specializes H x; rewrite from_list_spec in ×.
tests¬ : (x = X).
apply H. rewrite wfp_GV_Abs; rewrite in_remove; splits¬.
rewrite¬ <- wfp_GV_pipe_abs1.
tests : (X # p); unfold fresh_gvar in *; rewrite wfp_GV_Abs in H.
rewrite¬ remove_while_notin in H.
rewrite¬ IHp. apply¬ remove_while_notin.
unfold notin in *; apply not_not_elim in C0.
specializes IHp a (X :: xs)...
rewrite wfp_GV_Abs in IHp. apply IHp.
unfolds subset; introv Hyp; specializes H x; rewrite from_list_spec in ×.
tests : (X = x); constructor.
apply H; rewrite¬ in_remove.
apply¬ wfp_GV_pipe_gvar2. unfolds subset. rewrite <- from_list_spec. apply H. simpl; rewrite¬ in_singleton.
rewrite wfp_GV_pipe_par. rewrite IHp1, IHp2.
rewrite¬ union_empty_l.
simpls; rewrite union_comm in H. applys× union_subset.
simpls; applys× union_subset.
apply wfp_GV_pipe_nil.
Qed.