Library HOC10CongrLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.


Require Import Relations.

Inductive wfcgr_step : relation wfprocess :=
 | WfCgrSend : ∀ a p q, wfcgr_step p q → wfcgr_step (wfp_Send a p) (wfp_Send a q)
 | WfCgrAbs : ∀ a X p q, wfcgr_step p q → wfcgr_step (wfp_Abs a X p) (wfp_Abs a X q)
 | WfCgrPar : ∀ p p´ q q´, wfcgr_step p p´ → wfcgr_step q q´ → wfcgr_step (wfp_Par p q) (wfp_Par p´ q´)
 | WfCgrPar_nil1 : ∀ p, (wfcgr_step p (wfp_Par p wfp_Nil))
 | WfCgrPar_nil2 : ∀ p, (wfcgr_step (wfp_Par p wfp_Nil) p)
 | WfCgrPar_com : ∀ p q, (wfcgr_step (wfp_Par p q) (wfp_Par q p))
 | WfCgrPar_assoc1 : ∀ p q r, (wfcgr_step (wfp_Par p (wfp_Par q r)) (wfp_Par (wfp_Par p q) r))
 | WfCgrPar_assoc2 : ∀ p q r, (wfcgr_step (wfp_Par (wfp_Par p q) r) (wfp_Par p (wfp_Par q r)))
 | WfCgrRefl : ∀ p, (wfcgr_step p p).

Hint Resolve WfCgrSend WfCgrAbs WfCgrPar WfCgrPar_nil1 WfCgrPar_nil2
             WfCgrPar_com WfCgrPar_assoc1 WfCgrPar_assoc2 WfCgrRefl.

Definition wfcgr := (clos_trans wfprocess wfcgr_step).

Infix "≡" := wfcgr_step (at level 60).
Infix "≡*" := wfcgr (at level 60).

Instance wfcgr_step_refl : Reflexive wfcgr_step.
Proof.
  auto.
Qed.

Instance wfcgr_step_sym : Symmetric wfcgr_step.
Proof.
  induction 1; auto; constructor¬.
Qed.

Instance wfcgr_is_eq_rel : Equivalence wfcgr.
Proof.
  split; introv.
    constructor¬.
    induction 1.
      constructor; applys¬ wfcgr_step_sym.
      eapply t_trans; eassumption.
      apply t_trans.
Qed.

Hint Resolve wfcgr_is_eq_rel.


Lemma sizeX_subst_fresh : ∀ p q X Y, X # q → X ≠ Y → sizeX X p = sizeX X ([q // Y]p).
Proof.
  inductions p; introv Hf Hneq; simpls×.
  repeat cases_if×.
    rewrite e; simpls; cases_if×.
    rewrite¬ sizeX_gfresh in Hf.
    simpls; cases_if×.
Qed.



Lemma wfcgr_step_f_inv : ∀ p q X, p ≡ q → (f X p) = (f X q).
Proof.
  induction p using (measure_induction wfp_size); introv Hc; inverts¬ Hc;
    [ | | | simpl; rewrite¬ max0neutralr |
            simpl; rewrite¬ max0neutralr |
            simpl; rewrite¬ maxcomm |
            simpl; rewrite¬ maxassoc |
            simpl; rewrite¬ maxassoc].

  simpls; apply¬ H; solve_wfp_size.

  Focus 2. simpls.
  lets Hyp1 : H X H0; try solve_wfp_size.
  lets Hyp2 : H X H1; try solve_wfp_size.
  rewrite Hyp1; rewrite¬ Hyp2.

  simpls; rename X0 into Y; elim (classic (X = Y)); intro Hneq; subst;
  repeat cases_if*; repeat rewrite <- GoodFresh_iff in *;
    try solve [false; apply n; fresh_solve];
    try solve
      [false; apply n; try fresh_solve;
       rewrite GoodFresh_iff; fold f; rewrite <- H with (y := p0); auto;
       try solve_wfp_size; rewrite <- GoodFresh_iff; fresh_solve];
    try solve
      [false; apply n; try fresh_solve;
       rewrite GoodFresh_iff; fold f; rewrite H with (q := q0); auto;
       try solve_wfp_size; rewrite <- GoodFresh_iff; fresh_solve].
    repeat rewrite <- XHP_GoodF; auto; try apply gfresh_lvar; fold f.
      apply¬ H; solve_wfp_size.
    rewrite GoodFresh_iff in *; rewrite <- XHP_GoodF in *; auto; try apply gfresh_lvar; fold f in ×.
      lets Hx : H X H0; try solve_wfp_size.
      lets Hy : H Y H0; try solve_wfp_size.
      false; nat_math.
    rewrite GoodFresh_iff in *; rewrite <- XHP_GoodF in *; auto; try apply gfresh_lvar; fold f in ×.
      lets Hx : H X H0; try solve_wfp_size.
      lets Hy : H Y H0; try solve_wfp_size.
      false; nat_math.
      lets Hy : H Y H0; try solve_wfp_size.
Qed.

Lemma wfcgr_f_inv : ∀ X p q, p ≡* q → (f X p) = (f X q).
Proof.
  introv H.
  induction H; [ | etransitivity; eassumption].
  apply¬ wfcgr_step_f_inv.
Qed.


Lemma wfcgr_send : ∀ a p q,
  p ≡* q → (wfp_Send a p) ≡* (wfp_Send a q).
Proof.
  induction 1; introv.
  constructor. constructor. assumption.
  etransitivity. eassumption. assumption.
Qed.

Lemma wfcgr_abs : ∀ a X p q,
  p ≡* q → (wfp_Abs a X p) ≡* (wfp_Abs a X q).
Proof.
  induction 1; introv.
  constructor. constructor. assumption.
  etransitivity. eassumption. assumption.
Qed.

