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.