Library Syntax

Require Export Binders TLC.LibList.

Inductive proc (V : Set) : Set :=
| pr_var : V proc V
| pr_inp : name proc (incV V) proc V
| pr_snd : name proc V proc V proc V
| pr_par : proc V proc V proc V
| pr_nu : proc V proc V
| pr_nil : proc V
.

Arguments pr_var [V] _.
Arguments pr_inp [V] _ _.
Arguments pr_snd [V] _ _ _.
Arguments pr_par [V] _ _.
Arguments pr_nu [V] _.
Arguments pr_nil [V].

Notation "a ? P" := (@pr_inp _ a P) (at level 42, right associativity).
Notation "a '!(' P ')' Q" := (@pr_snd _ a P Q) (at level 42, right associativity).
Notation "P '//' Q" := (@pr_par _ P Q) (at level 40, left associativity).
Notation " 'nu' P" := (@pr_nu _ P) (at level 42, right associativity).
Notation PO := (@pr_nil _ ).

Notation proc0 := (proc Empty_set).
Notation proc1 := (proc (incV Empty_set)).


Operations on names


Fixpoint open{V:Set} (k : nat) (b : var) (P : proc V) : proc V:=
  match P with
  | pr_var xpr_var x
  | a ? Q(If (b_name k = a) then b else a) ? (open k b Q)
  | a !(Q) R(If (b_name k = a) then b else a) !(open k b Q) (open k b R)
  | Q // Ropen k b Q // open k b R
  | nu Qnu (open (S k) b Q)
  | POPO
  end.

Fixpoint close {V:Set} (k : nat) (b : var) (P : proc V) : proc V:=
  match P with
  | pr_var xpr_var x
  | a ? Q(If (f_name b = a) then k else a) ? (close k b Q)
  | a !(Q) R(If (f_name b = a) then k else a) !(close k b Q) (close k b R)
  | Q // Rclose k b Q // close k b R
  | nu Qnu (close (S k) b Q)
  | POPO
  end.

Fixpoint mapN {V: Set} (f : nat nat) (p : proc V) : proc V :=
  match p with
  | pr_var xpr_var x
  | (b_name k) ? P(b_name (f k)) ? (mapN f P)
  | (b_name k) !(P) Q(b_name (f k)) !(mapN f P) (mapN f Q)
  | (f_name n) ? P(f_name n) ? (mapN f P)
  | (f_name n) !(P) Q(f_name n) !(mapN f P) (mapN f Q)
  | nu Pnu (mapN (liftN f 1) P)
  | P // Q(mapN f P) // (mapN f Q)
  | POPO
  end.

Notation shiftN k := (mapN (fun xk+x)).