Lemma wfcgr_par1 : ∀ p1 p2 q1,
  p1 ≡* q1 → wfp_Par p1 p2 ≡* wfp_Par q1 p2.
Proof.
  induction 1; introv.
  constructor. constructor. assumption. reflexivity.
  etransitivity. eassumption. assumption.
Qed.

Lemma wfcgr_par2 : ∀ p1 p2 q2,
  p2 ≡* q2 → (wfp_Par p1 p2) ≡* (wfp_Par p1 q2).
Proof.
  induction 1; introv.
  constructor. constructor. reflexivity. assumption.
  etransitivity. eassumption. assumption.
Qed.

Lemma wfcgr_par : ∀ p1 p2 q1 q2,
  p1 ≡* q1 → p2 ≡* q2 → (wfp_Par p1 p2) ≡* (wfp_Par q1 q2).
Proof.
  introv Hc1 Hc2.
  etransitivity. eapply wfcgr_par1. eassumption.
  applys¬ wfcgr_par2.
Qed.

Lemma wfcgr_nil_l : ∀ p, p ≡* (wfp_Par p wfp_Nil).
Proof.
  introv; constructor×.
Qed.

Lemma wfcgr_nil_r : ∀ p, (wfp_Par p wfp_Nil) ≡* p.
Proof.
  introv; constructor×.
Qed.

Lemma wfcgr_par_com : ∀ p q, (wfp_Par p q) ≡* (wfp_Par q p).
Proof.
  introv; constructor×.
Qed.

Lemma wfcgr_par_assoc_l : ∀ p q r, (wfp_Par p (wfp_Par q r)) ≡* (wfp_Par (wfp_Par p q) r).
Proof.
  introv; constructor×.
Qed.

Lemma wfcgr_par_assoc_r : ∀ p q r, (wfp_Par (wfp_Par p q) r) ≡* (wfp_Par p (wfp_Par q r)).
Proof.
  introv; constructor×.
Qed.


Fixpoint num_send (p : process) :=
match p with
 | Send _ _ ⇒ 1
 | Par p q ⇒ num_send p + num_send q
 | _ ⇒ 0
end.

Lemma num_send_wfcgr : ∀ p q, p ≡* q → num_send p = num_send q.
Proof.
  introv Hc. inductions Hc; intuition.
  gen y; induction x using (measure_induction wfp_size).
  introv Hcgr. inverts Hcgr; simpls*; try solve [nat_math].
  simpls. erewrite (H p); try eassumption; try solve_wfp_size.
  erewrite (H q); try eassumption. nat_math. solve_wfp_size.
Qed.

Fixpoint num_abs (p : process) :=
match p with
 | Receive _ _ _ ⇒ 1
 | Par p q ⇒ num_abs p + num_abs q
 | _ ⇒ 0
end.

Lemma num_abs_wfcgr : ∀ p q, p ≡* q → num_abs p = num_abs q.
Proof.
  introv Hc. inductions Hc; intuition.
  gen y; induction x using (measure_induction wfp_size).
  introv Hcgr. inverts Hcgr; simpls*; try solve [nat_math].
  simpls. erewrite (H p); try eassumption; try solve_wfp_size.
  erewrite (H q); try eassumption. nat_math. solve_wfp_size.
Qed.

Fixpoint num_var (p : process) :=
match p with
 | Gvar _ ⇒ 1
 | Par p q ⇒ num_var p + num_var q
 | _ ⇒ 0
end.

Lemma num_var_wfcgr : ∀ p q, p ≡* q → num_var p = num_var q.
Proof.
  introv Hc. inductions Hc; intuition.
  gen y; induction x using (measure_induction wfp_size).
  introv Hcgr. inverts Hcgr; simpls*; try solve [nat_math].
  simpls. erewrite (H p); try eassumption; try solve_wfp_size.
  erewrite (H q); try eassumption. nat_math. solve_wfp_size.
Qed.


Lemma no_wfcgr_send_abs : ∀ a b X p q, ¬ (wfp_Send a p ≡* wfp_Abs b X q).
Proof.
  introv Hc. apply num_send_wfcgr in Hc; simpls; nat_math.
Qed.

Lemma no_wfcgr_send_gvar : ∀ a X p, ¬ (wfp_Send a p ≡* wfp_Gvar X).
Proof.
  introv Hc. apply num_send_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_send_nil : ∀ a p, ¬ (wfp_Send a p ≡* wfp_Nil).
Proof.
  introv Hc. apply num_send_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_abs_send : ∀ a b X p q, ¬ (wfp_Abs a X p ≡* wfp_Send b q).
Proof.
  introv Hc. apply num_abs_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_abs_gvar : ∀ a X Y p, ¬ (wfp_Abs a X p ≡* wfp_Gvar Y).
Proof.
  introv Hc. apply num_abs_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_abs_nil : ∀ a X p, ¬ (wfp_Abs a X p ≡* wfp_Nil).
Proof.
  introv Hc. apply num_abs_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_gvar_send : ∀ a X p, ¬ (wfp_Gvar X ≡* wfp_Send a p).
Proof.
  introv Hc. apply num_send_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_gvar_abs : ∀ a X Y p, ¬ (wfp_Gvar X ≡* wfp_Abs a Y p).
Proof.
  introv Hc. apply num_var_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_gvar_nil : ∀ X, ¬ (wfp_Gvar X ≡* wfp_Nil).
Proof.
  introv Hc. apply num_var_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_nil_send : ∀ a p, ¬ (wfp_Nil ≡* wfp_Send a p).
Proof.
  introv Hc. apply num_send_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_nil_abs : ∀ a X p, ¬ (wfp_Nil ≡* wfp_Abs a X p).
Proof.
  introv Hc. apply num_abs_wfcgr in Hc. simpls; nat_math.
Qed.

