Library HOC01Defs

Require Export aux.
Require Import LibEpsilon.


Definition lvar := nat.

Definition chan := nat.

Inductive process : Set :=
 | Send : chan → process → process
 | Receive : chan → lvar → process → process
 | Lvar : lvar → process
 | Gvar : var → process
 | Par : process → process → process
 | Nil : process.

Definition height_fun : Type :=
  var → process → lvar.


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
    | nil ⇒ True
    | x :: xs ⇒ closed_process x ∧ closed_proc_list xs
  end.

Fixpoint gvar_list (l: list var) : list process :=
  match l with
    | nil ⇒ nil
    | 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 _ p ⇒ S (size p)
    | Receive _ _ p ⇒ S (size p)
    | Lvar _ ⇒ 1
    | Gvar _ ⇒ 1
    | Par p q ⇒ S ((size p) + (size q))
    | Nil ⇒ 0
  end.

Fixpoint sizeP (p:process) : nat :=
  match p with
    | Send _ p ⇒ sizeP p + 1
    | Receive _ _ p ⇒ sizeP 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 Y ⇒ ifb (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 p ⇒ ifb (a=m) then 1 + sizeCh m p else sizeCh m p
    | Receive a _ p ⇒ ifb (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 _ p ⇒ fresh_gvar_dec p X
    | Receive _ _ p ⇒ fresh_gvar_dec p X
    | Lvar _ ⇒ true
    | Gvar Y ⇒ ifb (X=Y) then false else true
    | Par p q ⇒ (fresh_gvar_dec p X) && (fresh_gvar_dec q X)
    | Nil ⇒ true
  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 _ p ⇒ fresh_lvar_dec p x
    | Receive _ y p ⇒ ifb (x=y) then true else fresh_lvar_dec p x
    | Lvar y ⇒ ifb (x=y) then false else true
    | Gvar _ ⇒ true
    | Par p q ⇒ (fresh_lvar_dec p x) && (fresh_lvar_dec q x)
    | Nil ⇒ true
  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 H´. 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 p ⇒ X#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 p ⇒ X#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 p ⇒ ifb (a=m) then false else fresh_chan_dec p m
    | Receive a _ p ⇒ ifb (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)
    | Nil ⇒ true
  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 l → n < 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 l ⇒ E = 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 p ⇒ m###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 p ⇒ m###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 fms → Forall (fun p ⇒ m###p) ps) ∧
      (∀ m, Mem m fms → Forall (≠ 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 (m´ := 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 m´ in M.
    unfold notin in M; repeat rewrite in_union in M; rew_logic in M; destruct M as (H1 & H2 & H3).
    ∃ (m´ :: 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 q ⇒ Send a (subst p X q)
    | Receive a x q ⇒ Receive a x (subst p X q)
    | Lvar _ ⇒ q
    | Gvar Y ⇒ ifb (X=Y) then p else q
    | Par q1 q2 ⇒ (Par (subst p X q1) (subst p X q2))
    | Nil ⇒ Nil
  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 q ⇒ Send a (lsubst p x q)
    | Receive a y q´ ⇒ ifb (x=y) then q else Receive a y (lsubst p x q´)
    | Lvar y ⇒ ifb (x=y) then p else q
    | Gvar _ ⇒ q
    | Par q1 q2 ⇒ (Par (lsubst p x q1) (lsubst p x q2))
    | Nil ⇒ Nil
  end.

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

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

Fixpoint swap (X X´:var) (p:process) :=
  match p with
    | Send a p ⇒ Send a (swap X X´ p)
    | Receive a x p ⇒ Receive a x (swap X X´ p)
    | Lvar _ ⇒ p
    | Gvar Y ⇒ Gvar (swap_gvar X X´ Y)
    | Par p q ⇒ Par (swap X X´ p) (swap X X´ q)
    | Nil ⇒ Nil
  end.

Notation "{{ X , X´ }} Y " := (swap_gvar X X´ Y) (at level 60).
Notation "{{[ X , X´ ]}} p " := (swap X 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 p ⇒ Send (swap_name m n a) (swap_chan m n p)
    | Receive a x p ⇒ Receive (swap_name m n a) x (swap_chan m n p)
    | Lvar _ ⇒ p
    | Gvar _ ⇒ p
    | Par p q ⇒ Par (swap_chan m n p) (swap_chan m n q)
    | Nil ⇒ Nil
  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
    | nil ⇒ Nil
    | h :: t ⇒ Par h (prod t)
  end.

Fixpoint repeat {X : Type} (x : X) (n : nat) :=
  match n with
    | 0 ⇒ nil
    | S n ⇒ x :: (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 p ⇒ size (fst p) + size (snd p)) p} : bool :=
  match fst p, snd p with
    | Send a p´, Send b q´ ⇒ ifb (a = b) then (process_eq_dec (p´, q´)) else false
    | Receive a x p´, Receive b y q´ ⇒ ifb (a = b) then ifb (x = y) then (process_eq_dec (p´, q´)) else false else false
    | Lvar x, Lvar y ⇒ ifb (x = y) then true else false
    | Gvar X, Gvar Y ⇒ ifb (X = Y) then true else false
    | Par p1 p2, Par q1 q2 ⇒ andb (process_eq_dec (p1, q1)) (process_eq_dec (p2, q2))
    | Nil, Nil ⇒ true
    | _, _ ⇒ 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.