# Library HOC01Defs

Require Export aux.
Require Import LibEpsilon.

Definition lvar := nat.

Definition chan := nat.

Inductive process : Set :=
| Send : chanprocessprocess
| Lvar : lvarprocess
| Gvar : varprocess
| Par : processprocessprocess
| Nil : process.

Definition height_fun : Type :=
varprocesslvar.

Fixpoint LV (p:process) :=
match p with
| Send _ p ⇒ (LV p)
| Receive _ x p(LV p) \- \{x}
| Lvar x\{x}
| Gvar _\{}
| Par p q(LV p) \u (LV q)
| Nil\{}
end.

Fixpoint GV (p:process) :=
match p with
| Send _ p ⇒ (GV p)
| Receive _ _ p ⇒ (GV p)
| Lvar _\{}
| Gvar X\{X}
| Par p q(GV p) \u (GV q)
| Nil\{}
end.

Definition closed_process (p:process) : Prop :=
(GV p) = \{}.

Fixpoint closed_proc_list (lr: list process) : Prop :=
match lr with
| nilTrue
| x :: xsclosed_process x closed_proc_list xs
end.

Fixpoint gvar_list (l: list var) : list process :=
match l with
| nilnil
| X :: l(Gvar X) :: (gvar_list l)
end.

Notation "^ xs" := (gvar_list xs) (at level 60).

Fixpoint size (p:process) : nat :=
match p with
| Send _ pS (size p)
| Receive _ _ pS (size p)
| Lvar _ ⇒ 1
| Gvar _ ⇒ 1
| Par p qS ((size p) + (size q))
| Nil ⇒ 0
end.

Fixpoint sizeP (p:process) : nat :=
match p with
| Send _ psizeP p + 1
| Receive _ _ psizeP p + 1
| Lvar _ ⇒ 1
| Gvar _ ⇒ 1
| Par p q(sizeP p) + (sizeP q)
| Nil ⇒ 0
end.

Fixpoint sizeX (X:var) (p:process) : nat :=
match p with
| Send _ p ⇒ (sizeX X p)
| Receive _ _ p ⇒ (sizeX X p)
| Lvar _ ⇒ 0
| Gvar Yifb (X=Y) then 1 else 0
| Par p q(sizeX X p) + (sizeX X q)
| Nil ⇒ 0
end.

Fixpoint sizeCh (m:chan) (p:process) : nat :=
match p with
| Send a pifb (a=m) then 1 + sizeCh m p else sizeCh m p
| Receive a _ pifb (a=m) then 1 + sizeCh m p else sizeCh m p
| Lvar _ ⇒ 0
| Gvar _ ⇒ 0
| Par p q(sizeCh m p) + (sizeCh m q)
| Nil ⇒ 0
end.

Definition fresh_gvar (p:process) (X:var) : Prop :=
X \notin (GV p).

Notation "X # p" := (fresh_gvar p X) (at level 60).

Fixpoint fresh_gvar_dec (p:process) (X:var) : bool :=
match p with
| Send _ pfresh_gvar_dec p X
| Receive _ _ pfresh_gvar_dec p X
| Lvar _true
| Gvar Yifb (X=Y) then false else true
| Par p q(fresh_gvar_dec p X) && (fresh_gvar_dec q X)
| Niltrue
end.