Lemma no_wfcgr_nil_gvar : ∀ X, ¬ (wfp_Nil ≡* wfp_Gvar X).
Proof.
  introv Hc. apply num_var_wfcgr in Hc. simpls; nat_math.
Qed.

Ltac congr_impossible :=
match goal with
 | [ H : wfp_Send _ _ ≡* wfp_Abs _ _ _ |- _ ] ⇒ false; applys× no_wfcgr_send_abs
 | [ H : wfp_Send _ _ ≡* wfp_Gvar _ |- _ ] ⇒ false; applys× no_wfcgr_send_gvar
 | [ H : wfp_Send _ _ ≡* wfp_Nil |- _ ] ⇒ false; applys× no_wfcgr_send_nil
 | [ H : wfp_Abs _ _ _ ≡* wfp_Send _ _ |- _ ] ⇒ false; applys× no_wfcgr_abs_send
 | [ H : wfp_Abs _ _ _ ≡* wfp_Gvar _ |- _ ] ⇒ false; applys× no_wfcgr_abs_gvar
 | [ H : wfp_Abs _ _ _ ≡* wfp_Nil |- _ ] ⇒ false; applys× no_wfcgr_abs_nil
 | [ H : wfp_Gvar _ ≡* wfp_Send _ _ |- _ ] ⇒ false; applys× no_wfcgr_gvar_send
 | [ H : wfp_Gvar _ ≡* wfp_Abs _ _ _ |- _ ] ⇒ false; applys× no_wfcgr_gvar_abs
 | [ H : wfp_Gvar _ ≡* wfp_Nil |- _ ] ⇒ false; applys× no_wfcgr_gvar_nil
 | [ H : wfp_Nil ≡* wfp_Send _ _ |- _ ] ⇒ false; applys× no_wfcgr_nil_send
 | [ H : wfp_Nil ≡* wfp_Abs _ _ _ |- _ ] ⇒ false; applys× no_wfcgr_nil_abs
 | [ H : wfp_Nil ≡* wfp_Gvar _ |- _ ] ⇒ false; applys× no_wfcgr_nil_gvar
end.


Lemma wfcgr_sizeP : ∀ p q, p ≡* q → wfp_sizeP p = wfp_sizeP q.
Proof.
  induction 1.
    induction H; auto; try solve_wfp_sizeP.
  etransitivity; eassumption.
Qed.

Lemma wfp_sizeP_0_wfcgr_nil : ∀ (p : wfprocess),
  wfp_sizeP p = 0 ↔ p ≡* wfp_Nil.
Proof.
  induction p using (measure_induction wfp_size);
  splits; introv Hyp; destruct_wf p; try congr_impossible;
  try solve [false; solve_wfp_sizeP]; try solve [solve_wfp_sizeP];
  try solve [constructor*].

  transitivity (wfp_Par wfp_Nil wfp_Nil).
  apply wfcgr_par; apply H; solve_wfp_size; solve_wfp_sizeP. constructor×.
  apply wfcgr_sizeP in Hyp. solve_wfp_sizeP.
Qed.


Lemma wfcgr_subst1_step : ∀ (X:var) (p q q´ : wfprocess),
  q ≡ q´ → wfp_subst q X p ≡ wfp_subst q´ X p.
Proof.
  introv H.
  induction p using (measure_induction wfp_size).
  lets Hcp : wf_characterize p.
  inverts Hcp as Hcp.
    destruct Hcp as (a & p´ & Heq); subst.
    do 2 rewrite wfp_eq_subst_send; constructor;
    apply H0; solve_wfp_size.
  inverts Hcp as Hcp.
    destruct Hcp as (a & Y & p´ & Heq); subst.
    elim (classic (X = Y)); introv Hneq; subst.
    do 2 rewrite wfp_eq_subst_abs1; auto.
    lets (Z & Hfz) : find_fresh (Gvar X :: proc p´ :: proc q :: proc q´ :: nil).
    rewrite Forall_to_conj_4 in Hfz; destruct Hfz as (Hfzx & Hfzp´ & Hfzq & Hfzq´).
    do 2 (rewrite wfp_eq_subst_abs3 with (Z := Z); auto).
    constructor. apply H0; solve_wfp_size.
  inverts Hcp as Hcp.
    destruct Hcp as (Y & Heq); subst.
    do 2 rewrite wfp_eq_subst_gvar; repeat cases_if×.
  inverts Hcp as Hcp.
    destruct Hcp as (p1 & p2 & Heq); subst.
      do 2 rewrite wfp_eq_subst_par; constructor*;
      apply H0; solve_wfp_size.
  do 2 rewrite wfp_eq_subst_nil; auto.
Qed.

Lemma wfcgr_subst1 : ∀ (X:var) (p q q´ : wfprocess),
  q ≡* q´ → wfp_subst q X p ≡* wfp_subst q´ X p.
Proof.
  induction 1. constructor; apply¬ wfcgr_subst1_step.
  etransitivity; eassumption.
Qed.

Lemma wfcgr_subst2_step : ∀ (p p´ q : wfprocess) (X:var),
  p ≡ p´ → wfp_subst q X p ≡ wfp_subst q X p´.
Proof.
  induction p using (measure_induction (wfp_size)).
  introv Hcgr; inverts Hcgr; repeat rewrite_wfp_subst;
    try solve [constructor~; (repeat (apply¬ H; solve_wfp_size))]; jauto.

    rename X0 into Y.
    elim (classic (X = Y)); introv Hneq; subst.
    do 2 rewrite¬ wfp_eq_subst_abs1; constructor¬.
    lets (Z & Hfz) : find_fresh (Gvar X :: proc q :: proc p0 :: proc q0 :: nil).
    rewrite Forall_to_conj_4 in Hfz; destruct Hfz as (HfzX & Hfzq´ & Hfzp0 & Hfzq0).
    do 2 (rewrite wfp_eq_subst_abs3 with (Z := Z); auto).
    constructor. repeat (apply¬ H; try solve_wfp_size).
