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

Fixpoint open{V:Set} (k : nat) (b : var) (P : proc V) : proc V:=
  match P with
  | pr_var x ⇒ pr_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 // R ⇒ open k b Q // open k b R
  | nu Q ⇒ nu (open (S k) b Q)
  | PO ⇒ PO
  end.

Fixpoint close {V:Set} (k : nat) (b : var) (P : proc V) : proc V:=
  match P with
  | pr_var x ⇒ pr_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 // R ⇒ close k b Q // close k b R
  | nu Q ⇒ nu (close (S k) b Q)
  | PO ⇒ PO
  end.

Fixpoint mapN {V: Set} (f : nat → nat) (p : proc V) : proc V :=
  match p with
  | pr_var x ⇒ pr_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 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)).

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) ? Q ⇒ fn Q
  | (b_name k) !(Q) R ⇒ fn Q \u fn R
  | Q // R ⇒ fn Q \u fn R
  | nu Q ⇒ fn Q
  | PO ⇒ \{}
  end.

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

Lemma minus_one_list : ∀ (l:list nat),
      not(mem 0 l) → ∀ x, mem x (map (fun x⇒x-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 : nat ⇒ x0 - 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) ? Q ⇒ bn Q
  | (f_name n) !(Q) R ⇒ bn 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 // R ⇒ bn Q \u bn R
  | nu Q ⇒ down_fset (bn 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 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 x ⇒ x).
   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 x ⇒ 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 ]; 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 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 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 x ⇒ mapN 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 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 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: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 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.

Fixpoint size {V:Set} (P:proc V) :=
  match P with
  | pr_var v ⇒ 0
  | a ? P' ⇒ S (size P')
  | a !(P') Q ⇒ S (size P' + size Q)
  | P' // Q ⇒ S (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.