Instance fresh_gvar_decidable :
(p:process) (X:var), Decidable (X # p).
Proof.
intros.
applys¬ decidable_make (fresh_gvar_dec p X).
unfolds fresh_gvar.
induction p; simpls¬.
symmetry. applys¬ isTrue_true.
cases_if; symmetry.
substs. applys× isTrue_false. intro H. notin_false.
applys× isTrue_true.
rewrite IHp1,IHp2; repeat rewrites isTrue_def.
repeat cases_if¬.
false¬ H1.
symmetry. applys¬ isTrue_true.
Qed.

Definition fresh_lvar (p:process) (x:lvar) : Prop :=
x \notin (LV p).

Notation "x ## p" := (fresh_lvar p x) (at level 60).

Fixpoint fresh_lvar_dec (p:process) (x:lvar) : bool :=
match p with
| Send _ pfresh_lvar_dec p x
| Receive _ y pifb (x=y) then true else fresh_lvar_dec p x
| Lvar yifb (x=y) then false else true
| Gvar _true
| Par p q(fresh_lvar_dec p x) && (fresh_lvar_dec q x)
| Niltrue
end.

Instance fresh_lvar_decidable :
(p:process) (x:lvar), Decidable (x ## p).
Proof.
intros.
applys¬ decidable_make (fresh_lvar_dec p x).
unfolds fresh_lvar.
induction p; simpls~; unfolds notin; rew_logic in *; symmetry.
cases_if.
applys¬ isTrue_true. rewrite in_remove. rew_logic.
right. rewrite e. unfolds notin. rew_logic. rewrite¬ in_singleton.
rewrite isTrue_def. cases_if; symmetry.
rewrite IHp. applys¬ isTrue_true. introv . apply H. rewrite in_remove. split¬.
rewrite¬ notin_singleton.
rewrite IHp. applys¬ isTrue_false. unfolds notin. rew_logic in ×. rewrite× in_remove in H.
cases_if.
apply isTrue_false. rew_logic. rewrite¬ in_singleton.
apply isTrue_true. rewrite¬ in_singleton.
applys isTrue_true. apply notin_empty.
rewrite IHp1,IHp2. repeat rewrites isTrue_def.
repeat cases_if; rewrite in_union in H; rew_logic in H; destruct H; auto; try false.
apply isTrue_true. apply notin_empty.
Qed.

Lemma ex_fresh_gvar :
p, X, X#p.
Proof.
introv.
(proj1_sig (var_fresh (GV p))).
apply (proj2_sig (var_fresh (GV p))).
Qed.

Fixpoint GV_set (ps: list process) :=
match ps with
| nil\{}
| (p :: ps) ⇒ (GV p) \u (GV_set ps)
end.

Lemma fresh_set:
X ps,
X \notin (GV_set ps)Forall (fun pX#p) ps.
Proof.
inductions ps; simpls~; introv H.
apply Forall_nil.
apply Forall_cons.
apply notin_union in H. apply H.
apply notin_union in H. apply IHps. apply H.
Qed.

Lemma find_fresh :
(ps: list process), X, Forall (fun pX#p) ps.
Proof.
introv.
(var_gen (GV_set ps)).
lets K: var_gen_spec (GV_set ps). applys¬ fresh_set.
Qed.

Fixpoint CHS (p:process) :=
match p with
| Send a p\{a} \u (CHS p)
| Receive a _ p\{a} \u (CHS p)
| Lvar _\{}
| Gvar _\{}
| Par p q(CHS p) \u (CHS q)
| Nil\{}
end.

Definition fresh_chan (p:process) (a:chan) : Prop := a \notin (CHS p).

Notation "a ### p" := (fresh_chan p a) (at level 60).

Fixpoint fresh_chan_dec (p:process) (m:chan) : bool :=
match p with
| Send a pifb (a=m) then false else fresh_chan_dec p m
| Receive a _ pifb (a=m) then false else fresh_chan_dec p m
| Lvar _true
| Gvar _true
| Par p q(fresh_chan_dec p m) && (fresh_chan_dec q m)
| Niltrue
end.

Instance fresh_chan_decidable :
(p:process) (m:chan), Decidable (m ### p).
Proof.
intros.
applys¬ decidable_make (fresh_chan_dec p m).
unfolds fresh_chan.
induction p; simpls~; unfolds notin; rew_logic in *; symmetry.
cases_if.
applys¬ isTrue_false. rewrite in_union. rew_logic.
left. rewrite¬ in_singleton.
rewrite isTrue_def in ×. cases_if; cases_if~; symmetry.
rewrite in_union in H. rew_logic in H. false¬ H.
rewrite in_union in H. rewrite in_singleton in H. destruct H; false.
rewrite isTrue_def in ×. cases_if; cases_if~; symmetry.
rewrite in_union in H. rew_logic in H. rewrite in_singleton in H. destruct H. congruence.
cases_if¬. rewrite in_union in H. rew_logic in H. false¬ H.
cases_if¬. rewrite in_union in H. rewrite in_singleton in H. destruct H; false.
rewrite isTrue_def. cases_if¬. rewrite in_empty in H. false.
rewrite isTrue_def. cases_if¬. rewrite in_empty in H. false.
rewrite IHp1,IHp2. repeat rewrites isTrue_def.
repeat cases_if; rewrite in_union in H; rew_logic in H; destruct H; auto; try false.
apply isTrue_true. apply notin_empty.
Qed.

Definition chan_gen_list (l : list nat) :=
1 + fold_right plus O l.

Lemma chan_gen_list_spec :
n l,
n \in from_list ln < chan_gen_list l.
Proof.
unfold chan_gen_list. induction l; introv I.
rewrite from_list_nil in I. false (in_empty_elim I).
rewrite from_list_cons in I. rew_list.
rewrite in_union in I. destruct I as [H|H].
rewrite in_singleton in H. subst. nat_math.
specializes IHl H. nat_math.
Qed.

Definition chan_gen (E : fset chan) : chan :=
chan_gen_list (epsilon (fun lE = from_list l)).

Lemma chan_gen_spec :
E, (chan_gen E) \notin E.
Proof.
intros. unfold chan_gen. spec_epsilon as l.
applys fset_finite. rewrite Hl. introv H.
forwards M: chan_gen_list_spec H. nat_math.
Qed.

Fixpoint CHSs (ps : list process) : fset chan :=
match ps with
| nil\{}
| cons p ps´(CHS p) \u (CHSs ps´)
end.

Lemma fresh_CHSs:
m ps,
m \notin (CHSs ps)Forall (fun pm###p) ps.
Proof.
inductions ps; simpls~; introv H.
apply Forall_nil.
apply Forall_cons.
apply notin_union in H. apply H.
apply notin_union in H. apply IHps. apply H.
Qed.

Lemma find_fresh_chan :
(ps: list process),
m, Forall (fun pm###p) ps.
Proof.
introv.
(chan_gen (CHSs ps)).
forwards M : chan_gen_spec (CHSs ps). applys¬ fresh_CHSs.
Qed.

Lemma find_fresh_chan_n :
(n : nat) (ps : list process) (ms : list chan),
(fms : list chan),
length fms = n
noDup fms
( m, Mem m fmsForall (fun pm###p) ps)
( m, Mem m fmsForall ( m) ms).
Proof.
inductions n; introv.
(@nil chan); splits~; try constructor; introv Hm; rewrite× Mem_nil_eq in Hm.
specialize (IHn ps ms).
destruct IHn as (fms´ & Hl & Hnd & Hfp & Hfm).
set ( := chan_gen (CHSs ps \u from_list ms \u from_list fms´)).
forwards M : chan_gen_spec (CHSs ps \u from_list ms \u from_list fms´); fold in M.
unfold notin in M; repeat rewrite in_union in M; rew_logic in M; destruct M as (H1 & H2 & H3).
( :: fms´); splits.
rew_length; auto.
simpl; splits~; rewrite¬ <- from_list_spec.
introv Hm; rewrite Mem_cons_eq in Hm; inverts¬ Hm.
apply¬ fresh_CHSs.
introv Hm; rewrite Mem_cons_eq in Hm; inverts¬ Hm.
rewrite <- Forall_Mem; introv Hm; rewrite <- from_list_spec in Hm.
intro Heq; substs¬.
Qed.

Fixpoint subst (p:process) (X:var) (q:process) : process :=
match q with
| Send a qSend a (subst p X q)
| Lvar _q
| Gvar Yifb (X=Y) then p else q
| Par q1 q2 ⇒ (Par (subst p X q1) (subst p X q2))
| NilNil
end.

Notation "[ p // X ] q" := (subst p X q) (at level 60).

Fixpoint lsubst (p:process) (x:lvar) (q:process) : process :=
match q with
| Send a qSend a (lsubst p x q)
| Receive a y ifb (x=y) then q else Receive a y (lsubst p x )
| Lvar yifb (x=y) then p else q
| Gvar _q
| Par q1 q2 ⇒ (Par (lsubst p x q1) (lsubst p x q2))
| NilNil
end.

Notation "[ p /// x ] q" := (lsubst p x q) (at level 60).

Definition swap_gvar (X Y : var) : var :=
ifb (X=Y) then else ifb (=Y) then X else Y.

Fixpoint swap (X :var) (p:process) :=
match p with
| Send a pSend a (swap X p)
| Lvar _p
| Gvar YGvar (swap_gvar X Y)
| Par p qPar (swap X p) (swap X q)
| NilNil
end.

Notation "{{ X , X´ }} Y " := (swap_gvar X Y) (at level 60).
Notation "{{[ X , X´ ]}} p " := (swap X p) (at level 60).

Definition swap_name (a b c:chan) : chan :=
ifb (a=c) then b else ifb (b=c) then a else c.

Fixpoint swap_chan (m n:chan) (p:process) :=
match p with
| Send a pSend (swap_name m n a) (swap_chan m n p)
| Receive a x pReceive (swap_name m n a) x (swap_chan m n p)
| Lvar _p
| Gvar _p
| Par p qPar (swap_chan m n p) (swap_chan m n q)
| NilNil
end.

Notation "{{| m , n |}} a " := (swap_name m n a) (at level 60).
Notation " | m , n | p " := (swap_chan m n p) (at level 60).

Definition Abs (f:height_fun) (a:chan) (X:var) (p:process) :=
Receive a (f X p) ([Lvar (f X p)//X]p).

Fixpoint prod (l : list process) :=
match l with
| nilNil
| h :: tPar h (prod t)
end.

Fixpoint repeat {X : Type} (x : X) (n : nat) :=
match n with
| 0 ⇒ nil
| S nx :: (repeat x n)
end.

Lemma repeat_length :
{X : Type} (x : X) n, length (repeat x n) = n.
Proof.
induction n; simpls¬.
rew_length; nat_math.
Qed.

Lemma repeat_from_list_n :
{X : Type} (x : X) n, from_list (repeat x (S n)) = \{x}.
Proof.
induction n; simpls~; rewrite from_list_cons.
rewrite from_list_nil; rewrites¬ union_empty_r.
rewrite IHn; rewrites¬ union_same.
Qed.

Lemma repeat_Mem_in :
{X : Type} (x y : X) n,
Mem x (repeat y n) → x = y.
Proof.
inductions n; simpls; introv Hm.
rewrites× Mem_nil_eq in Hm.
rewrite Mem_cons_eq in Hm; inverts× Hm.
Qed.

Require Import Recdef.

Function process_eq_dec (p : process × process)
{measure (fun psize (fst p) + size (snd p)) p} : bool :=
match fst p, snd p with
| Send a , Send b ifb (a = b) then (process_eq_dec (, )) else false
| Receive a x , Receive b y ifb (a = b) then ifb (x = y) then (process_eq_dec (, )) else false else false
| Lvar x, Lvar yifb (x = y) then true else false
| Gvar X, Gvar Yifb (X = Y) then true else false
| Par p1 p2, Par q1 q2andb (process_eq_dec (p1, q1)) (process_eq_dec (p2, q2))
| Nil, Niltrue
| _, _false
end.
introv Hfst Hsnd _; rewrite Hfst, Hsnd; simpls; nat_math.
introv Hfst Hsnd _; rewrite Hfst, Hsnd; simpls; nat_math.
introv Hfst Hsnd ; rewrite Hfst, Hsnd; simpls; nat_math.
introv Hfst Hsnd ; rewrite Hfst, Hsnd; simpls; nat_math.
Defined.

Instance process_eq_decidable :
(p q : process), Decidable (p = q).
Proof.
intros.
applys¬ decidable_make (process_eq_dec (p, q)).
inductions p; destruct q; rewrite process_eq_dec_equation; simpl;
try cases_if; try subst; try rewrite IHp; try solve [repeat rewrite isTrue_def; repeat cases_if~].
rewrite IHp1; rewrite IHp2. repeat rewrite isTrue_def; repeat cases_if¬.
Qed.