Qed.

Lemma wfcgr_subst2 : ∀ (p p´ q : wfprocess) (X:var),
  p ≡* p´ → wfp_subst q X p ≡* wfp_subst q X p´.
Proof.
  induction 1. constructor; apply¬ wfcgr_subst2_step.
  etransitivity; eassumption.
Qed.

Lemma wfcgr_subst : ∀ (p p´ : wfprocess),
  p ≡* p´ → ∀ q q´ X, q ≡* q´ → wfp_subst q X p ≡* wfp_subst q´ X p´.
Proof.
  introv Hcp Hcq.
  etransitivity. eapply wfcgr_subst1; eassumption.
  apply¬ wfcgr_subst2.
Qed.


Lemma congr_swap : ∀ (p q : wfprocess),
  p ≡* q → ∀ X Y, wfp_swap X Y p ≡* wfp_swap X Y q.
Proof.
  induction 1.
  induction H; introv; repeat rewrite_wfp_swap.
  applys¬ wfcgr_send.
  applys¬ wfcgr_abs.
  applys¬ wfcgr_par; constructor.
  constructor. constructor.
  constructor. constructor.
  constructor. apply WfCgrPar_com.
  constructor. apply WfCgrPar_assoc1.
  constructor. apply WfCgrPar_assoc2.
  reflexivity. etransitivity.
  apply IHclos_trans1. apply IHclos_trans2.
Qed.


Lemma sizeX_wfcgr : ∀ X p q,
  p ≡ q → sizeX X p = sizeX X q.
Proof.
  induction 1; simpls*; try nat_math.
  elim (classic (X0 = X)); introv Hneq; subst.
  lets Hf1 : gfresh_lvar (f X p) X.
    apply gfresh_in_self_subst with (p := p) in Hf1.
  lets Hf2 : gfresh_lvar (f X q) X.
    apply gfresh_in_self_subst with (p := q) in Hf2.
  rewrite sizeX_gfresh in *; nat_math.
  rewrite¬ <- sizeX_subst_fresh; try apply gfresh_lvar.
  rewrite¬ <- sizeX_subst_fresh; try apply gfresh_lvar.
Qed.

Lemma wfcgr_fresh_step : ∀ p p´ X,
  p ≡ p´ → X#p → X#p´.
Proof.
  introv Hc Hf.
  rewrite sizeX_gfresh in ×. apply sizeX_wfcgr with (X := X) in Hc; nat_math.
Qed.

Lemma wfcgr_fresh : ∀ p p´ X,
  p ≡* p´→ X#p → X#p´.
Proof.
  induction 1. applys¬ wfcgr_fresh_step.
  intros H1. apply IHclos_trans2. applys¬ IHclos_trans1.
Qed.


Lemma wfcgr_inst_Abs : ∀ f (p q r : wfprocess),
   p ≡*q → wfp_inst_Abs f p ≡* wfp_inst_Abs f q.
Proof.
  inductions f; intros; simpls; try solve [applys¬ wfcgr_par; constructor*].
  apply¬ wfcgr_subst. reflexivity.
Qed.


Lemma sizeCh_wfcgr : ∀ a p q,
  p ≡ q → sizeCh a p = sizeCh a q.
Proof.
  induction 1; simpls*; try nat_math.
  repeat cases_if×. cases_if*; subst; repeat cases_if×.

  repeat rewrite <- sizeCh_subst; simpls; nat_math.
  repeat rewrite <- sizeCh_subst; simpls; nat_math.
Qed.

Lemma wfcgr_freshCh_step : ∀ p p´ a,
  p ≡ p´ → a ### p → a ### p´.
Proof.
  introv Hc Hf.
  rewrite sizeCh_cfresh in ×. apply sizeCh_wfcgr with (a := a) in Hc. nat_math.
Qed.

Lemma wfcgr_alt_freshCh : ∀ p p´ a,
  p ≡* p´→ a ### p → a ### p´.
Proof.
  induction 1. applys¬ wfcgr_freshCh_step.
  intros H1; jauto.
Qed.


Fixpoint top_channels (p : process ) :=
match p with
 | Send a _ ⇒ a :: nil
 | Receive a _ _ ⇒ a :: nil
 | Par p q ⇒ top_channels p ++ top_channels q
 | _ ⇒ nil
end.

Lemma wfcgr_top_chan_base : ∀ p q, p ≡ q → permut (top_channels p) (top_channels q).
Proof.
  induction p using (measure_induction wfp_size); introv Hcgr.
  inverts Hcgr; simpls; try rewrite app_nil_l;
  try rewrite app_nil_r; repeat rewrite app_assoc; try solve [apply permut_refl].

  apply permut_app_lr; applys¬ H; solve_wfp_size.

  apply permut_flip.
Qed.

Lemma wfcgr_top_chan : ∀ p q, p ≡* q → permut (top_channels p) (top_channels q).
Proof.
  introv Hcgr.
  inductions Hcgr. applys¬ wfcgr_top_chan_base.
  eapply permut_trans; eassumption.
Qed.


Lemma wfcgr_send_chan_eq : ∀ p q a b, wfp_Send a p ≡* wfp_Send b q → a = b.
Proof.
  introv Hcgr.
  apply wfcgr_top_chan in Hcgr; simpls.
  apply permut_mem with (x := a) in Hcgr. inverts¬ Hcgr. inverts H0.
  constructor.
Qed.

Lemma wfcgr_abs_chan_eq : ∀ p q a b X Y, wfp_Abs a X p ≡* wfp_Abs b Y q → a = b.
Proof.
  introv Hcgr.
  apply wfcgr_top_chan in Hcgr; simpls.
  apply permut_mem with (x := a) in Hcgr. inverts¬ Hcgr. inverts H0.
  constructor.
