# Library HOC03CanonicalLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.

Definition XHE (f:height_fun) :=
X Y p, (f Y p) = (f ({{X,}}Y ) ({{[X,]}}p)).

Definition XHF (f:height_fun) :=
X p, (f X p) \notin (E X p).

Definition XHP (f:height_fun) :=
X Y p q, XYX#qf X p = f X ([q//Y]p).

Definition good (f:height_fun) := (XHE f) (XHF f) (XHP f).

Fixpoint GoodF X P : nat :=
match P with
| Gvar Yifb (X=Y) then 1 else 0
| Lvar _ ⇒ 0
| Nil ⇒ 0
| Par P1 P2max (GoodF X P1) (GoodF X P2)
| Send a PGoodF X P
| Receive a x Plet := GoodF X P in
ifb (=0) then 0
else ifb (x < ) then
else S x
end.

Lemma XHE_GoodF : XHE GoodF.
Proof.
unfolds. induction p; simpls~; repeat cases_if¬.
rewrite <- swap_gvar_equal_iff in e; tauto.
Qed.

Lemma Good0 : Y p, ifb (GoodF Y p = 0)
then Y \notin (GV p) else Y \in (GV p).
Proof.
introv. inductions p; simpls; repeat cases_if¬.
rewrite¬ in_singleton.
unfold max in e; cases_if.
rewrite e in l. false. nat_math.
unfold max in e; cases_if.
rewrite e in n0. false n0. nat_math.
unfold max in e; cases_if.
unfold max in n; cases_if.
rewrite in_union. left¬.
rewrite in_union. right¬.
rewrite in_union. right¬.
Qed.

Lemma xEGood : x Y p, x \in (E Y p)x < (GoodF Y p).
Proof.
introv H. induction p; simpls*; unfolds lvar.
cases_if. cases_if. rewrite <- e. apply IHp. rewrite¬ gfresh_E_empty.
lets K: Good0. specialize (K Y p). cases_if¬.
false n. unfolds¬.
cases_if. cases_if. false. rewrite¬ <- (in_empty x).
rewrite in_union in H. elim H.
introv H1. rewrite in_singleton in H1. rewrite¬ H1.
introv H1. applys¬ IHp.
cases_if. false. erewrite <- in_empty. eassumption.
rewrite in_union in H. elim H.
introv H1. rewrite in_singleton in H1. rewrite H1. nat_math.
introv H1. specialize (IHp H1). nat_math.
rewrite× in_empty in H.
cases_if; rewrite× in_empty in H.
rewrite in_union in H. destruct H.
unfold max. cases_if.
specialize (IHp1 H). nat_math.
applys¬ IHp1.
unfold max. cases_if.
applys¬ IHp2.
specialize (IHp2 H). nat_math.
rewrite in_empty in H. false.
Qed.

Lemma XHF_GoodF : XHF GoodF.
Proof.
unfolds. introv HG. apply xEGood in HG. unfolds lvar; nat_math.
Qed.

Lemma GoodFresh : X Q, X # QGoodF X Q = 0.
Proof with freshen_up.
inductions Q; introv Hf; simpls*; repeat cases_if×...
false Hf. simpl. rewrite¬ in_singleton.
unfold max; cases_if...
Qed.

Lemma GoodFresh_iff : X p, X # p GoodF X p = 0.
Proof with (freshen_up).
introv; splits. apply GoodFresh.
gen X. induction p using (measure_induction size); destruct p;
introv Hf; simpl_fresh...
apply¬ H; simpl; nat_math.
simpls; repeat cases_if×.
apply¬ H. nat_math.
simpls; cases_if×.
simpls. assert (GoodF X p1 = 0 GoodF X p2 = 0) by (unfold max in Hf; cases_if; nat_math).
splits; apply H; nat_math.
Qed.