Inductive is_proc {V:Set} : proc V Prop :=
| proc_var : x, is_proc (pr_var x)
| proc_inp : (a:var) P, @is_proc (incV V) P is_proc (a? P)
| proc_out : (a:var) P Q, is_proc P is_proc Q is_proc (a!(P) Q)
| proc_par : P Q, is_proc P is_proc Q is_proc (P//Q)
| proc_nu : L P, ( x, x \notin L is_proc (open 0 x P)) is_proc (nu P)
| proc_nil : is_proc PO
.

Hint Constructors is_proc:hopi.

Fixpoint fn{V:Set} (P:proc V) : vars :=
  match P with
  | pr_var x\{}
  | (f_name n) ? Q\{n} \u fn Q
  | (f_name n) !(Q) R\{n} \u fn Q \u fn R
  | (b_name k) ? Qfn Q
  | (b_name k) !(Q) Rfn Q \u fn R
  | Q // Rfn Q \u fn R
  | nu Qfn Q
  | PO\{}
  end.

Definition down_fset (E : fset nat) := from_list (map (fun xx-1) (to_list E)).

Lemma minus_one_list : (l:list nat),
      not(mem 0 l) x, mem x (map (fun xx-1) l) mem (S x) l.
Proof.
  split; intros.
  - induction l.
    + rewrite map_nil in H0. rewrite mem_nil_eq in H0. tryfalse.
    + rewrite map_cons in H0. rewrite mem_cons_eq in H0. destruct H0.
      × subst. destruct a. false. apply H. rewrite mem_cons_eq; intuition.
        replace (S (S a - 1)) with (S a) by omega. rewrite mem_cons_eq; intuition.
      × assert (not (mem 0 l)).
        { intros_all. apply H. rewrite mem_cons_eq. intuition. }
        forwards: IHl H1; auto.
  - remember (fun x0 : natx0 - 1) as f. replace x with (f (S x)) by (subst; omega).
    apply mem_map; auto.
Qed.

Lemma down_fset_spec : E, 0 \notin E x, x \in (down_fset E) (S x) \in E.
Proof.
  intros. unfold down_fset in ×.
  rewrite from_list_spec. rewrite minus_one_list. rewrite <- from_list_spec.
  rewrite from_list_to_list. reflexivity.
  intros_all. apply H. rewrite <- from_list_to_list. rewrite from_list_spec. auto.
Qed.

Lemma down_fset_spec' : E x, x \in (down_fset (E \- \{ 0})) (S x) \in E.
Proof.
  intros. rewrite down_fset_spec; autofs. omega.
Qed.

Lemma down_fset_empty: down_fset \{} =\{}.
Proof.
  autofs. rewrite down_fset_spec in H; autofs.
Qed.

Lemma down_fset_empty_rev : E, down_fset (E \- \{0}) = \{} E \c \{0}.
Proof.
  intros.
  autofs. destruct x; auto. assert (x \in down_fset (E \- \{0})).
  apply× down_fset_spec. autofs. autofs. omega. rewrite H in H1. autofs.
Qed.

Fixpoint bn{V:Set} (P:proc V) : fset nat :=
  match P with
  | pr_var x\{}
  | (f_name n) ? Qbn Q
  | (f_name n) !(Q) Rbn Q \u bn R
  | (b_name k) ? Q\{k} \u bn Q
  | (b_name k) !(Q) R\{k} \u bn Q \u bn R
  | Q // Rbn Q \u bn R
  | nu Qdown_fset (bn Q \- \{ 0})
  | PO\{}
  end.


Operations on process variables


Fixpoint mapV {V W : Set} (f : V W) (P : proc V) : proc W :=
  match P with
  | pr_var xpr_var (f x)
  | a ? Pa ? (mapV (incV_map f) P)
  | a !(P) Qa !(mapV f P) (mapV f Q)
  | nu Pnu (mapV f P)
  | P // Q(mapV f P) // (mapV f Q)
  | POPO
  end.

Notation shiftV := (mapV (@VS _)).
Notation shiftV1 := (mapV (incV_map (@VS _))).

Definition liftV {V W: Set} (f : V proc W) (x : incV V) : proc (incV W) :=
  match x with
  | VZpr_var VZ
  | VS yshiftV (f y)
  end.

Fixpoint bind {V W : Set} (f : V proc W) (P : proc V) : proc W :=
  match P with
  | pr_var xf x
  | a ? Pa ? (bind (liftV f) P)
  | a !(P) Qa !(bind f P) (bind f Q)
  | nu Pnu (bind (fun xshiftN 1 (f x)) P)
  | P // Q(bind f P) // (bind f Q)
  | POPO
  end.

Definition subst_func {V: Set} (P : proc V) (x : incV V) : proc V :=
  match x with
  | VZP
  | VS ypr_var y
  end.

Notation subst P Q := (@bind _ _ (@subst_func _ Q) P).


Basic lemmas about monadic operations


Lemma mapV_id {V: Set} (P : proc V) :
  mapV (fun xx) P = P.
Proof.
  induction P as [ V x | V a P IHP | V a P IHP Q IHQ | V P IHP Q IHQ | V P IHP | V ];
    simpl; try (rewrite IHP); try (rewrite IHQ); auto.
  assert (incV_map (fun (x:V) ⇒ x) = fun xx).
   extens. intros [ | x ]; simpl; congruence.
  rewrite H. rewrite× IHP.
Qed.

Lemma mapV_mapV {A B C : Set} : (P : proc A)(f : A B) (g : B C),
  mapV g (mapV f P) = mapV (fun xg (f x)) P.
Proof.
  intros. gen B C. induction P as [ A x | A a P IHP | A a P IHP Q IHQ
                     | A P IHP Q IHQ | A P IHP | A ]; intros; simpl;
    try (erewrite IHP);
    try (erewrite IHQ); auto.
  repeat fequals. extens. intros [ | x]; simpl; try reflexivity.
Qed.

Lemma mapN_id {V:Set} : (P:proc V) f, ( x, f x = x) mapN f P = P.
Proof.
  induction P; intros; simpl; auto with hopi.
  - destruct n; rewrite× IHP. rewrite× H.
  - destruct n; rewrite× IHP1; rewrite× IHP2; rewrite× H.
  - rewrite× IHP1; rewrite× IHP2.
  - rewrite× IHP. intros; unfold liftN. case_if; auto. rewrite H; omega.
Qed.

Lemma mapN_id' {V:Set} : (P:proc V), mapN (fun xx) P = P.
Proof.
  intros; apply mapN_id; auto.
Qed.

Lemma mapN_mapN {V:Set}: (P:proc V) f g,
  mapN g (mapN f P) = mapN (fun xg (f x)) P.
Proof.
  induction P as [ V x | V a P IHP | V a P IHP Q IHQ
                     | V P IHP Q IHQ | V P | V ];
  simpl; intros; try (rewrite IHP; trivial); try (rewrite IHQ; trivial); auto.
  - destruct a; simpl; auto; rewrite× IHP.
  - destruct a; simpl; auto; rewrite× IHP; rewrite× IHQ.
  - repeat fequals.
    extens; intros. simpl_liftN; try omega. repeat fequals. omega.
Qed.

Lemma mapV_mapN {V W: Set}: (P:proc V) f (g:V W),
  mapV g (mapN f P) = mapN f (mapV g P).
Proof.
  intros; gen W f.
  induction P as [ V x | V a P IHP | V a P IHP Q IHQ
                     | V P IHP Q IHQ | V P | V ];
  simpl; intros; try (rewrite IHP; trivial); try (rewrite IHQ; trivial); auto.
  - destruct a; simpl; auto; rewrite× IHP.
  - destruct a; simpl; auto; rewrite× IHP; rewrite× IHQ.
Qed.

Lemma bind_return {V : Set} : (P : proc V)(f : V proc V),
  ( x, f x = pr_var x) bind f P = P.
Proof.
  induction P as [ V x | V a P IHP | V a P IHP Q IHQ
                     | V P IHP Q IHQ | V P | V ]; intros;
  simpl; try (rewrite IHP; trivial); try (rewrite IHQ; trivial); auto.
  + intros [ | x ]; simpl; trivial.
    rewrite× H.
  + intros. rewrite H. simpl; auto.
Qed.

Lemma bind_return' {V: Set} : (P : proc V), bind (@pr_var _) P = P.
Proof.
  intros; apply bind_return; reflexivity.
Qed.

Lemma bind_proc0 : (P: proc0) (f : Empty_set proc0), bind f P = P.
Proof.
  intros. apply bind_return. intros; inverts x.
Qed.

Lemma bind_mapV {A B1 B2 C : Set} : (P : proc A)
    (f1 : A B1) (f2 : B1 proc C)(g1 : A proc B2) (g2 : B2 C),
      ( x, f2 (f1 x) = mapV g2 (g1 x)) bind f2 (mapV f1 P) = mapV g2 (bind g1 P).
Proof.
  intros. gen B1 B2 C.
  induction P as [ A x | A a P IHP | A a P IHP Q IHQ | A P IHP Q IHQ | A P IHP | A ]; simpl;
    intros; try (erewrite IHP); try (erewrite IHQ); auto.
  + intros [ | x ]; simpl; auto.
    rewrite H; repeat rewrite mapV_mapV; reflexivity.
  + intros. simpl. rewrite× @mapV_mapN. rewrite× H.
Qed.

Lemma bind_mapN {V W:Set}: (P:proc V) f (g:V proc W),
    mapN f (bind g P) = bind (fun xmapN f (g x))(mapN f P).
Proof.
  intros; gen W f.
  induction P as [ V x | V a P IHP | V a P IHP Q IHQ
                     | V P IHP Q IHQ | V P | V ];
  simpl; intros; try (rewrite IHP; trivial); try (rewrite IHQ; trivial); auto.
  - destruct a; simpl; auto; repeat fequals;
    extens; intros [|]; auto; intros; simpl; rewrite mapV_mapN; auto.
  - destruct a; simpl; auto; rewrite× IHP; rewrite× IHQ.
  - repeat fequals. extens; intros. repeat (rewrite mapN_mapN).
    fequals. extens; intros. simpl_liftN. rewrite× <- minus_n_O.
Qed.

Lemma subst_mapN {V:Set}: P (Q:proc V) f, mapN f (subst P Q) = subst (mapN f P)(mapN f Q).
Proof.
  intros. rewrite bind_mapN. asserts_rewrite× ((
    fun x : incV VmapN f (subst_func Q x)) = subst_func (mapN f Q)).
    extens; intros [ |]; simpl; auto.
Qed.

Lemma bind_bind {A B C : Set}: (P : proc A)(f : A proc B) (g : B proc C),
  bind g (bind f P) = bind (fun xbind g (f x)) P.
Proof.
  intros. gen B C. induction P as [ A x | A a P IHP
                     | A a P IHP Q IHQ | A P IHP Q IHQ | A P IHP | A ];
  simpl; intros; try (erewrite IHP); try (erewrite IHQ); auto.
  + repeat fequals. extens. intros [ | x ]; simpl; [ reflexivity | ].
    apply bind_mapV; reflexivity.
  + repeat fequals. extens. intros. rewrite× <- @bind_mapN.
Qed.

Lemma bind_mapV_comp {A B C:Set}: P (f:Bproc C)(g:AB),
  bind f (mapV g P) = bind (fun xf (g x)) P.
Proof.
  intros; gen C B.
   induction P as [ A x | A a P IHP | A a P IHP Q IHQ | A P IHP Q IHQ | A P IHP | A ]; simpl;
  intros; try (erewrite IHP); try (erewrite IHQ); auto.
    repeat fequals. extens. intros [ | x ]; simpl; auto.
Qed.

Lemma subst_shift {V: Set} : (P Q : proc V), subst (shiftV P) Q = P.
Proof.
  intros; erewrite bind_mapV.
  + rewrite mapV_id; apply bind_return'.
  + reflexivity.
Qed.


size


Fixpoint size {V:Set} (P:proc V) :=
  match P with
  | pr_var v ⇒ 0
  | a ? P'S (size P')
  | a !(P') QS (size P' + size Q)
  | P' // QS (size P' + size Q)
  | nu P'S (size P')
  | PO ⇒ 0
  end.

Require Import TLC.LibNat.

Lemma size_induction :
  (P: V, proc V Prop),
    ( V x, ( W (y:proc W), size y < size x P W y) P V x)
    ( V x, P V x).
Proof.
  introv IH. intros V x. gen_eq n: (size x). gen V x.
  induction n using peano_induction. introv Eq. subst×.
Qed.