Pi-calculus defs in Coq

pi.v

Require Import List.

(* A name defines a pair of channels.
 * We need countably many names, so we use nat.
 *
 * Denoted as "a", "b", "c", ...
 *)
Definition Name := nat.

(* A pair of channels looks like FIFO.
 * However, in π-calculus, they merely function as a synchronization point.
 * Moreover unlike FIFOs, they're symmetric.
 *
 * Denoted as "α", "β", "γ", ...
 *)
Variant Channel :=
  | ChanPos : Name -> Channel
  | ChanNeg : Name -> Channel.

Definition cneg(c: Channel) :=
  match c with
  | ChanPos a => ChanNeg a
  | ChanNeg a => ChanPos a
  end.

Lemma cneg_invol: forall c, cneg (cneg c) = c.
Proof. intros [a|a]; reflexivity. Qed.

(* A step is send/recv or a neutral computation.
 * A computation comes from a matching pair of send and recv.
 *
 * Denoted as "α", "β", "γ", ...
 * Computation is specifically denoted as "τ".
 *)
Variant Step :=
  | StepChan : Channel -> Step
  | StepComp : Step.

(* A name of recursively-defined procedure.
 * The definition is given by the corresponding environment.
 *
 * Denoted as "A", "B", "C", ...
 * With arguments, it is denoted like "A(a, b, c)".
 *)
Definition ProcName := nat.

(* A term. It comes with LTS (labeled transition system) semantics.
 *
 * Denoted as "t", "s", and alike.
 *)
Inductive Term :=
  | T0 : Term
  | Tstep : Step -> Term -> Term
  | Tpar : Term -> Term -> Term
  | Tor : Term -> Term -> Term
  | Tbind : Name -> Term -> Term
  | Tcall : ProcName -> list Name -> Term.

(* Here an environment only contains definitions of procedures.
 * An environment doesn't change time-to-time.
 *)
Record Env := {
  env_defs: list (ProcName * (list Name * Term))
}.

Definition lookup_def(e: Env) (p: ProcName) : list Name * Term :=
  match find (fun entry => Nat.eqb (fst entry) p) e.(env_defs) with
  | Some entry => snd entry
  | None => (nil, T0)
  end.

(* Simultaneous substitution of names.
   This is used in procedure call. *)
Definition substitute_name(a: Name) :=
  fix substitute_name(dict: list (Name * Name)) :=
  match dict with
  | nil => a
  | cons (from, to) dict' =>
      if Nat.eqb from a then to else substitute_name dict'
  end.

Definition bind_name_in_dict(a: Name) :=
  fix bind_name_in_dict(dict: list (Name * Name)) :=
  match dict with
  | nil => nil
  | cons (from, to) dict' =>
      if Nat.eqb from a then bind_name_in_dict dict'
      else cons (from, to) (bind_name_in_dict dict')
  end.

Fixpoint substitute(t: Term) (dict: list (Name * Name)) :=
  match t with
  | T0 => T0
  | Tstep α t' => Tstep
      match α with
      | StepChan α' => StepChan
          match α' with
          | ChanPos a => ChanPos (substitute_name a dict)
          | ChanNeg a => ChanNeg (substitute_name a dict)
          end
      | StepComp => StepComp
      end (substitute t' dict)
  | Tpar t' t'' => Tpar (substitute t' dict) (substitute t'' dict)
  | Tor t' t'' => Tor (substitute t' dict) (substitute t'' dict)
  | Tbind a t' => Tbind a (substitute t' (bind_name_in_dict a dict))
  | Tcall p args => Tcall p (map (fun a => substitute_name a dict) args)
  end.


(* Semantics of terms is given by LTS (labeled transition system).
 * That is, (→) ∈ Term × Step × Term.
 *)
