Require Export Syntax.

Inductive label : Set :=
| out : var → label
| inp : var → label
| tau : label
.

Definition fn_lab (l:label) : vars :=
  match l with
  | tau ⇒ \{}
  | out a ⇒ \{a}
  | inp a ⇒ \{a}
  end.

Inductive abs : Set :=
| abs_def : proc1 → abs
.

Definition asubst (F : abs) (P : proc0) : proc0 :=
  match F with
  | abs_def Q ⇒ subst Q P
  end.

Inductive conc : Set :=
| conc_def : nat → proc0 → proc0 → conc
.

Inductive agent :=
| ag_proc : proc0 → agent
| ag_abs : abs → agent
| ag_conc : conc → agent
.

Coercion ag_abs : abs >-> agent.
Coercion ag_conc : conc >-> agent.

Tactic Notation "destructA" constr(A) := destruct A as [|[]|[]].

Definition fn_agent A :=
  match A with
  | ag_proc P ⇒ fn P
  | ag_abs F ⇒ match F with | abs_def P ⇒ fn P end
  | ag_conc C ⇒ match C with | conc_def k P Q ⇒ fn P \u fn Q end
  end.

Definition bn_agent A := match A with
| ag_proc P ⇒ bn P
| ag_abs F ⇒ match F with | abs_def P ⇒ bn P end
| ag_conc C ⇒ match C with | conc_def n P Q ⇒
    map_fset (fun k ⇒ k-n) (filter_fset (fun k ⇒ k ≥ n) (bn P \u bn Q)) end
end.

Definition is_agent A := match A with
| ag_proc P ⇒ is_proc P
| ag_abs F ⇒ match F with | abs_def P ⇒ is_proc P end
| ag_conc C ⇒ match C with | conc_def n P Q ⇒
                    (∀ k, k \in bn P \u bn Q → k < n) end
end.

Definition conc_wf C := match C with
| conc_def n P Q ⇒ ∀ k, k < n → k \in bn P
end.

Definition fmapN f F :=
  match F with | abs_def P ⇒ abs_def (mapN f P) end.

Definition cmapN f C :=
  match C with | conc_def n P Q ⇒ conc_def n (mapN (liftN f n) P)(mapN (liftN f n) Q) end.

Definition amapN f A := match A with
| ag_proc P ⇒ ag_proc (mapN f P)
| ag_abs F ⇒ fmapN f F
| ag_conc C ⇒ cmapN f C
end.

