Companion.ccs_rep_lang

Syntax and Semantics for CCS with Replication


Require Import prelim companion companion_mu.

Syntax

Note that exp is defined coinductively. This avoids the explicit environment in the reduction relation.

Inductive act :=
| ActSend (n : nat)
| ActRecv (n : nat)
| ActTau.

CoInductive exp :=
| Null
| Act (a : act) (s : exp)
| Sum (s t : exp)
| Par (s t : exp)
| Rep (s : exp)
| New (n : nat) (s : exp).

Definition lts := exp -> act -> exp -> Prop.

Definition observable (a : act) : bool :=
  if a isn't ActTau then true else false.

Definition dual (a : act) : act :=
  match a with
  | ActSend n => ActRecv n
  | ActRecv n => ActSend n
  | ActTau => ActTau
  end.

Definition guard (n : nat) (a : act) : bool :=
  match a with
  | ActSend m | ActRecv m => n != m
  | ActTau => true
  end.

Reduction Relation as an Explicit Fixed Point


Inductive Fstep (R : lts) : lts :=
| Fstep_act a s : Fstep R (Act a s) a s
| Fstep_suml a s t u :
    R s a t -> Fstep R (Sum s u) a t
| Fstep_sumr a s t u :
    R t a u -> Fstep R (Sum s t) a u
| Fstep_parl a s t u :
    R s a t -> Fstep R (Par s u) a (Par t u)
| Fstep_parr a s t u :
    R t a u -> Fstep R (Par s t) a (Par s u)
| Fstep_comm a s t u v :
    observable a -> R s a t -> R u (dual a) v -> Fstep R (Par s u) ActTau (Par t v)
| Fstep_rep a s t :
    R (Par (Rep s) s) a t -> Fstep R (Rep s) a t
| Fstep_restrict n a s t :
    guard n a -> R s a t -> Fstep R (New n s) a (New n t).

Notation Step := (l Fstep).
Notation step := (Step top).

Boilerplate Lemmas for Reduction


Instance Fstep_mono : monotone Fstep.
Proof.
  move=> R S /(_ _ _ _ _)le_r_s s a t h. inv h; eauto using Fstep.
Qed.

Lemma step_unfold (R : lts) s a t : Step R s a t -> Fstep (Step R) s a t.
Proof. exact: (@l_unfold _ Fstep). Qed.

Lemma step_fold s a t : Fstep step s a t -> step s a t.
Proof. by rewrite -mu_l mu_fp. Qed.

Lemma fstep_step R a s t : Step R s a t -> step s a t.
Proof. apply: (l_monotone Fstep). exact: topI. Qed.

Constructors


Lemma step_act a s : step (Act a s) a s.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_suml a s t u : step s a t -> step (Sum s u) a t.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_sumr a s t u : step t a u -> step (Sum s t) a u.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_parl a s t u : step s a t -> step (Par s u) a (Par t u).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_parr a s t u : step t a u -> step (Par s t) a (Par s u).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_comm a s t u v :
  observable a ->
  step s a t -> step u (dual a) v -> step (Par s u) ActTau (Par t v).
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_rep a s t : step (Par (Rep s) s) a t -> step (Rep s) a t.
Proof. eauto using step_fold, Fstep. Qed.

Lemma step_new n a s t :
  guard n a -> step s a t -> step (New n s) a (New n t).
Proof. eauto using step_fold, Fstep. Qed.

Inversions


Lemma step_act_inv (R : lts) (P : act -> exp -> Prop) a s :
  P a s -> forall b t, Step R (Act a s) b t -> P b t.
Proof. move=> p b t /step_unfold st. by inv st. Qed.

Lemma step_sum_inv (R : lts) (P : exp -> Prop) a s t :
  (forall u, Step R s a u -> P u) ->
  (forall u, Step R t a u -> P u) ->
  forall u, Step R (Sum s t) a u -> P u.
Proof.
  move=> p1 p2 u /step_unfold st. inv st; by [exact: p1|exact: p2].
Qed.

Lemma step_par_inv (R : lts) (P : act -> exp -> Prop) s t :
  (forall a u, Step R s a u -> P a (Par u t)) ->
  (forall a u, Step R t a u -> P a (Par s u)) ->
  (forall a u v, observable a -> Step R s a u -> Step R t (dual a) v -> P ActTau (Par u v)) ->
  (forall a u, Step R (Par s t) a u -> P a u).
Proof.
  move=> p1 p2 p3 a u /step_unfold st. inv st; eauto.
Qed.

Lemma step_rep_inv (R : lts) s a t :
  Step R (Rep s) a t -> Step R (Par (Rep s) s) a t.
Proof.
  move=> /step_unfold st. by inv st.
Qed.

Lemma step_new_inv (R : lts) (P : act -> exp -> Prop) n s :
  (forall a t, guard n a -> Step R s a t -> P a (New n t)) ->
  forall a t, Step R (New n s) a t -> P a t.
Proof.
  move=> p a t /step_unfold st. inv st; eauto.
Qed.

Induction principle for repetition

This is a special case of dual tower induction

Lemma step_rep_ind (s : exp) (R : act -> exp -> Prop) :
  (forall a t, step (Rep s) a t -> R a t -> R a (Par t s)) ->
  (forall a t, step s a t -> R a (Par (Rep s) t)) ->
  (forall a t u,
      observable a ->
      step (Rep s) a t -> R a t ->
      step s (dual a) u ->
      R ActTau (Par t u)) ->
  (forall a t, step (Rep s) a t -> R a t).
Proof.
  move=> h1 h2 h3. apply ind => /= [T F ih a t []|S ih a t st];
    eauto; try exact _. inv st. move: H0.
  apply: step_par_inv a t => [a u st|a u st|a u v ob st1 st2].
  - apply: h1. exact: fstep_step st. exact: ih.
  - apply: h2. exact: fstep_step st.
  - apply: h3 ob _ _ _. exact: fstep_step st1. exact: ih. exact: fstep_step st2.
Qed.