Library HOC02BaseLemmas

Require Import HOC01Defs.


Fixpoint E (X:var) (p:process) :=
  match p with
    | Send _ p ⇒ (E X p)
    | Receive _ x p ⇒ ifb (X#p)
                         then \{}
                         else (\{x} \u (E X p))
    | Lvar _ ⇒ \{}
    | Gvar _ ⇒ \{}
    | Par p q ⇒ (E X p) \u (E X q)
    | Nil ⇒ \{}
  end.



Lemma fresh_GV : ∀ p X, GV p = \{} → X#p.
Proof.
  unfolds fresh_gvar. introv H. rewrites¬ H.
Qed.

Lemma gfresh_send : ∀ a X p, X # (Send a p) = X # p.
Proof.
  auto.
Qed.

Lemma gfresh_receive : ∀ a x X p, X # (Receive a x p) = X # p.
Proof.
  auto.
Qed.

Lemma gfresh_lvar : ∀ x X, X # (Lvar x).
Proof.
  unfolds fresh_gvar.
  intro. applys× in_empty_elim.
Qed.

Lemma gfresh_gvar : ∀ X Y, X # (Gvar Y) = (X ≠ Y).
Proof.
  introv; unfold fresh_gvar; simpl.
  unfold notin; rewrite in_singleton; tauto.
Qed.

Lemma gfresh_par_iff : ∀ X p1 p2,
  X # (Par p1 p2) = (X#p1 ∧ X#p2).
Proof.
  introv; unfolds fresh_gvar; simpl.
  unfold notin; rewrite in_union; rew_logic.
  tauto.
Qed.

Lemma gfresh_nil : ∀ X, X # Nil.
Proof.
  introv; unfolds fresh_gvar; simpls×.
Qed.


Lemma fresh_LV : ∀ p x, LV p = \{} → x ## p.
Proof.
  unfolds fresh_lvar. introv H. rewrites¬ H.
Qed.

Lemma lfresh_send : ∀ a x p,
  x ## (Send a p) = x ## p.
Proof.
  auto.
Qed.

Lemma lfresh_receive : ∀ a x y p,
  x ## (Receive a y p) = (x=y ∨ x ## p).
Proof.
  introv; unfold fresh_lvar; simpl.
  unfold notin; rewrite in_remove.
  unfold notin; rewrite in_singleton.
  rew_logic. tauto.
Qed.

Lemma lfresh_lvar : ∀ x y,
  x ## (Lvar y) = (x ≠ y).
Proof.
  introv; unfolds fresh_lvar; simpl.
  unfold notin; rewrite¬ in_singleton.
Qed.

Lemma lfresh_gvar : ∀ x X,
  x ## (Gvar X).
Proof.
  introv; unfold fresh_lvar; simpls¬.
Qed.

Lemma lfresh_par_iff : ∀ x p1 p2,
  x ## (Par p1 p2) = (x##p1 ∧ x##p2).
Proof.
  introv; unfold fresh_lvar; simpls¬.
  unfold notin; rewrite in_union; rew_logic.
  tauto.
Qed.

Lemma lfresh_nil : ∀ x,
  x ## Nil.
Proof.
  unfolds fresh_lvar; introv; simpls¬.
Qed.


Lemma cfresh_send : ∀ a m p,
  m ### (Send a p) = (m ### p ∧ a ≠ m).
Proof.
  introv; unfolds fresh_chan; simpls.
  unfold notin; rewrite in_union; rewrite in_singleton.
  rew_logic. intuition.
Qed.

Lemma cfresh_receive : ∀ a m y p,
  m ### (Receive a y p) = (m ### p ∧ a ≠ m).
Proof.
  introv; unfolds fresh_chan; simpls×.
  unfold notin; rewrite in_union; rewrite in_singleton.
  rew_logic; intuition.
Qed.

Lemma cfresh_lvar : ∀ m y,
  m ### (Lvar y).
Proof.
  introv. unfolds. simpls¬.
Qed.

Lemma cfresh_gvar : ∀ m X,
  m ### (Gvar X).
Proof.
  introv. unfolds. simpls¬.
Qed.

Lemma cfresh_par_iff : ∀ m p1 p2,
  m ### (Par p1 p2) = (m###p1 ∧ m###p2).
Proof.
  introv; unfold fresh_chan; simpls.
  unfold notin; rewrite in_union; rew_logic; tauto.
Qed.

Lemma cfresh_nil : ∀ m,
  m ### Nil.
Proof.
  introv. unfolds. simpls¬.
Qed.

Lemma cfresh_send_nil: ∀ m n, m ### Send n Nil = (m ≠ n).
Proof.
  introv; unfold fresh_chan; simpls.
  rewrite union_empty_r; unfold notin; rewrite in_singleton; intuition.
Qed.

Ltac freshen_up :=
  try solve [rewrite gfresh_send in *; jauto |
             rewrite gfresh_receive in *; jauto |
             rewrite gfresh_gvar in *; jauto |
             rewrite gfresh_par_iff in *; try splits; jauto |
             rewrite lfresh_send in *; jauto |
             rewrite lfresh_receive in *; jauto |
             rewrite lfresh_lvar in *; jauto |
             rewrite lfresh_par_iff in *; try splits; jauto |
             rewrite cfresh_send in *; jauto |
             rewrite cfresh_receive in *; jauto |
             rewrite cfresh_par_iff in *; try splits; jauto |
             apply× gfresh_lvar | apply× gfresh_nil |
             apply× lfresh_gvar | apply× lfresh_nil |
             apply× cfresh_lvar | apply× cfresh_gvar | apply× cfresh_nil
             ].

Ltac simpl_fresh :=
  try (rewrite gfresh_send in *);
  try (rewrite gfresh_receive in *);
  try (rewrite gfresh_gvar in *);
  try (rewrite gfresh_par_iff in *);
  try (rewrite lfresh_send in *);
  try (rewrite lfresh_receive in *);
  try (rewrite lfresh_lvar in *);
  try (rewrite lfresh_par_iff in *);
  try (rewrite cfresh_send in *);
  try (rewrite cfresh_receive in *);
  try (rewrite cfresh_par_iff in *);
  try (rewrite cfresh_send_nil in *).


Lemma size_subst : ∀ X p q,
  (size q) = 1 → (size ([q // X]p)) = (size p).
Proof.
  induction p; simpls*; cases_if×.
Qed.

Lemma size_lsubst : ∀ x p q,
  size q = 1 → size p = size ([q /// x]p).
Proof.
  introv H.
  inductions p; simpls× ; cases_if× ; simpls×.
Qed.

Lemma sizeP_subst : ∀ X p q,
  (sizeP q) = 1 → (sizeP ([q // X]p)) = (sizeP p).
Proof.
  induction p; simpls*; cases_if×.
Qed.



Lemma swap_gvar_left : ∀ X X´, {{X,X´}}X = X´.
Proof.
  introv. unfolds. cases_if×.
Qed.

Lemma swap_gvar_right : ∀ X X´, {{X,X´}}X´ = X.
Proof.
  introv. unfolds. cases_if×. cases_if×.
Qed.

Lemma swap_gvar_equal : ∀ X Y,
  {{X,X}}Y = Y.
Proof.
  introv. unfolds ; cases_if× ; cases_if×.
Qed.

Lemma swap_equal : ∀ X p, {{[X,X]}}p = p.
Proof.
  inductions p; simpls*; fequals. apply swap_gvar_equal.
Qed.

Lemma swap_gvar_equal_iff : ∀ X X´ Y Y´,
  Y = Y´ ↔ {{X,X´}}Y = {{X,X´}}Y´.
Proof.
  split. introv H. congruence.
  introv H. unfolds in H ; repeat cases_if*; repeat congruence.
Qed.

Lemma swap_gvar_involutive : ∀ X X´ Y,
  {{X,X´}}({{X,X´}}Y) = Y.
Proof.
  introv ; unfolds ; repeat cases_if×. congruence.
Qed.

Lemma swap_involutive : ∀ X Y p, {{[X,Y]}}({{[X,Y]}}p) = p.
Proof.
  inductions p; simpls*; fequals. apply swap_gvar_involutive.
Qed.

Lemma swap_sym : ∀ p X Y, {{[X,Y]}}p = {{[Y,X]}}p.
Proof.
  inductions p; introv; simpls; try rewrite¬ IHp; auto.
  unfold swap_gvar; repeat cases_if*; substs¬.
  rewrite IHp1; rewrite¬ IHp2.
Qed.


Lemma swap_name_equal : ∀ m n,
  {{|m,m|}}n = n.
Proof.
  introv. unfolds ; cases_if× ; cases_if×.
Qed.

Lemma swap_chan_equal : ∀ m p, |m,m|p = p.
Proof.
  inductions p; simpls*; fequals; apply swap_name_equal.
Qed.

Lemma swap_chan_sym : ∀ p m n, |m, n|p = |n, m|p.
Proof.
 inductions p; introv; simpls; try rewrite¬ IHp; auto.
  unfold swap_name; repeat cases_if*; substs¬.
  unfold swap_name; repeat cases_if*; substs¬.
  rewrite IHp1; rewrite¬ IHp2.
Qed.

Lemma swap_name_involutive : ∀ m n a,
  {{|m,n|}}({{|m,n|}}a) = a.
Proof.
  introv ; unfolds ; repeat cases_if×. congruence.
Qed.

Lemma swap_chan_involutive : ∀ m n p,
  |m,n|(|m,n|p) = p.
Proof.
  inductions p; simpls*; fequals; apply swap_name_involutive.
Qed.


Lemma subst_gvar_idem : ∀ X p,
  [Gvar X//X]p = p.
Proof.
  inductions p; simpls*; fequals; cases_if×. congruence.
Qed.

Lemma subst_gvar_equal : ∀ X q, [q//X](Gvar X) = q.
Proof.
  introv; unfolds; cases_if×.
Qed.

Lemma subst_lvar_idem : ∀ x p,
  [Lvar x /// x]p = p.
Proof.
  inductions p; simpls*; fequals; cases_if×. congruence.
Qed.

Lemma subst_lvar_equal : ∀ x q, [q///x](Lvar x) = q.
Proof.
  introv; unfolds; cases_if×.
Qed.


Lemma gfresh_from_subst : ∀ X Y p q, X ≠ Y → X # ([q//Y]p) → X # p.
Proof with freshen_up.
  induction p; intros; simpls×...
  cases_if*; subst...
Qed.

Lemma gfresh_from_lsubst : ∀ X Y p x,
  X ≠ Y → X # ([(Gvar Y) /// x]p) → X # p.
Proof with freshen_up.
  induction p; intros q Hf1 Hf2; simpls...
  cases_if×.
Qed.

Lemma gfresh_in_subst_p_q : ∀ X Y p q,
  X # p → X # q → X # ([q // Y]p).
Proof with freshen_up.
  induction p; intros q Hf1 Hf2; simpls...
  cases_if*; subst...
Qed.

Lemma gfresh_in_lsubst_p_q : ∀ X x p q,
  X # p → X # q → X # ([q /// x]p).
Proof with freshen_up.
  induction p; intros q Hf1 Hf2; simpls...
  cases_if*; subst...
  cases_if×.
Qed.

Lemma gfresh_in_self_subst : ∀ p X q, X # q → X # [q // X]p.
Proof with freshen_up.
  inductions p; introv Hf; simpls×...
  cases_if×...
Qed.

Lemma gfresh_subst_rewrite : ∀ (X:var) (p q:process),
  X # p → [q // X]p = p.
Proof with freshen_up.
  introv H. inductions p; simpls*; try fequals...
  cases_if*; subst; false...
Qed.

Lemma lfresh_subst_rewrite : ∀ (x:lvar) (p q:process),
  x ## p → [q /// x]p = p.
Proof with freshen_up.
  introv H; inductions p; simpls; fequals...
  cases_if*; fequals; apply IHp. rewrite lfresh_receive in H. intuition eauto.
  cases_if*; subst; false...
Qed.

Lemma lfresh_in_subst_p_q : ∀ x X p q, x ## p → x ## q → x ## ([q//X] p).
Proof with freshen_up.
  induction p; intros q Hfp Hfq; simpls¬...
  rewrite lfresh_receive in ×. inverts Hfp; jauto.
  cases_if*; subst; false...
Qed.

Lemma gfresh_swap_rewrite : ∀ X X´ p,
  X # p → X´ # p → {{[X,X´]}}p = p.
Proof with freshen_up.
  inductions p; simpls; intros; fequals...
  unfolds; repeat cases_if*; false...
Qed.

Lemma gfresh_swap_inv : ∀ X X´ Y p,
  Y # p → ({{X,X´}}Y) # ({{[X,X´]}}p).
Proof with freshen_up.
  induction p; simpl; intros...
  unfold swap_gvar. repeat cases_if*; substs...
Qed.

Lemma gfresh_subst_is_swap : ∀ (X Y:var) (p : process),
  Y # p → [(Gvar Y)//X] p = {{[X,Y]}} p.
Proof with freshen_up.
  inductions p; simpls; introv Hf; fequals; eauto; try apply IHm1; try apply IHm2...
  cases_if*; unfold swap_gvar; unfolds in Hf; repeat cases_if×.
  apply notin_singleton in Hf; false¬.
Qed.

Lemma gfresh_subst_involutive : ∀ p X Y, X # p →
  [Gvar Y // X]([Gvar X // Y]p) = p.
Proof with freshen_up.
  inductions p; introv Hf; simpls; fequals×...
    cases_if; simpls; cases_if×.
      rewrite¬ e. false...
Qed.

Ltac fresh_solve :=
  try match goal with
    | [ |- ?X # ([?q // ?X]?p) ] ⇒ apply× (gfresh_in_self_subst p X q)
    | [ |- ?X # ([?q // ?Y]?p) ] ⇒ apply× (gfresh_in_subst_p_q X Y p q)
    | [ |- ?x ## ([?q // ?y]?p) ] ⇒ apply× (lfresh_in_subst_p_q x y p q)
    | [ |- ({{?X,?X´}}?Y) # ({{[?X,?X´]}}?p) ] ⇒ apply× (gfresh_swap_inv X X´ Y p)
    | [ H : ?X # ([?q // ?Y] ?p) |- ?X # ?p ] ⇒ apply× (gfresh_from_subst X Y p q)
    | [ H : ?X # ([?q // ?Y] ?p) |- _ ] ⇒ apply (gfresh_from_subst X Y p q) in H
    | [ H : ?X # ([(Gvar ?Y) /// ?x]?p) |- ?X # ?p ] ⇒ apply× (gfresh_from_lsubst X Y p x)
  end; freshen_up; try solve [intuition eauto].


Lemma gfresh_E_empty : ∀ (X:var) (p:process), X # p → (E X p) = \{}.
Proof with fresh_solve.
  intros X. induction p; simpl; intros H; auto...
  cases_if*; false...
  rewrite IHp1... rewrite IHp2...
  rewrite¬ union_empty_l.
Qed.

Lemma E_subst_inv : ∀ p l l´ X Z, X ≠ Z → (l \in E X p ↔ l \in E X ([(Lvar l´) // Z]p)).
Proof with fresh_solve.
  inductions p; introv Hneq; splits; simpls*; introv Hyp; try solve [rewrite¬ IHp; eassumption]; try solve [rewrite¬ <- IHp].
  repeat cases_if×...
  false n...
  rewrite in_union in *; inverts Hyp.
    left; auto.
    right; rewrite¬ <- IHp.
  repeat cases_if×...
  false n...
    rewrite in_union in *; inverts Hyp.
    left; auto.
    right; rewrite¬ IHp; eassumption.
  rewrite× in_empty in Hyp.
  cases_if×.
  rewrite in_union in *; inverts Hyp; [left | right].
  rewrite¬ <- IHp1. rewrite¬ <- IHp2.
  rewrite in_union in *; inverts Hyp; [left | right].
  rewrite¬ IHp1; eassumption. rewrite¬ IHp2; eassumption.
Qed.


Lemma subst_decomposition_l : ∀ (x:lvar) (X:var) (p q:process),
  x##p → ~(x \in (E X p)) → [q//X]p = [q///x][Lvar x//X]p.
Proof with freshen_up.
  introv H H1.
  inductions p; simpls; fequals; repeat cases_if; fequals×.
  repeat rewrite¬ gfresh_subst_rewrite.
  false H1. rewrite in_union. left. rewrite¬ in_singleton.
  apply IHp. rewrite lfresh_receive in H. inversion¬ H. false¬ n. rewrite¬ gfresh_E_empty.
  apply IHp. rewrite lfresh_receive in H. inversion¬ H. false¬ n. rewrite¬ in_union in H1.
  unfolds in H. apply notin_singleton in H. false¬ H.
  rewrite¬ subst_lvar_equal.
  apply IHp1... rewrite¬ in_union in H1.
  apply IHp2... rewrite¬ in_union in H1.
Qed.

Lemma subst_decomposition_g : ∀ (X Y:var) (p q:process),
  Y#p → [q//X]p = [q//Y][(Gvar Y)//X]p.
Proof with freshen_up.
  introv H.
  inductions p; simpls; fequals; repeat cases_if*; simpls×...
    cases_if¬.
    cases_if¬. false H. simpl. rewrite¬ in_singleton.
Qed.

Lemma lsubst_decomposition_g : ∀ (x:lvar) (X:var) (p q:process),
  X#p → [q///x]p = [q//X][Gvar X///x]p.
Proof.
  introv H.
  inductions p; simpls*; try rewrite× IHp; repeat cases_if×.
  rewrite¬ gfresh_subst_rewrite. rewrite¬ subst_gvar_equal.
  false. unfolds in H. apply notin_singleton in H. congruence.
  fequals;[ apply IHp1 | apply IHp2]; rewrite gfresh_par_iff in *; jauto.
Qed.


Lemma substs_commute_gg : ∀ (X Y:var) (p q r:process),
  X≠Y → X#r → Y#q → [r//Y] ([q//X] p) = [q//X] ([r//Y] p).
Proof.
  introv Hneq Hf1 Hf2. induction p; simpls~; try rewrite¬ IHp.
    cases_if~; cases_if¬.
      rewrite¬ gfresh_subst_rewrite. rewrite e. simpl. cases_if¬.
      rewrite¬ (gfresh_subst_rewrite X). rewrite e. simpl. cases_if¬.
      simpls. cases_if; cases_if¬.
    fequals.
Qed.

Lemma substs_commute_lg : ∀ (x:lvar) (X:var) (p q r:process),
  X#r → x##q → [r///x] ([q//X] p) = [q//X] ([r///x] p).
Proof.
  introv H H0.
  induction p; simpls*; try rewrite× IHp; repeat cases_if×.
  rewrite¬ gfresh_subst_rewrite. rewrite¬ lfresh_subst_rewrite.
  fequals¬.
Qed.

Lemma subst_on_subst_same : ∀ X (p q r:process),
  X#r → [r//X] ([q//X] p) = [([r//X] q)//X] p.
Proof.
  inductions p; simpls; introv Hf; try solve [fequals*].
  repeat cases_if×.
  simpls; cases_if×.
Qed.


Lemma subst_on_subst : ∀ (X Y:var) (p q r:process),
  X≠Y → X#r → [r//Y] ([q//X] p) = [([r//Y] q)//X] ([r//Y] p).
Proof.
  inductions p; simpls; introv Hneq Hf; try solve [fequals*].
  repeat cases_if×.
  rewrite e. rewrite¬ subst_gvar_equal.
  rewrite (gfresh_subst_rewrite X r ([r//Y]q)).
  rewrite e. rewrite¬ subst_gvar_equal. assumption.
  rewrite <- gfresh_gvar in n. rewrite <- gfresh_gvar in n0.
  repeat rewrite× gfresh_subst_rewrite.
Qed.

Lemma swap_on_subst : ∀ (X X´ Y:var) (p q:process),
  {{[X,X´]}} ([q//Y] p) = [({{[X,X´]}} q)//({{X,X´}} Y)] ({{[X,X´]}} p).
Proof.
  inductions p; introv; simpl; fequals*; repeat cases_if×.
  false n. rewrite× swap_gvar_equal_iff.
Qed.

Lemma subst_on_swap : ∀ X X´ Y p q, [q//Y]({{[X,X´]}}p)= {{[X,X´]}}([({{[X,X´]}}q)//({{X,X´}}Y)]p).
Proof.
  introv. rewrite <- swap_involutive with (X:=X) (Y:=X´) (p:= [q // Y]({{[X, X´]}}p)).
  fequals. rewrite swap_on_subst.
  fequals. apply swap_involutive.
Qed.

Lemma swap_chan_on_subst: ∀ m n p q X,
  (|m,n| ([q//X]p)) = [(|m,n|q) // X] (|m,n|p).
Proof.
  induction p; introv; simpls~; try rewrite¬ IHp.
    cases_if. cases_if¬. cases_if¬.
    rewrite IHp1. rewrite¬ IHp2.
Qed.


Lemma GV_subst: ∀ p q X, ¬ X # p → GV ([q // X]p) = GV p \- \{X} \u GV q.
Proof with freshen_up.
  induction p; introv Hlv; simpls¬.
    false¬ Hlv...

    cases_if; subst.
      rewrite remove_same; rewrite¬ union_empty_l.
      false Hlv...

    rewrite gfresh_par_iff in Hlv; rew_logic in Hlv.
    tests : (X # p1); tests : (X # p2);
      try lets Hc1 : IHp1 q C; try lets Hc2 : IHp2 q C0;
      try rewrite Hc1; try rewrite Hc2; try rewrite¬ gfresh_subst_rewrite.

    false×.

    rewrite union_assoc. rewrite <- remove_union_distr.
    unfold fresh_gvar in C. rewrite¬ (remove_while_notin C).
    rewrite <- remove_union_distr.
    unfold fresh_gvar in C0. rewrite¬ (remove_while_notin C0).
    repeat rewrite <- union_assoc. rewrite¬ (union_comm (GV q)).

    rewrite¬ <- union_assoc. rewrite union_comm_assoc. rewrite union_comm.
    do 2 rewrite <- union_assoc. rewrite union_same. rewrite¬ union_assoc.
    rewrite¬ remove_union_distr.

    false Hlv...
Qed.

Lemma LV_subst: ∀ p q X, LV ([q // X]p) \c LV p \u LV q.
Proof with freshen_up.
  induction p; introv Hlv; simpls; unfold subset in *;
  try solve [rewrite× in_union; cases_if*].
    applys× IHp.

    rewrite in_remove in Hlv; destruct Hlv as (Hlv1 & Hlv2).
    apply IHp in Hlv1.
    rewrite in_union in *; rewrite× in_remove.

    repeat rewrite in_union in *; inverts Hlv as Hlv;
    [apply IHp1 in Hlv | apply IHp2 in Hlv]; rewrite× in_union in Hlv.
Qed.