Qed.


Require Program.Wf.

Program Fixpoint Core (p : wfprocess) {measure (wfp_size p)} : option wfprocess :=
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         ifb (wfp_sizeP wfp = 0) then (Core wfq)
          else ifb (wfp_sizeP wfq = 0) then (Core wfp)
            else None
  | mkWfP (Send a q) wfc ⇒ Some p
  | mkWfP (Receive a x p´) wfc ⇒ Some p
  | mkWfP (Gvar X) wfc ⇒ Some p
  | _ ⇒ None
end.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.

Lemma Core_eq : ∀ p, Core p =
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         ifb (wfp_sizeP wfp = 0) then (Core wfq)
          else ifb (wfp_sizeP wfq = 0) then (Core wfp)
            else None
  | mkWfP (Send a q) wfc ⇒ Some p
  | mkWfP (Receive a x p´) wfc ⇒ Some p
  | mkWfP (Gvar X) wfc ⇒ Some p
  | _ ⇒ None
end.
Proof.
intros.
  unfold Core at 1. rewrite Wf.Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    inductions proc; simpl; try solve [repeat rewrite H; intuition].
    destruct proc1; destruct proc2;
    repeat cases_if*; try solve [false; solve_wfp_sizeP]; repeat fequals.
Qed.

Lemma core_eq_send : ∀ a p, Core (wfp_Send a p) = Some (wfp_Send a p).
Proof.
  introv; rewrite Core_eq; simpls¬.
Qed.

Lemma core_eq_abs : ∀ a X p, Core (wfp_Abs a X p) = Some (wfp_Abs a X p).
Proof.
  introv; rewrite Core_eq; simpls¬.
Qed.

Lemma core_eq_gvar : ∀ X, Core (wfp_Gvar X) = Some (wfp_Gvar X).
Proof.
  introv; rewrite Core_eq; simpls¬.
Qed.

Lemma core_eq_nil : Core (wfp_Nil) = None.
Proof.
  introv; rewrite Core_eq; simpls¬.
Qed.

Lemma core_eq_par : ∀ p q,
  Core (wfp_Par p q) =
    ifb (wfp_sizeP p = 0) then (Core q)
      else ifb (wfp_sizeP q = 0) then (Core p)
        else None.
Proof.
  introv; rewrite Core_eq; simpls; repeat cases_if*; fequals; rewrite_wfp_equal.
Qed.

Ltac simpl_core := repeat
  (repeat rewrite core_eq_send in *;
   repeat rewrite core_eq_abs in *;
   repeat rewrite core_eq_gvar in *;
   repeat rewrite core_eq_nil in *;
   repeat rewrite core_eq_par in *).

Lemma core_par_sizeP_0 : ∀ p, wfp_sizeP p = 0 → Core p = None.
Proof.
  induction p using (measure_induction wfp_size); introv Hyp.
  destruct_wf p; simpl_core; try solve [false; solve_wfp_sizeP]; auto.
  repeat cases_if×.
    assert (wfp_sizeP p2 = 0) by solve_wfp_sizeP.
    applys¬ H; solve_wfp_size. false; solve_wfp_sizeP.
Qed.

Lemma core_par_com : ∀ p q, Core (wfp_Par p q) = Core (wfp_Par q p).
Proof.
  introv; simpl_core; repeat cases_if×.
  apply core_par_sizeP_0 in e. apply core_par_sizeP_0 in e0.
  rewrite e, e0; auto.
Qed.

Lemma core_par_assoc_l : ∀ p q r,
  Core (wfp_Par p (wfp_Par q r)) = Core (wfp_Par (wfp_Par p q) r).
Proof.
  introv; simpl_core; repeat cases_if*; try solve [false; solve_wfp_sizeP].
Qed.

Lemma core_par_assoc_r : ∀ p q r,
  Core (wfp_Par (wfp_Par p q) r) = Core (wfp_Par p (wfp_Par q r)).
Proof.
  introv; simpl_core; repeat cases_if*; try solve [false; solve_wfp_sizeP].
Qed.


Lemma none_core_wfcgr : ∀ p q, p ≡* q → Core p = None → Core q = None.
Proof.
  introv Hc. inductions Hc; introv Hcp; [ | tauto].

  + inductions H; try solve [simpl_core; inverts Hcp]; auto.
    - simpl_core; repeat cases_if*;
      apply (t_step wfprocess wfcgr_step) in H; apply wfcgr_sizeP in H;
      apply (t_step wfprocess wfcgr_step) in H0; apply wfcgr_sizeP in H0;
      apply core_par_sizeP_0; solve_wfp_size.
    - simpl_core; repeat cases_if×.
    - simpl_core; repeat cases_if×. applys¬ core_par_sizeP_0.
    - rewrite¬ core_par_com.
    - rewrite¬ core_par_assoc_r.
    - rewrite¬ core_par_assoc_l.
Qed.

Lemma send_core_wfcgr : ∀ a p q, (p ≡* q) → ∀ p´, Core p = Some (wfp_Send a p´) → (∃ q´, Core q = Some (wfp_Send a q´) ∧ p´ ≡* q´).
Proof with (subst_wfp; jauto).
  introv Hyp. inductions Hyp; introv Hcore_x.

  + inductions H.
    - simpl_core; inverts Hcore_x... ∃ q; splits×. constructor×.
    - simpl_core; inverts Hcore_x...
    - simpl_core; repeat cases_if*;
      apply (t_step wfprocess wfcgr_step) in H; apply wfcgr_sizeP in H;
      apply (t_step wfprocess wfcgr_step) in H0; apply wfcgr_sizeP in H0;
      try solve [false; solve_wfp_sizeP].
    - simpl_core; repeat cases_if×.
      apply core_par_sizeP_0 in e. rewrite e in Hcore_x; inverts Hcore_x.
      eexists; splits*; reflexivity.
    - simpl_core; repeat cases_if×.
      eexists; splits*; reflexivity.
    - rewrite core_par_com. eexists; splits; try eassumption. reflexivity.
    - rewrite core_par_assoc_r. eexists; splits; try eassumption. reflexivity.
    - rewrite core_par_assoc_l. eexists; splits; try eassumption. reflexivity.
    - eexists; splits; try eassumption. reflexivity.

  + specializes IHHyp1 Hcore_x. destruct IHHyp1 as (y´ & Hcore_y & Hcgr_y).
    specializes IHHyp2 Hcore_y. destruct IHHyp2 as (z´ & Hcore_z & Hcgr_z).
    ∃ z´; splits×. etransitivity; eassumption.
