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