Inductive Transition(e: Env) : Step -> Term -> Term -> Prop :=
  | TrStep α t : Transition e α (Tstep α t) t
  | TrParL α tl tl' tr :
      Transition e α tl tl' -> Transition e α (Tpar tl tr) (Tpar tl' tr)
  | TrParR α tl tr tr' :
      Transition e α tr tr' -> Transition e α (Tpar tl tr) (Tpar tl tr')
  | TrParC α tl tl' tr tr' :
      Transition e (StepChan α) tl tl' ->
      Transition e (StepChan (cneg α)) tr tr' ->
      Transition e StepComp (Tpar tl tr) (Tpar tl' tr')
  | TrOrL α tl tr t' :
      Transition e α tl t' -> Transition e α (Tor tl tr) t'
  | TrOrR α tl tr t' :
      Transition e α tr t' -> Transition e α (Tor tl tr) t'
  | TrBind α a t t' :
      match α with
      | StepChan (ChanPos b) => a <> b
      | StepChan (ChanNeg b) => a <> b
      | StepComp => True
      end ->
      Transition e α t t' ->
      Transition e α (Tbind a t) (Tbind a t')
  | TrCall α p args t':
      let entry := lookup_def e p in
      Transition e α (substitute (snd entry) (combine (fst entry) args)) t' ->
      Transition e α (Tcall p args) t'.


(* Bisimilarity is one of the well-behaving definitions of process equivalence.
 * They fully exploit functionality of coinduction.
 *)
CoInductive Bisimilar(e: Env) (t0 t1: Term) : Prop := {
  bisimilarity_l: forall α t0', Transition e α t0 t0' ->
    exists t1', Transition e α t1 t1' /\ Bisimilar e t0' t1';
  bisimilarity_r: forall α t1', Transition e α t1 t1' ->
    exists t0', Transition e α t0 t0' /\ Bisimilar e t0' t1'
}.



(* Inversion lemmas *)
Lemma transition_Tstep_inv: forall e α β t t',
  Transition e α (Tstep β t) t' -> α = β /\ t = t'.
Proof.
  intros e α β t t' H; inversion H; auto.
Qed.

Lemma transition_Tpar_inv: forall e α tl tr t',
  Transition e α (Tpar tl tr) t' ->
  (exists tl', Transition e α tl tl' /\ t' = Tpar tl' tr) \/
  (exists tr', Transition e α tr tr' /\ t' = Tpar tl tr') \/
  (exists β tl' tr',
    (Transition e (StepChan β) tl tl' /\
      Transition e (StepChan (cneg β)) tr tr') /\
    t' = Tpar tl' tr' /\ α = StepComp).
Proof.
  intros e α tl tr t' H; inversion H.
  - left; exists tl'; auto.
  - right; left; exists tr'; auto.
  - right; right; exists α0; exists tl'; exists tr'; auto.
Qed.

Lemma transition_Tor_inv: forall e α tl tr t',
  Transition e α (Tor tl tr) t' ->
  Transition e α tl t' \/ Transition e α tr t'.
Proof.
  intros e α tl tr t' H; inversion H.
  - left; auto.
  - right;  auto.
Qed.

Lemma transition_Tbind_inv: forall e α a t t',
  Transition e α (Tbind a t) t' ->
  exists t'', Transition e α t t'' /\ t' = Tbind a t'' /\
    match α with
    | StepChan (ChanPos b) => a <> b
    | StepChan (ChanNeg b) => a <> b
    | StepComp => True
    end.
Proof.
  intros e α a t t' H; inversion H.
  exists t'0; auto.
Qed.

Lemma transition_Tcall_inv: forall e α p args t',
  Transition e α (Tcall p args) t' ->
  let entry := lookup_def e p in
  Transition e α (substitute (snd entry) (combine (fst entry) args)) t'.
Proof.
  intros e α p args t' H; inversion H.
  auto.
Qed.


Theorem par_comm: forall e t0 t1, Bisimilar e (Tpar t0 t1) (Tpar t1 t0).
Proof.
  intros e.
  cofix CIH.
  intros t0 t1.
  split.
  - intros α t' H.
    apply transition_Tpar_inv in H.
    destruct H as [H|[H|H]].
    + destruct H as [t0' [H ->]].
      exists (Tpar t1 t0').
      split; [apply TrParR, H|].
      apply CIH.
    + destruct H as [t1' [H ->]].
      exists (Tpar t1' t0).
      split; [apply TrParL, H|].
      apply CIH.
    + destruct H as [β [t0' [t1' H]]].
      destruct H as [[Hl Hr] [-> ->]].
      exists (Tpar t1' t0').
      split.
      * apply (TrParC e (cneg β)); [apply Hr|].
        rewrite cneg_invol; apply Hl.
      * apply CIH.
  - intros α t' H.
    apply transition_Tpar_inv in H.
    destruct H as [H|[H|H]].
    + destruct H as [t1' [H ->]].
      exists (Tpar t0 t1').
      split; [apply TrParR, H|].
      apply CIH.
    + destruct H as [t0' [H ->]].
      exists (Tpar t0' t1).
      split; [apply TrParL, H|].
      apply CIH.
    + destruct H as [β [t1' [t0' H]]].
      destruct H as [[Hl Hr] [-> ->]].
      exists (Tpar t0' t1').
      split.
      * apply (TrParC e (cneg β)); [apply Hr|].
        rewrite cneg_invol; apply Hl.
      * apply CIH.
Qed.