Qed.

Lemma abs_core_wfcgr : ∀ a p q, (p ≡* q) → ∀ p´ X, Core p = Some (wfp_Abs a X p´) → (∃ q´, Core q = Some (wfp_Abs a X q´) ∧ p´ ≡* q´).
Proof with (subst_wfp; jauto).
  introv Hyp. inductions Hyp; introv Hcore_x.

  + inductions H.
    - simpl_core; inverts Hcore_x...
    - simpl_core. inverts Hcore_x...
      assert (wfp_Abs a X p = wfp_Abs a X0 p´).
        rewrite_wfp_equal; unfolds. rewrite H3. rewrite¬ H2. clear H2 H3.
      symmetry in H0. lets Heq : H0. apply wfp_Abs_equal in H0.
      destruct H0 as (_ & Hyp). cases_if*; subst.
      ∃ q; splits×. constructor×.
      destruct Hyp as (Hp´ & HfX0).
      ∃ (wfp_subst (wfp_Gvar X0) X q); substs; splits.
      fequals. apply wfp_Abs_eq. eapply wfcgr_fresh; try eassumption. constructor×.
      apply wfcgr_subst2. constructor×.
    - simpl_core; repeat cases_if*;
      apply (t_step wfprocess wfcgr_step) in H; apply wfcgr_sizeP in H;
      apply (t_step wfprocess wfcgr_step) in H0; apply wfcgr_sizeP in H0;
      try solve [false; solve_wfp_sizeP].
    - simpl_core; repeat cases_if×.
      apply core_par_sizeP_0 in e. rewrite e in Hcore_x; inverts Hcore_x.
      eexists; splits*; reflexivity.
    - simpl_core; repeat cases_if×.
      eexists; splits*; reflexivity.
    - rewrite core_par_com. eexists; splits; try eassumption. reflexivity.
    - rewrite core_par_assoc_r. eexists; splits; try eassumption. reflexivity.
    - rewrite core_par_assoc_l. eexists; splits; try eassumption. reflexivity.
    - eexists; splits; try eassumption. reflexivity.

  + specializes IHHyp1 Hcore_x. destruct IHHyp1 as (y´ & Hcore_y & Hcgr_y).
    specializes IHHyp2 Hcore_y. destruct IHHyp2 as (z´ & Hcore_z & Hcgr_z).
    ∃ z´; splits×. etransitivity; eassumption.
Qed.

Lemma gvar_core_wfcgr : ∀ p q, (p ≡* q) → ∀ X, Core p = Some (wfp_Gvar X) → Core q = Some (wfp_Gvar X).
Proof with (subst_wfp; jauto).
  introv Hyp. inductions Hyp; introv Hcore_x.

  + inductions H; jauto.
    - simpl_core; inverts Hcore_x...
    - simpl_core; inverts Hcore_x...
    - simpl_core; repeat cases_if*;
      apply (t_step wfprocess wfcgr_step) in H; apply wfcgr_sizeP in H;
      apply (t_step wfprocess wfcgr_step) in H0; apply wfcgr_sizeP in H0;
      try solve [false; solve_wfp_sizeP].
    - simpl_core; repeat cases_if×.
      apply core_par_sizeP_0 in e. rewrite e in Hcore_x; inverts Hcore_x.
    - simpl_core; repeat cases_if×.
    - rewrite¬ core_par_com.
    - rewrite¬ core_par_assoc_r.
    - rewrite¬ core_par_assoc_l.

  + specializes IHHyp1 Hcore_x. applys IHHyp2...
Qed.


Lemma send_wfcgr_inv : ∀ a p q, wfp_Send a p ≡* wfp_Send a q → p ≡* q.
Proof.
  introv Hcgr. lets Hyp : send_core_wfcgr a Hcgr.
  simpl_core. lets¬ (q´ & Hq & Hcq) : Hyp p.
  inverts Hq; subst_wfp.
Qed.

Lemma abs_wfcgr_inv : ∀ a X p q, wfp_Abs a X p ≡* wfp_Abs a X q → p ≡* q.
Proof.
  introv Hcgr. lets Hyp : abs_core_wfcgr a Hcgr.
  simpl_core. lets¬ (q´ & Hq & Hcq) : Hyp p X.
  inverts Hq. assert (wfp_Abs a X q = wfp_Abs a X q´).
    rewrite_wfp_equal; unfolds. rewrite H1. rewrite¬ H0. clear H0 H1.
  apply wfp_Abs_equal in H; inverts H as (_ & H); cases_if*; subst_wfp; substs¬.
Qed.

Lemma gvar_wfcgr_inv : ∀ X Y, wfp_Gvar X ≡* wfp_Gvar Y → X = Y.
Proof.
  introv Hcgr. tests Hyp : (X = Y); auto.
  apply wfcgr_fresh with (X := Y) in Hcgr.
  simpls; rewrite gfresh_gvar in Hcgr. tauto.
  simpls; fresh_solve.
Qed.