Lemma XHP_GoodF : XHP GoodF.
Proof.
unfold XHP. introv HXY HXQ.
inductions p; simpls*; repeat cases_if×.
rewrite¬ <- IHp.
false n. rewrite¬ <- IHp.
rewrite <- e. applys¬ IHp.
false n1. rewrite¬ <- IHp.
false n. rewrite <- e. applys¬ IHp.
false n0. rewrite¬ (IHp q).
simpl. cases_if¬.
symmetry. applys¬ GoodFresh.
simpl. cases_if¬.
Qed.

Definition f := GoodF.

Theorem f_is_good : good f.
Proof.
unfolds good. splits.
apply XHE_GoodF.
apply XHF_GoodF.
apply XHP_GoodF.
Qed.

Opaque GoodF.

Lemma Good_chan_swap: p X m n, f X p = f X (|m,n|p).
Proof.
induction p; simpls~; introv; repeat cases_if¬.
Qed.

Lemma Abs_eq : p a X Y, Y#pAbs f a X p = Abs f a Y ([Gvar Y//X]p).
Proof.
introv H. unfolds.
assert (Hre: f Y ([Gvar Y//X]p) = f X p).
rewrite gfresh_subst_is_swap.
rewrite <- (swap_gvar_left X Y) at 1. symmetry. apply f_is_good.
assumption.
rewrite Hre. fequals.
rewrite¬ (subst_decomposition_g X Y).
Qed.

Lemma subst_on_Abs : a X Y p r,
X YX#r[r//Y]Abs f a X p = Abs f a X ([r//Y]p).
introv Hneq Hf. unfolds Abs. simpl.
lets (_ & _ & XHP) : f_is_good. specialize (XHP X Y p r Hneq Hf).
rewrite XHP. fequals.
applys¬ subst_on_subst.
Qed.

Inductive wf : processProp :=
| WfSend : (a:chan) (p:process), (wf p) → (wf (Send a p))
| WfAbs : (a:chan) (X:var) (p:process), (wf p) → (wf (Abs f a X p))
| WfGvar : (X:var), (wf (Gvar X))
| WfPar : (p q : process), (wf p) → (wf q) → (wf (Par p q))
| WfNil : (wf Nil).

Lemma my_wf_ind : (P : processProp),
( (a : chan) (p : process), wf pP pP (Send a p)) →
( (a : chan) (X : var) (p : process), wf pP pP (Abs f a X p)) →
( X : var, P (Gvar X)) →
( p q : process, wf pP pwf qP qP (Par p q)) →
P Nil
p : process, wf pP p.
Proof.
introv HI1 HI2 HI3 HI4 HI5 Hwf.
induction p using (measure_induction size). inverts Hwf.
applys¬ HI1. applys¬ H. simpl. nat_math.
unfold Abs in HI2. applys¬ HI2. applys¬ H. simpl. rewrite (size_subst).
nat_math.
simpls¬.
exact (HI3 X).
applys¬ HI4.
applys¬H. simpl. nat_math.
applys¬ H. simpl. nat_math.
exact HI5.
Qed.

Lemma wf_send : a p, (wf (Send a p)) → wf p.
Proof.
introv H; inverts¬ H.
Qed.

Lemma wf_LV : p,
(wf p) → LV p = \{}.
Proof.
induction 1 using my_wf_ind; simpls¬.
assert (Has: x X p, (LV ([Lvar x // X]p) \- \{x}) \c (LV p)).
introv. induction p0; simpls¬.
rewrite remove_comm. applys¬ remove_in_subsets.
unfold subset. introv H1. rewrite in_remove in H1. apply H1.
cases_if×. simpl. lets H1: (remove_same \{x}). applys¬ fset_eq_sub.
simpl. lets H1: (remove_from_empty \{x}). applys¬ fset_eq_sub.
simpl. rewrite union_remove. applys¬ subset_union_2.
simpl. lets H1: (remove_from_empty \{x}). applys¬ fset_eq_sub.
specialize (Has (f X p) X p). apply subset_of_empty. rewrite¬ <- IHwf.
rewrite IHwf1. rewrite IHwf2. rewrite¬ union_empty_l.
Qed.

Lemma wf_lfresh : x p,
(wf p) → x##p.
Proof.
introv Hwf. apply fresh_LV. applys¬ wf_LV.
Qed.

Lemma wf_par1 : p q, (wf (Par p q)) → (wf p).
Proof.
introv H. inverts¬ H.
Qed.

Lemma wf_par2 : p q, (wf (Par p q)) → (wf q).
Proof.
introv H. inverts¬ H.
Qed.

Lemma wf_swapping : p X , wf pwf ({{[X, ]}}p).
Proof.
introv Hwf.
induction Hwf using my_wf_ind; simpl; try constructor¬.
forwards (XHE & _ & _): f_is_good. specialize (XHE X X0 p).
rewrite XHE. rewrite swap_on_subst. constructor¬.
Qed.

Lemma wf_chan_swap : p m n, wf pwf (|m,n|p).
Proof.
introv Hwf.
induction Hwf using my_wf_ind; simpl; try constructor¬.
rewrite swap_chan_on_subst. simpl.
rewrite (Good_chan_swap p X m n); constructor¬.
Qed.

Lemma wf_prod_repeat : n p, wf pwf (prod (repeat p n)).
Proof.
induction n; introv H; simpl; constructor¬.
Qed.

Lemma wf_ind_gen : (P : processProp),
( a p, wf pP pP (Send a p)) →
( a X p, wf p → ( Y, Y#pP ([Gvar Y//X]p)) → P (Abs f a X p)) →
( X, P (Gvar X)) →
( p q, wf pP pwf qP qP (Par p q)) →
(P Nil) →
p, wf pP p.
Proof.
introv HI1 HI2 HI3 HI4 HI5 Hwf.
induction p using (measure_induction size). inverts× Hwf.
applys¬ HI1. applys¬ H. simpl. nat_math.
unfold Abs in HI2. applys¬ HI2. introv HF. applys¬ H.
simpl. rewrite_all size_subst; simpls¬. nat_math.
rewrite¬ gfresh_subst_is_swap. applys¬ wf_swapping.
applys¬ HI4; applys¬ H; simpl; nat_math.
Qed.

Lemma wf_subst : p, wf p X q, wf qwf ([q//X]p).
Proof.
introv Hwf1.
elim Hwf1 using wf_ind_gen; intros; try constructor¬.
lets (Y & Hf) : find_fresh (p0::q::(Gvar X)::(Gvar X0)::nil).
rewrite Forall_to_conj_4 in Hf. destruct Hf as (Hfp & Hfq & HfX & HfX0).
rewrite gfresh_gvar in HfX. rewrite gfresh_gvar in HfX0.
rewrite¬ (Abs_eq p0 a X Y).
rewrite¬ subst_on_Abs.
constructor¬.
simpls. cases_if¬. constructor.
Qed.

Lemma wf_receive : a x p, wf (Receive a x p) →
X, X#pwf ([Gvar X///x]p) Receive a x p = Abs f a X ([Gvar X///x]p).
Proof.
introv Hwf Hf. split.
inverts Hwf. rewrite <- subst_decomposition_l.
applys¬ wf_subst. constructor.
applys¬ wf_lfresh. apply f_is_good.
inversion Hwf. subst a0. unfold Abs.
assert (Heq: ([Gvar X /// x]([Lvar x // X0]p0)) = {{[X0,X]}}p0).
etransitivity. symmetry. apply subst_decomposition_l.
apply wf_LV in H0. unfold fresh_lvar. rewrite H0. apply notin_empty.
rewrite <- H1. apply f_is_good.
destruct (comparable X X0) as (b & dec). cases b.
apply eq_true_l in dec. rewrite istrue_isTrue in dec.
subst X0. rewrite swap_equal. apply subst_gvar_idem.
apply eq_false_l in dec. rewrite istrue_neg in dec. rewrite istrue_isTrue in dec.
apply gfresh_subst_is_swap. rewrite <- H2 in Hf. eapply gfresh_from_subst; eassumption.
subst.
rewrite Heq. assert (Heq2: f X ({{[X0, X]}}p0) = f X0 p0).
symmetry. assert (Hre: X = {{X0, X}}X0).
symmetry. apply swap_gvar_left.
rewrite Hre at 1. apply f_is_good.
rewrite Heq2. fequals. rewrite subst_on_swap.
simpl. rewrite swap_gvar_right. symmetry.
rewrite¬ swap_on_subst; simpl. rewrite swap_gvar_left.
tests : (X = X0). rewrite¬ swap_equal.
apply gfresh_from_subst in Hf; auto.
rewrite <- Heq2. rewrite¬ <- gfresh_subst_is_swap.
rewrite¬ <- subst_decomposition_g.
Qed.

Lemma wf_receive_part1 : a x p, wf (Receive a x p) → X, X#pwf ([Gvar X///x]p).
Proof.
introv Hwf; introv Hf; lets H : (wf_receive a x p Hwf X Hf); tauto.
Qed.

Record wfprocess : Set := mkWfP {proc :> process; wf_cond : wf proc}.

Hint Resolve wf_cond.

Lemma wfprocess_eq : (p q : wfprocess), p = q proc p = proc q.
Proof.
intros ; split.

intro H; rewrite H; auto.

elim ; elim ; intros procP wP procQ wQ H; simpl in H.
generalizes wQ wP; rewrite H; intros wP wQ.
assert (Heq_wP_wQ : wP = wQ) by (apply proof_irrelevance).
rewrite Heq_wP_wQ; reflexivity.
Qed.

Definition wfp_Send m (p : wfprocess) := mkWfP (Send m p) (WfSend m p (wf_cond p)).
Definition wfp_Abs a X (p : wfprocess) := mkWfP (Abs f a X p) (WfAbs a X p (wf_cond p)).
Definition wfp_Gvar X := mkWfP (Gvar X) (WfGvar X).
Definition wfp_Par (p q : wfprocess) :=
mkWfP (Par p q) (WfPar p q (wf_cond p) (wf_cond q)).
Definition wfp_Nil := mkWfP (Nil) (WfNil).

Definition wfp_subst (q : wfprocess) X (p : wfprocess) :=
mkWfP ([q//X]p) (wf_subst p (wf_cond p) X q (wf_cond q)).

Ltac rewrite_wfp_equal := rewrite wfprocess_eq; simpls¬.

Ltac rewrite_into_wfp :=
match goal with

| [ |- context[mkWfP (Send ?a ?p) ?wfCond]] ⇒
match goal with
| [ H : wf p |- _ ] ⇒
replace (mkWfP (Send a p) wfCond) with (wfp_Send a (mkWfP p H))
in × by rewrite_wfp_equal
| [ p : wfprocess |- _ ] ⇒
replace (mkWfP (Send a p) wfCond) with (wfp_Send a (mkWfP p (wf_cond p)))
in × by rewrite_wfp_equal
end

| [ |- context[mkWfP (Abs ?f ?a ?X ?p) ?wfCond]] ⇒
match goal with
| [ H : wf p |- _ ] ⇒
replace (mkWfP (Abs f a X p) wfCond) with (wfp_Abs a X (mkWfP p H))
in × by rewrite_wfp_equal
| [ p : wfprocess |- _ ] ⇒
replace (mkWfP (Abs f a X p) wfCond) with (wfp_Abs a (mkWfP p (wf_cond p)))
in × by rewrite_wfp_equal
end

| [ |- context[mkWfP (Receive ?a (?f ?X ?p) ([Lvar (?f ?X ?p) // ?X]?p)) ?wfCond]] ⇒
match goal with
| [ H : wf p |- _ ] ⇒
replace (mkWfP (Receive a (f X p) ([Lvar (f X p) // X]p)) wfCond)
with (wfp_Abs a X (mkWfP p H))
in × by rewrite_wfp_equal
| [ p : wfprocess |- _ ] ⇒
replace (mkWfP (Receive a (f X p) ([Lvar (f X p) // X]p)) wfCond)
with (wfp_Abs a X (mkWfP p (wf_cond p)))
in × by rewrite_wfp_equal
end

| [ |- context[mkWfP (Gvar ?X) ?wfCond]] ⇒
replace (mkWfP (Gvar X) wfCond) with (wfp_Gvar X)
in × by rewrite_wfp_equal

| [ |- context[mkWfP (Par ?p ?q) ?wfCond]] ⇒
match goal with
| [ Hp : wf p, Hq : wf q |- _ ] ⇒
replace (mkWfP (Par p q) wfCond) with (wfp_Par (mkWfP p Hp) (mkWfP q Hq))
in × by rewrite_wfp_equal
| [ p : wfprocess, Hq : wf q |- _ ] ⇒
replace (mkWfP (Par p q) wfCond)
with (wfp_Par (mkWfP p (wf_cond p)) (mkWfP q Hq))
in × by rewrite_wfp_equal
| [ Hp : wf p, Hq : wf q |- _ ] ⇒
replace (mkWfP (Par p q) wfCond) with (wfp_Par (mkWfP p Hp) (mkWfP q Hq))
in × by rewrite_wfp_equal
| [ Hp : wf p, q : wfprocess |- _ ] ⇒
replace (mkWfP (Par p q) wfCond)
with (wfp_Par (mkWfP p Hp) (mkWfP q (wf_cond q)))
in × by rewrite_wfp_equal
| [ p : wfprocess, q : wfprocess |- _ ] ⇒
replace (mkWfP (Par p q) wfCond)
with (wfp_Par (mkWfP p (wf_cond p)) (mkWfP q (wf_cond q)))
in × by rewrite_wfp_equal
end

| [ |- context[mkWfP Nil ?wfCond]] ⇒
replace (mkWfP Nil wfCond) with (wfp_Nil)
in × by rewrite_wfp_equal
end.

Definition wfp_size (p : wfprocess) : nat := size (proc p).

Ltac solve_wfp_size :=
try match goal with
| [ |- wfp_size _ < wfp_size (wfp_Abs _ _ _) ] ⇒
unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
| [ |- wfp_size _ = wfp_size (wfp_Abs _ _ _) ] ⇒
unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
| [ |- wfp_size (wfp_Abs _ _ _) = wfp_size _ ] ⇒
unfold wfp_size in *; simpls; repeat rewrite¬ size_subst; nat_math
end;
try (unfold wfp_size in *; simpls; nat_math).

Definition wfp_sizeP (p : wfprocess) : nat := sizeP (proc p).

Ltac solve_wfp_sizeP :=
try match goal with
| [ |- wfp_sizeP _ < wfp_sizeP (wfp_Abs _ _ _) ] ⇒
unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
| [ |- wfp_sizeP _ = wfp_sizeP (wfp_Abs _ _ _) ] ⇒
unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
| [ |- wfp_sizeP (wfp_Abs _ _ _) = wfp_sizeP _ ] ⇒
unfold wfp_sizeP in *; simpls; repeat rewrite¬ sizeP_subst; nat_math
end;
try (unfold wfp_sizeP in *; simpls; nat_math).

Lemma wfp_ind : (P : wfprocessProp),
( (a : chan) (p : wfprocess), P pP (wfp_Send a p)) →
( (a : chan) (X : var) (p : wfprocess), P pP (wfp_Abs a X p)) →
( X : var, P (wfp_Gvar X)) →
( p q : wfprocess, P pP qP (wfp_Par p q)) →
P wfp_Nil
p : wfprocess, P p.
Proof with solve_wfp_size.
introv HSend HAbs HGvar HPar HNil.
induction p using (measure_induction wfp_size).

induction p; rename proc0 into p.
induction p; inversion wf_cond0; subst; try rewrite_into_wfp; auto.
applys¬ HSend; apply H...
applys¬ HAbs; apply H...
applys¬ HPar; apply H...
Qed.

Lemma wf_characterize : p : wfprocess,
( a , p = wfp_Send a )
( a X , p = wfp_Abs a X )
( X, p = wfp_Gvar X)
( p1 p2, p = wfp_Par p1 p2)
p = wfp_Nil.
Proof.
induction p using wfp_ind.
branch 1. ¬ a p.
branch 2. ¬ a X p.
branch 3. ¬ X.
branch 4. ¬ p1 p2.
branch 5. auto.
Qed.

Ltac destruct_wf q :=
let p := fresh "p" in
let a := fresh "a" in
let X := fresh "X" in
let p1 := fresh "p1" in
let p2 := fresh "p2" in
let Hyp := fresh "Hyp" in
destruct (wf_characterize q) as
[[a [p Hyp]] |
[[a [X [p Hyp]]] |
[[X Hyp] |
[[p1 [p2 Hyp]] | ]]]]; subst q.

Lemma wfp_ind_gen : (P : wfprocessProp),
( a p, P pP (wfp_Send a p)) →
( a X (p : wfprocess), ( Y, Y#pP (wfp_subst (wfp_Gvar Y) X p)) → P (wfp_Abs a X p)) →
( X, P (wfp_Gvar X)) →
( p q, P pP qP (wfp_Par p q)) →
(P wfp_Nil) →
p, P p.
Proof with (solve_wfp_size).
introv HI1 HI2 HI3 HI4 HI5.
induction p using (measure_induction wfp_size).
destruct_wf p; jauto.
applys¬ HI1. applys¬ H...
apply HI2. introv Hf; apply H...
applys¬ HI4; applys¬ H...
Qed.

Hint Resolve WfSend WfAbs WfGvar WfPar WfNil wf_subst wf_lfresh.

Require Import Recdef.

Function check_wf_bool (p : process) {measure size}: bool :=
match p with
| Send _ pcheck_wf_bool p
| Receive _ x p ⇒ (let X := var_gen (GV p) in
(isTrue (x = f X ([Gvar X /// x]p)) && check_wf_bool ([Gvar X /// x]p)))
| Lvar xfalse
| Gvar _true
| Par p q(check_wf_bool p) && (check_wf_bool q)
| Niltrue
end.
introv _; simpl; nat_math.
introv _. rewrite¬ <- size_lsubst.
introv _; simpl; nat_math.
introv _; simpl; nat_math.
Defined.

Instance wf_decidable : p, Decidable (wf p).
Proof with (repeat rewrite istrue_isTrue in *; jauto).
introv.
applys¬ decidable_make (check_wf_bool p).
induction p using (measure_induction size).
rewrite check_wf_bool_equation; destruct p; extens; splits; introv Hyp; simpls...
rewrite H in Hyp... constructor¬. nat_math.
rewrite H... inverts¬ Hyp. nat_math.

rewrite istrue_and in Hyp.
destruct Hyp as (Heql & Hwf)...
remember (var_gen (GV p)) as X.
rewrite <- (subst_lvar_idem l p).
rewrite lsubst_decomposition_g with (X := X).
rewrite Heql at 1 2. constructor.
rewrite¬ H in Hwf...
rewrite¬ <- size_lsubst; nat_math.
subst X. lets H1 : var_gen_spec (GV p).
unfolds¬ fresh_gvar.

rewrite istrue_and...
remember (var_gen (GV p)) as X.
apply wf_receive with (X := X) in Hyp.
destruct Hyp as (Hwf & Heq).
unfold Abs in *; splits.
inverts¬ Heq; repeat rewrite <- H2; rewrite <- H1; auto.
rewrite¬ H... rewrite¬ <- size_lsubst; nat_math.
subst X. lets H1 : var_gen_spec (GV p).
unfolds¬ fresh_gvar.

inverts Hyp.
inverts Hyp.

rewrite istrue_and in Hyp...
inverts Hyp; constructor; rewrite H in *; try nat_math...
rewrite istrue_and. inverts Hyp; split; rewrite H; try nat_math...
Qed.