Library Syntax

Require Export Binders MyFset TLC.LibEqual.

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 mapN {V: Set} (f : nat nat) (p : proc V) : proc V :=
  match p with
  | pr_var xpr_var x
  | a ? P(f a) ? (mapN f P)
  | a!(P) Q(f a) !(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)).

Definition downfs E := map (fun xx-1) E.

Lemma downfs_spec : E, 0 \notin E x, x \in (downfs E) (S x) \in E.
Proof.
  intros. unfold downfs in ×. split.
  - intros. apply map_spec in H0. do 2 (destruct H0). destruct x0. fsetdec. asserts_rewrite (x=x0). omega. auto.
  - intros. apply map_spec. (S x). split; auto. omega.
Qed.

Lemma downfs_0_spec : E x, x \in (downfs (E \- \{ 0})) (S x) \in E.
Proof.
  intros. rewrite downfs_spec. split; fsetdec. fsetdec.
Qed.

Hint Rewrite downfs_0_spec:fs.

Lemma downfs_empty: downfs \{} [=] \{}.
Proof.
  intros_all. rewrite downfs_spec; fsetdec.
Qed.

Lemma downfs_empty_rev : E, downfs (E \- \{0}) [=] \{} E \c \{0}.
Proof.
  intros_all. destruct a; try fsetdec. assert (a \in downfs (E \- \{0})).
  apply× downfs_0_spec. fsetdec.
Qed.

Fixpoint fn{V:Set} (P:proc V) :=
  match P with
  | pr_var x\{}
  | n ? Q\{ n } \u fn Q
  | n !(Q) R\{ n } \u fn Q \u fn R
  | Q // Rfn Q \u fn R
  | nu Qdownfs (fn 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; default_simp; auto.
  asserts_rewrite (incV_map (fun (x:V) ⇒ x) = fun xx).
   extens. intros [ | x ]; simpl; congruence.
   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; default_simp.
    rewrite IHP. 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; default_simp.
   rewrite× IHP. simpl_liftN. 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; default_simp.
   rewrite IHP. repeat fequals. extens. 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; default_simp.
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; default_simp.
  + rewrite× IHP. intros [ | x ]; simpl; trivial.
    rewrite× H.
  + rewrite× IHP. 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; default_simp.
  + erewrite IHP. eauto. intros [ | x ]; simpl; auto.
    rewrite H; repeat rewrite mapV_mapV; reflexivity.
  + erewrite IHP; eauto. 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; default_simp.
  - rewrite IHP. repeat fequals;
    extens; intros [|]; auto; intros; simpl; rewrite mapV_mapN; auto.
  - rewrite IHP. 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; default_simp.
  + rewrite IHP. repeat fequals. extens. intros [ | x ]; simpl; [ reflexivity | ].
    apply bind_mapV; reflexivity.
  + rewrite IHP. 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; default_simp.
  + rewrite IHP. fequals. extens. intros [ | x ]; simpl; auto.
  + rewrite× IHP.
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.

Lemma permut_shiftN {V:Set}: (P:proc V) k n, k < n mapN (permut k) (shiftN n P) = (shiftN n P).
Proof.
  intros. rewrite mapN_mapN. fequals.
  extens; intros. simpl_permut.
Qed.


Lemma fn_mapV {V W:Set} : (P:proc V) (f: V W), fn (mapV f P) [=] fn P.
Proof.
  intros; gen W; induction P; intros; simpl; try solve [fsetdec].
  - rewrite× IHP. fsetdec.
  - rewrite× IHP1; rewrite× IHP2. fsetdec.
  - rewrite IHP1; rewrite× IHP2. fsetdec.
  - split; intros; simplfs. rewrite× IHP in H. rewrite× IHP.
Qed.

Lemma fn_mapN {V:Set}: (P:proc V) f, fn (mapN f P) [=] map f (fn P).
Proof.
  induction P; simpl; intros.
  - rewrite map_empty. fsetdec.
  - rewrite map_union. simplfs. rewrite IHP. fsetdec.
  - rewrite map_union. rewrite map_union. simplfs. rewrite IHP1. rewrite IHP2. fsetdec.
  - rewrite map_union. rewrite IHP1. rewrite IHP2. fsetdec.
  - intros_all. split; intros; simplfs.
    rewrite IHP in H. simplfs. simpl_liftN.
     (x -1); intuition. simplfs. replace (S (x -1)) with x by omega. auto.
    rewrite IHP. simplfs. (S x). simpl_liftN. intuition.
  - rewrite map_empty. fsetdec.
Qed.

Hint Rewrite @fn_mapV @fn_mapN:fs.

Lemma fn_bind' {V W:Set} : (P:proc V) (f g: V proc W) k, k \in fn (bind g P)
    ( v, fn (g v) [=] fn (f v))
    ( v, k \notin fn (f v)) k \in fn P.
Proof.
  intros; gen W k; induction P; simpl; auto; intros.
  - false. eapply H1. rewrite H0 in H. apply H.
  - simplfs. destruct H. fsetdec. right. eapply (IHP _ (liftV f) (liftV g)); eauto.
    intros [ |]; simpl; auto. fsetdec.
    repeat (rewrite fn_mapV); rewrite H0; fsetdec. intros [ |]; simpl; auto. rewrite× @fn_mapV.
  - simplfs; destruct H. fsetdec.
    simplfs; destruct H. eapply IHP1 in H; auto; fsetdec. eapply IHP2 in H; eauto; fsetdec.
  - simplfs; destruct H. eapply IHP1 in H; auto; fsetdec. eapply IHP2 in H; eauto; fsetdec.
  - simplfs. forwards*: IHP (fun x : VmapN (fun x0S x0) (f x)) H.
    intros. repeat (rewrite fn_mapN). rewrite H0. fequals.
    intros. rewrite fn_mapN. intros_all. apply (H1 v). rewrite map_spec in H2.
    destruct H2. intuition. inverts× H3.
Qed.

Lemma fn_bind {V W:Set} : (P:proc V) (f: V proc W) x, x \in fn (bind f P)
    ( v, x \notin fn (f v)) x \in fn P.
Proof.
  intros. eapply fn_bind'; eauto. fsetdec.
Qed.

Lemma fn_subst {V:Set}: P (Q: proc V), fn (subst P Q) \c fn P \u fn Q.
Proof.
  intros_all.
  destruct (classic (a \in fn Q)). fsetdec.
  apply fn_bind in H. fsetdec.
  destruct v; simpl; auto.
Qed.