Require Import HOcore.Prelim.

(* Channels are used as De Bruijn indices, but are not bound. We do not need Autosubst to handle them. *)
Definition chan: Set := nat.

Inductive process: Type :=
| Send: chan -> process -> process
| Receive: chan -> {bind process} -> process
| Var: var -> process
| Par: process -> process -> process
| Nil: process.

(* Autosubst *)
Instance Ids_process: Ids process. derive. Defined.
Instance Rename_process: Rename process. derive. Defined.
Instance Subst_process: Subst process. derive. Defined.
Instance SubstLemmas_process : SubstLemmas process. derive. Qed.

(* 1. channel used, 2. output process, 3. source process, 4. target process *)
Inductive step_out: chan -> process -> process -> process -> Prop :=
| StOutSend (a: chan) (p: process):
    step_out a p (Send a p) Nil
| StOutParL (a: chan) (r p p' q: process):
    step_out a r p p' ->
    step_out a r (Par p q) (Par p' q)
| StOutParR (a: chan) (r q q' p: process):
    step_out a r q q' ->
    step_out a r (Par p q) (Par p q').

(* 1. channel, 2. source process, 3. target process *)
Inductive step_in: chan -> process -> process -> Prop :=
| StInReceive (a: chan) (p: process):
    step_in a (Receive a p) p
| StInParL (a: chan) (p p' q p2: process):
    step_in a p p' ->
    p2 = Par p' q.[ren (+1)] ->
    step_in a (Par p q) p2
| StInParR (a: chan) (p q q' p2: process):
    step_in a q q' ->
    p2 = Par p.[ren (+ 1)] q' ->
    step_in a (Par p q) p2.

(* 1. source process, 2. target process *)
Inductive step_tau: process -> process -> Prop :=
| StTauSynL (a: chan) (r p p' q q' p2: process):
    step_out a r p p' ->
    step_in a q q' ->
    p2 = Par p' q'.[r .: ids] ->
    step_tau (Par p q) p2
| StTauSynR (a: chan) (r p p' q q' p2: process):
    step_in a p p' ->
    step_out a r q q' ->
    p2 = Par p'.[r .: ids] q' ->
    step_tau (Par p q) p2
| StTauParL (p p' q: process):
    step_tau p p' ->
    step_tau (Par p q) (Par p' q)
| StTauParR (p q q': process):
    step_tau q q' ->
    step_tau (Par p q) (Par p q').

(* 1. variable, 2. source process, 3. target process *)
Inductive step_var_cxt: var -> process -> process -> Prop :=
| StVarCxt n:
    step_var_cxt n (Var n) (Var 0)
| StVarCxtParL n p p' q p2:
    step_var_cxt n p p' ->
    p2 = Par p' q.[ren (+1)] ->
    step_var_cxt n (Par p q) p2
| StVarCxtParR n p q q' p2:
    step_var_cxt n q q' ->
    p2 = Par p.[ren (+1)] q' ->
    step_var_cxt n (Par p q) p2.

(* 1. variable, 2. source process, 3. target process *)
Inductive step_var_rem: var -> process -> process -> Prop :=
| StVarRemRem n:
    step_var_rem n (Var n) Nil
| StVarRemParL n p p' q p2:
    step_var_rem n p p' ->
    p2 = Par p' q ->
    step_var_rem n (Par p q) p2
| StVarRemParR n p q q' p2:
    step_var_rem n q q' ->
    p2 = Par p q' ->
    step_var_rem n (Par p q) p2.

(* We need this for the proof of congruence of IO bisimilarity *)

Fixpoint instantiate' (sigma: var -> process) (p: process): process :=
  match p with
  | Send a p' => Send a (instantiate' sigma p')
  | Receive a p' => Receive a (instantiate' sigma p')
  | Var n => sigma n
  | Par p1 p2 => Par (instantiate' sigma p1) (instantiate' sigma p2)
  | Nil => Nil end.

(* Hints *)
Hint Constructors step_out
                  step_in
                  step_tau
                  step_var_cxt
                  step_var_rem.