Program Fixpoint has_top_nil (p : wfprocess) {measure (wfp_size p)} :=
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         has_top_nil wfp ∨ has_top_nil wfq
  | mkWfP (Nil) wfc ⇒ True
  | _ ⇒ False
end.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. solve_wfp_size. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.
Next Obligation. splits; introv Heq; rewrite wfprocess_eq in *; simpls; inverts Heq. Qed.

Lemma has_top_nil_eq : ∀ p, has_top_nil p =
match p with
  | mkWfP (Par p q) wfc ⇒
     let wfp := mkWfP p (wf_par1 p q wfc) in
       let wfq := mkWfP q (wf_par2 p q wfc) in
         has_top_nil wfp ∨ has_top_nil wfq
  | mkWfP (Nil) wfc ⇒ True
  | _ ⇒ False
end.
Proof.
intros.
  unfold has_top_nil at 1. rewrite Wf.Fix_eq.
  destruct p; simpl.
  destruct proc; try solve [simpls*].

  clear p; intros.
    destruct x; simpl.
    destruct proc; simpl; try solve [repeat rewrite H; intuition]; repeat fequals.
Qed.

Lemma has_top_nil_eq_send : ∀ p a, has_top_nil (wfp_Send a p) = False.
Proof.
  introv. rewrite has_top_nil_eq; simpls¬.
Qed.

Lemma has_top_nil_eq_abs : ∀ p a X, has_top_nil (wfp_Abs a X p) = False.
Proof.
  introv. rewrite has_top_nil_eq; simpls¬.
Qed.

Lemma has_top_nil_eq_gvar : ∀ X, has_top_nil (wfp_Gvar X) = False.
Proof.
  introv. rewrite has_top_nil_eq; simpls¬.
Qed.