Definition conc_parl C P : conc :=
  match C with
  | conc_def k P' Q ⇒ conc_def k P' (Q // (shiftN k P))
  end.

Definition conc_parr P C : conc :=
  match C with
  | conc_def k P' Q ⇒ conc_def k P' ((shiftN k P) // Q)
  end.

Definition abs_parl F P : abs :=
  match F with
  | abs_def Q ⇒ abs_def (Q // (shiftV P))
  end.

Definition abs_parr P F : abs :=
  match F with
  | abs_def Q ⇒ abs_def ((shiftV P) // Q)
  end.

Definition parl A P : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_parl F P)
  | ag_proc P' ⇒ ag_proc (P' // P)
  | ag_conc C ⇒ ag_conc (conc_parl C P)
  end.

Definition parr P A : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_parr P F)
  | ag_proc P' ⇒ ag_proc (P // P')
  | ag_conc C ⇒ ag_conc (conc_parr P C)
  end.

Definition down k x := If (x ≤ k) then x else x-1.

Tactic Notation "simpl_down" := unfold down in *; intros_all; repeat (case_if; try omega).

Tactic Notation "simpl_name" := simpl_liftN; simpl_down; simpl_permut; intuition.

Definition conc_new (C:conc) : conc :=
  match C with
  | conc_def k P Q ⇒ If k \in bn P then conc_def (S k) P Q
                                     else conc_def k (mapN (down k) P) (nu (mapN (permut k) Q))
  end.

Definition abs_new (F:abs) : abs :=
  match F with
  | abs_def P ⇒ abs_def (nu P)
  end.

Definition new (A: agent) : agent :=
  match A with
  | ag_abs F ⇒ ag_abs (abs_new F)
  | ag_proc P ⇒ ag_proc (nu P)
  | ag_conc C ⇒ ag_conc (conc_new C)
  end.

Definition open_agent k (b : var) A :=
  match A with
  | ag_abs F ⇒ match F with | abs_def P ⇒ ag_abs (abs_def (open k b P)) end
  | ag_proc P ⇒ ag_proc (open k b P)
  | ag_conc C ⇒ match C with | conc_def k' P Q ⇒
                    ag_conc (conc_def k' (open (k+k') b P) (open (k+k') b Q)) end
  end.

Fixpoint genNu {V:Set} k (P:proc V) :=
  match k with
  | 0 ⇒ P
  | S k' ⇒ nu (genNu k' P)
  end.

Lemma nu_genNu {V:Set}: ∀ (P:proc V) n, nu (genNu n P) = genNu n (nu P).
Proof.
  induction n; simpl; auto.
  intros; rewrite× <- IHn.
Qed.

Definition fshiftN k F := match F with
  | abs_def P ⇒ abs_def (shiftN k P)
  end.

Definition appr F C : proc0 :=
  match C with
  | conc_def k P Q ⇒ genNu k (asubst (fshiftN k F) P // Q)
  end.

Definition appl C F : proc0 :=
  match C with
  | conc_def k P Q ⇒ genNu k (Q // asubst (fshiftN k F) P)
  end.

Inductive lts: proc0 → label → agent → Prop :=
| lts_out : ∀ (a:var) P Q, lts (a !(P) Q) (out a) (ag_conc (conc_def 0 P Q))
| lts_inp : ∀ (a:var) P, lts (a ? P) (inp a) (ag_abs (abs_def P))
| lts_parl : ∀ P Q l A, lts P l A → lts (P // Q) l (parl A Q)
| lts_parr : ∀ P Q l A, lts P l A → lts (Q // P) l (parr Q A)
| lts_new : ∀ L P l A,
    (∀ x, x \notin L → x \notin fn_lab l → lts (open 0 x P) l (open_agent 0 x A)) →
    lts (nu P) l (new A)
| lts_taul : ∀ P Q a F C, lts P (out a) (ag_conc C) →
    lts Q (inp a) (ag_abs F) → lts (P // Q) tau (ag_proc (appl C F))
| lts_taur : ∀ P Q a F C, lts Q (inp a) (ag_abs F) →
    lts P (out a) (ag_conc C) → lts (Q // P) tau (ag_proc (appr F C))
.

Hint Constructors lts:hopi.

Ltac gather_vars V :=
  let A := gather_vars_with (fun x : vars ⇒ x) in
  let B := gather_vars_with (fun x : var ⇒ \{x}) in
  let C := gather_vars_with (fun x : label ⇒ fn_lab x) in
  let D := gather_vars_with (fun x : proc V ⇒ fn x) in
  let E := gather_vars_with (fun x : agent ⇒ fn_agent x) in
  constr:(A \u B \u C \u D \u E).

Ltac pick_fresh_V V x :=
  let L := gather_vars V in (pick_fresh_gen L x).

Ltac pick_fresh_fset_V V L' x :=
  let L := gather_vars V in (pick_fresh_gen (L \u L') x).

Tactic Notation "pick_fresh" ident(x) := pick_fresh_V Empty_set x.

Lemma lts_parl' : ∀ P Q l A A', lts P l A → parl A Q = A' → lts (P // Q) l A'.
Proof.
  intros; subst; eapply lts_parl; eassumption.
Qed.

Lemma lts_parr' : ∀ P Q l A A', lts P l A → parr Q A = A' → lts (Q // P) l A'.
Proof.
  intros; subst; eapply lts_parr; eassumption.
Qed.

Lemma lts_taul' : ∀ P A' Q a F C,
    lts P (out a) (ag_conc C) → lts Q (inp a) (ag_abs F) →
    ag_proc (appl C F) = A' → lts (P // Q) tau A'.
Proof.
  intros. subst. eapply lts_taul; eassumption.
Qed.

Lemma lts_taur' : ∀ P A' Q a F C,
    lts P (out a) (ag_conc C) → lts Q (inp a) (ag_abs F) →
    ag_proc (appr F C) = A' → lts (Q // P) tau A'.
Proof.
  intros; subst; eapply lts_taur; eassumption.
Qed.

Lemma lts_new' : ∀ L P l A A',
    (∀ x, x \notin L → x \notin fn_lab l → lts (open 0 x P) l (open_agent 0 x A)) →
    new A = A' → lts (nu P) l A'.
Proof.
  intros; subst; eapply lts_new; eassumption.
Qed.

Hint Resolve lts_parl' lts_parr' lts_taul' lts_taur':hopi.

Lemma lts_tau_proc: ∀ P A, lts P tau A → ∃ P', A = ag_proc P'.
Proof.
  introv Hlts. remember tau as l.
  induction Hlts; inverts Heql; eauto;
    try (destruct IHHlts; try reflexivity; subst; eexists; simpl; reflexivity).
    pick_fresh x.
    forwards*: H0 x.
    destruct H1 as [P']. destructA A; inversion H1.
    simpl; eexists; eauto.
Qed.

Lemma lts_inp_abs : ∀ P a A, lts P (inp a) A → ∃ F, A = ag_abs F.
Proof.
  intros P a A Hlts. remember (inp a) as l.
  induction Hlts; inverts Heql; eauto;
    try (destruct IHHlts; try reflexivity; subst; eexists; simpl; auto).
    pick_fresh x. forwards*: H0 x.
    destruct H1 as [ [P''] ]. destructA A; inversion H1.
    simpl; eexists; eauto.
Qed.

Lemma lts_out_conc : ∀ P a A, lts P (out a) A → ∃ C, A = ag_conc C.
Proof.
  intros P a A Hlts. remember (out a) as l.
  induction Hlts; inverts Heql; eauto;
    try (destruct IHHlts; try reflexivity; subst; eexists; simpl; auto).
    pick_fresh x.
    forwards*: H0 x.
    destruct H1 as [ [ k Q R ]]. destructA A; inverts H1.
    simpl. case_if; eexists; eauto.
Qed.