Library HOC06FreshLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.


Lemma wfp_gfresh_Abs : ∀ a X Y p, X # (wfp_Abs a Y p) = (X = Y ∨ X # p).
Proof with (try solve [fresh_solve]; jauto).
  introv; simpl; unfold Abs.
  rewrite gfresh_receive.
  tests : (X = Y); rew_logic; splits; intro Hyp...
Qed.



Lemma wfp_cfresh_par_iff : ∀ m p q,
  m ### wfp_Par p q = (m ### p ∧ m ### q).
Proof.
  introv; simpl; rewrite× cfresh_par_iff.
Qed.

Lemma wfp_cfresh_Abs : ∀ a m X p,
  m ### (wfp_Abs a X p) = (m ### p ∧ a ≠ m).
Proof.
  introv; simpl; unfold Abs; simpl.
  rewrite cfresh_receive.

  assert (∀ x X p, CHS ([Lvar x//X]p) = (CHS p)).
    clear; induction p; introv; simpls~; try rewrite¬ IHp.
    cases_if¬.
    rewrite IHp1, IHp2; auto.

  unfolds fresh_chan; rewrite H; tauto.
Qed.

Lemma wfp_cfresh_pipe : ∀ a m xs (p : wfprocess),
  m ### p ∧ a ≠ m → m ### (wfp_pipe a xs p).
Proof.
  induction xs; introv H.
    simpls×.
    rewrite wfp_pipe_to_Abs. rewrite wfp_cfresh_Abs; split×.
Qed.

Lemma wfp_cfresh_pipe_cons : ∀ xs a m x p,
  m ### (wfp_pipe a (x :: xs) p) → m###p ∧ a≠m.
Proof with
  (try rewrite wfp_pipe_to_Abs in *;
   try rewrite wfp_pipe_nil_eq in *;
   try rewrite wfp_cfresh_Abs in *; jauto).

  induction xs; introv Hf; simpl...
    applys× IHxs.
Qed.


Lemma wfp_cfresh_swap_inv : ∀ (p : wfprocess) m X Y, m ### p = m ### wfp_swap X Y p.
Proof.
  inductions p; simpl; rename proc into p; clear wf_cond.
  inductions p; introv; unfolds fresh_chan; simpls;
  unfold notin in *; repeat (rewrite in_union in *; rew_logic in × );
   try solve [rewrites¬ <- IHp; try reflexivity; intuition]; auto.
   rewrites¬ <- IHp1; rewrites¬ <- IHp2. tauto.
Qed.

Lemma wfp_cfresh_subst_in : ∀ m Y (p q : wfprocess),
  m ### p → m ### q → m ### (wfp_subst q Y p).
Proof with freshen_up.
  induction p using wfp_ind_gen; introv Hf1 Hf2;
    try solve [simpls; try cases_if~; freshen_up].
  rewrite wfp_cfresh_Abs in Hf1; destruct Hf1 as (Hf1 & Hneq).
  tests : (X = Y).
    rewrite wfp_eq_subst_abs1. rewrite× wfp_cfresh_Abs.
    lets (Z & Hfz) : find_fresh (Gvar Y :: proc p :: proc q :: nil).
    rewrite Forall_to_conj_3 in Hfz. rewrite gfresh_gvar in Hfz.
    rewrite wfp_eq_subst_abs3 with (Z := Z); jauto.
    rewrite wfp_cfresh_Abs; splits×. applys× H.
      rewrite× wfp_gfresh_subst_is_swap.
      rewrite¬ <- wfp_cfresh_swap_inv.
Qed.

Lemma wfp_cfresh_subst_from1 : ∀ m X p q,
  m ### wfp_subst q X p → m ### p.
Proof with freshen_up.
  inductions p; simpl; rename proc into p; clear wf_cond.
  induction p; simpls~; introv H...
Qed.

Lemma wfp_cfresh_msubst_from : ∀ m xs p rs,
  length rs = length xs → m ### wfp_multisubst (combine xs rs) p → m ### p.
Proof.
  induction xs.
    simpls¬.
    introv Hl; lets Hl´ : Hl; rew_length in Hl; apply lengthn in Hl.
    destruct Hl as (y & ys & Hys); subst; rew_length in Hl´.
    introv Hf; simpl wfp_multisubst in Hf; apply wfp_cfresh_subst_from1 in Hf; jauto.
Qed.

Lemma wfp_cfresh_subst_from2 : ∀ (p : wfprocess) m X q, X \in GV p →
  m ### (wfp_subst q X p) → m ### q.
Proof with freshen_up.
  induction p using wfp_ind_gen; introv Hgv Hfr; rewrite_wfp_subst; simpl in Hgv.
    eapply IHp. apply Hgv. simpls...

    tests : (X # p).
      rewrite¬ gfresh_subst_rewrite in Hgv.
      tests : (X = X0).
        lets (Z & Hfz) : find_fresh (Gvar X0 :: proc p :: proc q :: nil).
        rewrite Forall_to_conj_3 in Hfz. rewrite gfresh_gvar in Hfz.
        rewrite wfp_eq_subst_abs3 with (Z := Z) in Hfr; jauto.
        rewrite wfp_cfresh_Abs in Hfr. inverts Hfr.
        apply H in H0; jauto.
        rewrite¬ wfp_gfresh_subst_rewrite.
      rewrite¬ GV_subst in Hgv; simpl in Hgv. rewrite union_empty_r in Hgv.
      rewrite in_remove in Hgv; inverts Hgv as (Hgv & Hneq).
        lets (Z & Hfz) : find_fresh (Gvar X0 :: proc p :: proc q :: nil).
        rewrite Forall_to_conj_3 in Hfz. rewrite gfresh_gvar in Hfz.
        rewrite wfp_eq_subst_abs3 with (Z := Z) in Hfr; jauto.
        rewrite wfp_cfresh_Abs in Hfr. inverts Hfr.
        apply H in H0; jauto.
        simpl; rewrite¬ GV_subst; rewrite in_union; left.
        rewrite× in_remove.
        rewrite¬ notin_singleton in H2.

    rewrite in_singleton in Hgv. cases_if¬.
    rewrite in_union in Hgv; inverts Hgv; [eapply IHp1 | eapply IHp2];
      try apply H; simpls; rewrite× cfresh_par_iff in Hfr.
    rewrite in_empty in Hgv. false.
Qed.


Lemma wfp_fresh_cp : ∀ (r : wfprocess), closed_process r → ∀ X:var, X#r.
Proof.
  introv H. introv. unfolds in H. applys¬ fresh_GV.
Qed.

Lemma wfp_fresh_Msubst : ∀ xs rs X (p : wfprocess),
  X#p → length xs = length rs → closed_proc_list_wfp rs → X # (wfp_multisubst (combine xs rs) p).
Proof.
  induction xs; introv Hf Hls Hcp.
    simpls¬.
    rewrite length_cons in Hls. symmetry in Hls. lets (y & ys & H): (lengthn rs Hls).
    subst. simpls. apply gfresh_in_subst_p_q. applys× IHxs.
      rewrite length_cons in Hls. nat_math.
    unfolds. destruct Hcp. unfolds in H. rewrite H. apply notin_empty.
Qed.

Lemma wfp_fresh_chan_cswap : ∀ (p : wfprocess) m n a,
  a ### p → ({{|m,n|}}a) ### wfp_swap_chan m n p.
Proof with freshen_up.
  induction p; simpl; rename proc into p; clear wf_cond.
  induction p; simpl; intros...
    rewrite cfresh_send in ×. split×.
      unfolds swap_name; repeat cases_if~; substs×.
    rewrite cfresh_receive in ×. split×.
      unfolds swap_name; repeat cases_if~; substs×.
Qed.

Lemma wfp_fresh_chan_gswap: ∀ (p : wfprocess) m X Y, m ### p → m ### wfp_swap X Y p.
Proof with freshen_up.
  induction p; simpl; rename proc into p; clear wf_cond.
  induction p; introv Hf; simpls¬...
Qed.

Lemma wfp_fresh_gvar_cswap: ∀ (p : wfprocess) m n X, X # p → X # wfp_swap_chan m n p.
Proof.
  induction p; simpl; rename proc into p; clear wf_cond.
  induction p; introv Hf; simpls~; unfolds fresh_gvar; simpls¬.
Qed.

Lemma wfp_fresh_inst_Abs : ∀ p fp a X Y, {{p -- LabIn a ->> AA fp}} → X # p → X ≠ Y → X # wfp_inst_Abs fp (wfp_Gvar Y).
Proof with freshen_up.
  introv Ht; inductions Ht; simpls; intros...
  tests : (X = X0).
    fresh_solve.
    unfold Abs in H; rewrite gfresh_receive in H.
    apply¬ gfresh_in_subst_p_q... fresh_solve.
  destruct ap; inverts x; simpl; rewrite gfresh_par_iff in *; splits×.
  destruct aq; inverts x; simpl; rewrite gfresh_par_iff in *; splits×.
Qed.


Lemma wfp_cfresh_in: ∀ a m (p : wfprocess) f,
  m ### p → {{p--LabIn a->>(AA f)}} → ∀ (q : wfprocess), m###q → m ### (wfp_inst_Abs f q).
Proof with freshen_up.
  introv Hfm Ht; gen m. inductions Ht; introv Hf1 Hf2.
    rewrite wfp_cfresh_Abs in Hf1. destruct Hf1. simpl wfp_inst_Abs; apply¬ wfp_cfresh_subst_in.
    destruct ap; inverts x. simpls...
    destruct aq; inverts x. simpls...
Qed.

Lemma wfp_cfresh_out: ∀ (a m : chan) (p : wfprocess) p´ p´´,
  m###p → {{p -- LabOut a p´´ ->> (AP p´)}} →
    a ≠ m ∧ m ### p´ ∧ m ### p´´.
Proof with freshen_up.
  introv Hf Ht; gen m; inductions Ht; introv Hf.
    simpls; splits...
    destruct ap; inverts x...
    simpls; rewrite cfresh_par_iff in ×. rewrite and_assoc.
      splits*; try eapply IHHt; jauto.
    destruct aq; inverts x...
    simpls; rewrite cfresh_par_iff in ×. rewrite and_assoc.
      splits*; try eapply IHHt; jauto.
Qed.

Lemma wfp_cfresh_rem: ∀ a X (p : wfprocess) p´, a###p → {{p--LabRem X->>(AP p´)}} → a###p´.
Proof with freshen_up.
  introv Hf Ht; gen a; introv Hf; inductions Ht; simpls...
    destruct ap; inverts x; simpls...
    destruct aq; inverts x; simpls...
Qed.

Lemma wfp_cfresh_tau: ∀ m (p : wfprocess) p´, m###p → {{p--Tau->>(AP p´)}} → m###p´.
Proof with freshen_up.
  introv Hf Ht; gen m; inductions Ht; introv Hf; simpls...
    destruct ap; inverts x; simpl...
    destruct aq; inverts x; simpl...
    clear IHHt1 IHHt2.
    rename p´0 into p´.
    rewrite cfresh_par_iff in *; split.
      apply wfp_cfresh_out with (m := m) in Ht1; intuition.
      eapply wfp_cfresh_in; try eassumption; jauto.
      eapply wfp_cfresh_out; try eassumption; jauto.
    clear IHHt1 IHHt2.
    rewrite cfresh_par_iff in *; split.
      apply wfp_cfresh_out with (m := m) in Ht2; intuition.
      apply wfp_cfresh_in with (m := m) (q := q´´) in Ht1; auto.
      apply wfp_cfresh_out with (m := m) in Ht2; jauto.
Qed.

Lemma wfp_cfresh_Msubst1 : ∀ (XS : list var) m ms (p : wfprocess),
  m###p → length XS = length ms → Forall (≠ m) ms →
  m###(wfp_multisubst (combine XS (¬¬ms)) p).
Proof.
  induction XS; introv Hf Hls Hd.
    simpls¬.
    lets Hls´: Hls.
    rewrite length_cons in Hls. symmetry in Hls. apply lengthn in Hls.
    destruct Hls as (m´ & ms´ & Hys). subst. inverts Hd.
    simpl wfp_multisubst; applys¬ wfp_cfresh_subst_in.
    unfolds. simpls. rewrite notin_union. split¬. rewrite¬ notin_singleton.
Qed.


Lemma wfp_cfresh_out_inv : ∀ (a :chan) p p´ p´´,
  {{p -- LabOut a p´´ ->> AP p´}} → ¬ a ### p.
Proof with (freshen_up; try solve_wfp_size).
  induction p using (measure_induction wfp_size).
  introv Ht; inverts Ht; simpls.
    unfolds fresh_chan; simpl.
    unfold notin; rewrite in_union; rewrite¬ in_singleton.

    rewrite cfresh_par_iff; rew_logic; left.
    destruct ap; inverts H0; simpl...
    eapply H... eassumption.

    rewrite cfresh_par_iff; rew_logic; right.
    destruct aq; inverts H0; simpl...
    eapply H... eassumption.
Qed.