Lemma has_top_nil_eq_par : ∀ p q, has_top_nil (wfp_Par p q) = (has_top_nil p ∨ has_top_nil q).
Proof.
  introv. rewrite has_top_nil_eq; simpls.
  assert (Hp : p = mkWfP p (wf_par1 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hp.
  assert (Hq : q = mkWfP q (wf_par2 p q (WfPar p q (wf_cond p) (wf_cond q)))) by rewrite_wfp_equal; rewrite¬ <- Hq.
Qed.

Lemma has_top_nil_eq_nil : has_top_nil wfp_Nil = True.
Proof.
  introv. rewrite has_top_nil_eq; simpls¬.
Qed.

Ltac simpl_has_top_nil := repeat
  (repeat rewrite has_top_nil_eq_send in *;
   repeat rewrite has_top_nil_eq_abs in *;
   repeat rewrite has_top_nil_eq_gvar in *;
   repeat rewrite has_top_nil_eq_par in *;
   repeat rewrite has_top_nil_eq_nil in *).

Lemma has_top_nil_sizeP_0 : ∀ p, p ≠ wfp_Nil → wfp_sizeP p = 0 →
  has_top_nil p.
Proof.
  induction p using (measure_induction wfp_size); introv Hneq Hsp.
  destruct_wf p; try solve [false; solve_wfp_sizeP].

  tests : (p1 = wfp_Nil); simpl_has_top_nil; jauto.
  left; applys× H; solve_wfp_sizeP; solve_wfp_size.
Qed.


Lemma subst_nil_eq : ∀ p X x, p = Nil ↔ [Lvar x // X] p = Nil.
Proof.
  introv; splits; introv Hyp.
  + substs¬.
  + assert (size ([Lvar x // X] p) = size Nil).
      rewrite <- Hyp; auto.
      destruct p; simpls*; inverts Hyp.
      cases_if×.
Qed.

Lemma wfp_swap_nil_eq : ∀ p X Y, p = wfp_Nil ↔ wfp_swap X Y p = wfp_Nil.
Proof.
  introv; splits; introv Hyp.
  + substs. rewrite_wfp_equal.
  + assert (wfp_size (wfp_swap X Y p) = wfp_size wfp_Nil).
      rewrite¬ Hyp. unfolds wfp_size. simpls. rewrite size_swap in ×.
      destruct_wf p; simpls*; rewrite_wfp_swap; inverts× Hyp; nat_math.
Qed.


Fixpoint has_free_par_nil (p : process) :=
match p with
 | Send a p ⇒ has_free_par_nil p
 | Receive a x p ⇒ has_free_par_nil p
 | Par p q ⇒ p = Nil ∨ q = Nil ∨ has_free_par_nil p ∨ has_free_par_nil q
 | _ ⇒ False
end.

Lemma has_top_has_free_nil : ∀ p, p ≠ wfp_Nil → has_top_nil p → has_free_par_nil p.
Proof.
  induction p using (measure_induction wfp_size).
  introv Hneq Htn; destruct_wf p; simpl_has_top_nil; simpls; try solve [intuition].

  clear Hneq. tests : (p1 = wfp_Nil); tests : (p2 = wfp_Nil); jauto; right; right.
  inverts Htn as Htn; apply H in Htn; jauto; solve_wfp_size.
Qed.

Lemma has_free_par_nil_lsubst : ∀ p x X, has_free_par_nil p ↔ has_free_par_nil ([Lvar x // X]p).
Proof.
  induction p using (measure_induction size). destruct p; simpls; introv;
  try solve [applys¬ H; solve_wfp_size]; try solve [intuition].

  splits; intro Hyp; auto; cases_if×.

  splits; intro Hyp; inverts Hyp as Hyp.
    simpl; auto. inverts Hyp as Hyp.
    simpl; auto. inverts Hyp as Hyp;
    repeat (rewrite <- H; try solve_wfp_size); jauto.
    rewrite <- subst_nil_eq in Hyp; auto.
    inverts Hyp as Hyp. rewrite <- subst_nil_eq in Hyp; eauto.
    inverts Hyp as Hyp. rewrite H; solve_wfp_size; jauto.
    rewrite (H p2); solve_wfp_size; jauto.
Qed.

Lemma has_free_par_nil_abs : ∀ a X p, has_free_par_nil (wfp_Abs a X p) ↔ has_free_par_nil p.
Proof.
  introv; simpls. rewrite <- has_free_par_nil_lsubst; intuition.
Qed.

Lemma wfcgr_exists_no_free_par_nil :
  ∀ p, ∃ q, p ≡* q ∧ ¬ has_free_par_nil q.
Proof with (solve_wfp_size; subst_wfp; simpls; jauto).
  introv. tests Hfpnp : (has_free_par_nil p).
  Focus 2. ∃ p; splits×. constructor×.

  induction p using (measure_induction wfp_size); destruct_wf p.
  + lets (q0 & Hcq0 & Hnfq0) : H p0...
    ∃ (wfp_Send a q0); splits... applys¬ wfcgr_send.
  + lets (q0 & Hcq0 & Hnfq0) : H p0...
    rewrite <- has_free_par_nil_lsubst in Hfpnp; auto.
    ∃ (wfp_Abs a X q0); splits... applys¬ wfcgr_abs.
    rewrite¬ <- has_free_par_nil_lsubst.
  + ∃ (wfp_Gvar X); splits×. constructor×.
  + simpls.
    tests Hp1 : (p1 = wfp_Nil); tests Hp2 : (p2 = wfp_Nil).
    - ∃ wfp_Nil. splits×. constructor×.
    - tests Hfpnp2 : (has_free_par_nil p2).
      × lets (p2´ & Hcp2´ & Hfnp2´) : H p2...
        ∃ p2´; splits¬. etransitivity. eapply wfcgr_par_com.
        etransitivity. applys¬ wfcgr_nil_r. auto.
      × ∃ p2; splits¬. etransitivity. apply wfcgr_par_com. constructor×.
    - tests Hfpnp1 : (has_free_par_nil p1).
      × lets (p1´ & Hcp1´ & Hfnp1´) : H p1...
        ∃ p1´; splits¬. etransitivity. applys¬ wfcgr_nil_r. auto.
      × ∃ p1; splits¬. constructor×.
    - inverts Hfpnp as Hfpnp. false...
      inverts Hfpnp as Hfpnp. false...
      tests Hfpnp1 : (has_free_par_nil p1); tests Hfpnp2 : (has_free_par_nil p2).
      × lets (p1´ & Hcp1´ & Hfnp1´) : H p1... lets (p2´ & Hcp2´ & Hfnp2´) : H p2...
        {
          tests Hnp1´ : (p1´ = wfp_Nil); tests Hnp2´ : (p2´ = wfp_Nil).
          + ∃ wfp_Nil. splits×.
            etransitivity. applys¬ wfcgr_par; eassumption. constructor×.
          + ∃ p2´; splits×.
            etransitivity. applys¬ wfcgr_par; eassumption.
            etransitivity. apply wfcgr_par_com. constructor×.
          + ∃ p1´; splits×.
            etransitivity. applys¬ wfcgr_par; eassumption. constructor×.
          + ∃ (wfp_Par p1´ p2´); splits×.
            - applys¬ wfcgr_par.
            - simpls; rew_logic; rewrite wfprocess_eq in *; auto.
       }
     × lets (p1´ & Hcp1´ & Hfnp1´) : H p1...
       {
         tests Hnp1´ : (p1´ = wfp_Nil).
         + ∃ p2. splits×.
           etransitivity. applys¬ wfcgr_par. eassumption. reflexivity.
           etransitivity. apply wfcgr_par_com. constructor×.
         + ∃ (wfp_Par p1´ p2). splits×.
           - applys¬ wfcgr_par. reflexivity.
           - simpls; rew_logic; rewrite wfprocess_eq in *; auto.
       }
     × lets (p2´ & Hcp2´ & Hfnp2´) : H p2...
       {
         tests Hnp2´ : (p2´ = wfp_Nil).
         + ∃ p1. splits×.
           etransitivity. applys¬ wfcgr_par. reflexivity. eassumption. constructor×.
         + ∃ (wfp_Par p1 p2´). splits×.
           - applys¬ wfcgr_par. reflexivity.
           - simpls; rew_logic; rewrite wfprocess_eq in *; auto.
       }
     × false×.
  + ∃ wfp_Nil; splits×. reflexivity.
Qed.

Lemma send_wfcgr_no_nil : ∀ p a q, wfp_Send a p ≡* q → (∃ p´, q ≡* wfp_Send a p´ ∧ ¬ has_free_par_nil p´).
Proof.
  introv Hcgr.
  lets (q´ & Hcgrq & Hfpnq) : wfcgr_exists_no_free_par_nil p.
  ∃ q´; splits×.

  transitivity (wfp_Send a p). symmetry; auto. applys¬ wfcgr_send.
Qed.

Lemma abs_wfcgr_no_nil : ∀ p a X q, wfp_Abs a X p ≡* q → (∃ p´, q ≡* wfp_Abs a X p´ ∧ ¬ has_free_par_nil p´).
Proof.
  introv Hcgr.
  lets (q´ & Hcgrq & Hfpnq) : wfcgr_exists_no_free_par_nil p.
  ∃ q´; splits×.

  transitivity (wfp_Abs a X p). symmetry; auto. applys¬ wfcgr_abs.
Qed.

Lemma nil_process_char : ∀ (p : wfprocess), num_send p = 0 → num_abs p = 0 →
  num_var p = 0 → (p = wfp_Nil ∨ has_free_par_nil p).
Proof.
  induction p using (measure_induction wfp_size); destruct_wf p;
  intros Hs Ha Hv; jauto; simpls; try solve [false; nat_math].

  right. simpl_has_top_nil.
  assert (num_var p1 = 0) by nat_math. specializes H H0; solve_wfp_size.
  inverts× H.
Qed.