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)).

Fixpoint mapN {V: Set} (f : nat → nat) (p : proc V) : proc V :=
  match p with
  | pr_var x ⇒ pr_var x
  | a ? P ⇒ (f a) ? (mapN f P)
  | a!(P) Q ⇒ (f a) !(mapN f P) (mapN f Q)
  | nu P ⇒ nu (mapN (liftN f 1) P)
  | P // Q ⇒ (mapN f P) // (mapN f Q)
  | PO ⇒ PO
  end.

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

Definition downfs E := map (fun x ⇒ x-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 // R ⇒ fn Q \u fn R
  | nu Q ⇒ downfs (fn Q \- \{ 0})
  | PO ⇒ \{}
  end.

Fixpoint mapV {V W : Set} (f : V → W) (P : proc V) : proc W :=
  match P with
  | pr_var x ⇒ pr_var (f x)
  | a ? P ⇒ a ? (mapV (incV_map f) P)
  | a !(P) Q ⇒ a !(mapV f P) (mapV f Q)
  | nu P ⇒ nu (mapV f P)
  | P // Q ⇒ (mapV f P) // (mapV f Q)
  | PO ⇒ PO
  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
  | VZ ⇒ pr_var VZ
  | VS y ⇒ shiftV (f y)
  end.

Fixpoint bind {V W : Set} (f : V → proc W) (P : proc V) : proc W :=
  match P with
  | pr_var x ⇒ f x
  | a ? P ⇒ a ? (bind (liftV f) P)
  | a !(P) Q ⇒ a !(bind f P) (bind f Q)
  | nu P ⇒ nu (bind (fun x ⇒ shiftN 1 (f x)) P)
  | P // Q ⇒ (bind f P) // (bind f Q)
  | PO ⇒ PO
  end.

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

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

Lemma mapV_id {V: Set} (P : proc V) :
  mapV (fun x ⇒ x) P = P.
Proof.
  induction P; default_simp; auto.
  asserts_rewrite (incV_map (fun (x:V) ⇒ x) = fun x ⇒ x).
   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 x ⇒ g (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 x ⇒ x) 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 x ⇒ g (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 x ⇒ mapN 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 V ⇒ mapN 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 x ⇒ bind 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:B→proc C)(g:A→B),
  bind f (mapV g P) = bind (fun x ⇒ f (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 : V ⇒ mapN (fun x0 ⇒ S 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.