Syntax of CCS with Recursive Processes

Require Import prelim fin.

Processes

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

Inductive exp (n : nat) :=
| Act (a : act) (s : exp n)
| Sum (s t : exp n)
| Par (s t : exp n)
| New (a : nat) (s : exp n)
| Fix (s : exp n.+1)
| Var (x : 'I_n).

Instantiation

Definition upr {n m} (f : 'I_n -> 'I_m) : 'I_n.+1 -> 'I_m.+1 := 0 .: S \o f.

Fixpoint rmap {n m} (f : 'I_n -> 'I_m) (s : exp n) : exp m :=
match s with
| Act a s => Act a (rmap f s)
| Sum s t => Sum (rmap f s) (rmap f t)
| Par s t => Par (rmap f s) (rmap f t)
| New a s => New a (rmap f s)
| Fix s => Fix (rmap (upr f) s)
| Var x => Var (f x)
end.

Definition up {n m} (f : 'I_n -> exp m) : 'I_n.+1 -> exp m.+1 :=
Var 0 .: rmap S \o f.

Fixpoint rbind {n m} (f : 'I_n -> exp m) (s : exp n) : exp m :=
match s with
| Act a s => Act a (rbind f s)
| Sum s t => Sum (rbind f s) (rbind f t)
| Par s t => Par (rbind f s) (rbind f t)
| New a s => New a (rbind f s)
| Fix s => Fix (rbind (up f) s)
| Var x => f x
end.

Definition rcomp {n m k} (f : 'I_n -> exp m) (g : 'I_m -> exp k) : 'I_n -> exp k :=
rbind g \o f.

Definition ids {n} : 'I_n -> exp n := @Var n.

Notation "f >> g" := (rcomp f g) (at level 56, left associativity).
Notation "s .[ f ]" := (rbind f s)
(at level 2, f at level 200, left associativity,
format "s .[ f ]" ).
Notation "s .[ t /]" := (s.[t .: ids])
(at level 2, t at level 200, left associativity,
format "s .[ t /]").

Notation ren f := (ids \o f).

Unit Laws

Lemma id_inst n m (f : 'I_n -> exp m) x :
(ids x).[f] = f x.
Proof. by []. Qed.

Lemma up_id n :
up (@ids n) = ids.
Proof.
by rewrite -(@scons_eta _ n ids).
Qed.

Lemma inst_id n (s : exp n) :
s.[ids] = s.
Proof.
elim: s => {n}; try (intros=> //=; congruence).
move=> n s ihs /=. by rewrite up_id ihs.
Qed.

Expressing map using bind

Lemma up_ren n m (f : 'I_n -> 'I_m) :
ren (upr f) = up (ren f).
Proof.
apply: scons_eq.
- by rewrite/=/up/upr !scons0.
- move=> i. by rewrite/=/up/upr !sconsS.
Qed.

Lemma map_subst n m (f : 'I_n -> 'I_m) (s : exp n) :
rmap f s = s.[ren f].
Proof.
elim: s m f => {n}; try (intros=> //=; congruence).
move=> n s ihs m f /=. by rewrite ihs up_ren.
Qed.

Lemma upE n m (f : 'I_n -> exp m) :
up f = Var 0 .: f >> ren S.
Proof.
apply: scons_eq.
- by rewrite/up/upr !scons0.
- move=> i. by rewrite/up/upr/= !sconsS/= map_subst.
Qed.

Associativity

Lemma up_upr n m k (f : 'I_n -> 'I_m) (g : 'I_m -> exp k) :
up g \o upr f = up (g \o f).
Proof.
apply: scons_eq => [|x]; by rewrite/up/upr/= !scons_simpl.
Qed.

Lemma rbind_rmap_comp n m k (f : 'I_n -> 'I_m) (g : 'I_m -> exp k) (s : exp n) :
(rmap f s).[g] = s.[g \o f].
Proof.
elim: s m k f g => {n}; try (intros=> //=; congruence).
move=> n s ihs m k f g /=. by rewrite ihs up_upr.
Qed.

Lemma rmap_comp n m k (f : 'I_n -> 'I_m) (g : 'I_m -> 'I_k) (s : exp n) :
rmap g (rmap f s) = rmap (g \o f) s.
Proof. by rewrite map_subst rbind_rmap_comp map_subst. Qed.

Lemma upr_up n m k (f : 'I_n -> exp m) (g : 'I_m -> 'I_k) :
rmap (upr g) \o up f = up (rmap g \o f).
Proof.
apply: scons_eq => [|x]; rewrite/up/upr/= /=!scons_simpl/=?scons_simpl//.
rewrite !rmap_comp. congr rmap. apply: fext => {x}x /=. by rewrite sconsS.
Qed.

Lemma rmap_rbind_comp n m k (f : 'I_n -> exp m) (g : 'I_m -> 'I_k) (s : exp n) :
rmap g (rbind f s) = rbind (rmap g \o f) s.
Proof.
elim: s m k f g => {n}; try (intros=> //=; congruence).
move=> n s ihs m k f g /=. by rewrite ihs upr_up.
Qed.

Lemma up_comp n m k (f : 'I_n -> exp m) (g : 'I_m -> exp k) :
up f >> up g = up (f >> g).
Proof.
apply: scons_eq => [|x].
- by rewrite/rcomp/up/= !scons0 /= scons0.
- rewrite/rcomp/up/= !sconsS /= rbind_rmap_comp rmap_rbind_comp.
congr rbind. apply: fext => j /=. by rewrite sconsS.
Qed.

Lemma rbindA n m k (f : 'I_n -> exp m) (g : 'I_m -> exp k) (s : exp n) :
s.[f].[g] = s.[f >> g].
Proof.
elim: s m k f g => {n}; try (intros=> //=; congruence).
move=> n s ihs m k f g /=. by rewrite ihs up_comp.
Qed.

The remaining equations of the sigma SP calculus

Lemma scons_scomp n m k (s : exp m) (f : 'I_n -> exp m) (g : 'I_m -> exp k) :
(s .: f) >> g = s.[g] .: (f >> g).
Proof.
apply: scons_eq => [|x].
- by rewrite/rcomp/= !scons0.
- by rewrite/rcomp/= !sconsS/=.
Qed.

Lemma shift_scons n m (s : exp m) (f : 'I_n -> exp m) :
ren S >> (s .: f) = f.
Proof.
apply: fext => x. rewrite/rcomp/=. by rewrite sconsS.
Qed.

Lemma rcompA n m k l (f : 'I_n -> exp m) (g : 'I_m -> exp k) (h : 'I_k -> exp l) :
f >> g >> h = f >> (g >> h).
Proof.
apply: fext => x. by rewrite/rcomp/= rbindA.
Qed.

Lemma rcomp_id n m (f : 'I_n -> exp m) :
f >> ids = f.
Proof.
apply: fext => x. by rewrite/rcomp/= inst_id.
Qed.

Lemma id_rcomp n m (f : 'I_n -> exp m) :
ids >> f = f.
Proof. exact: fext. Qed.

Definition asimpl := (scons_simpl, id_inst, inst_id, rbindA,
scons_scomp, shift_scons, rcompA, rcomp_id, id_rcomp, upE).

Some useful substitution lemmas

Lemma subst_extend n m (f : 'I_n -> exp m) (s : exp n.+1) (t : exp m) :
s.[up f].[t/] = s.[t .: f].
Proof. by rewrite !asimpl. Qed.

Lemma subst_up n m (s : exp n.+1) u (f : 'I_n -> exp m) :
s.[up f].[u.[f]/] = s.[u/].[f].
Proof. by rewrite !asimpl. Qed.