# Syntax of CCS with Recursive Processes

Require Import base data.fintype.

## 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 : fin n).

## Instantiation

Fixpoint rmap {n m} (f : ren n 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 (up f) s)
| Var x => Var (f x)
end.

Definition upi {n m} (f : fin n -> exp m) : fin n.+1 -> exp m.+1 :=
Var bound .: f >> rmap shift.

Fixpoint rbind {n m} (f : fin 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 (upi f) s)
| Var x => f x
end.

Definition rcomp {n m k} (f : fin n -> exp m) (g : fin m -> exp k) : fin n -> exp k :=
f >> rbind g.

Definition ids {n} : fin 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 : fin n -> exp m) x :
(ids x).[f] = f x.
Proof. by []. Qed.

Lemma up_id n :
upi (@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 : fin n -> fin m) :
ren (up f) = upi (ren f).
Proof. by rewrite/up/upi; fsimpl. Qed.

Lemma map_subst n m (f : fin n -> fin 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 : fin n -> exp m) :
upi f = Var bound .: (f >>> ren shift).
Proof.
rewrite/upi/=. f_equal; fext=> x/=. by rewrite map_subst.
Qed.

## Associativity

Lemma up_upr n m k (f : fin n -> fin m) (g : fin m -> exp k) :
up f >> upi g = upi (f >> g).
Proof. by fsimpl. Qed.

Lemma rbind_rmap_comp n m k (f : fin n -> fin m) (g : fin m -> exp k) (s : exp n) :
(rmap f s).[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_upr.
Qed.

Lemma rmap_comp n m k (f : fin n -> fin m) (g : fin m -> fin k) (s : exp n) :
rmap g (rmap f s) = rmap (f >> g) s.
Proof. by rewrite map_subst rbind_rmap_comp map_subst. Qed.

Lemma upr_up n m k (f : fin n -> exp m) (g : fin m -> fin k) :
upi f >> rmap (up g) = upi (f >> rmap g).
Proof.
fext=> /=-[i|]//=. by rewrite !rmap_comp.
Qed.

Lemma rmap_rbind_comp n m k (f : fin n -> exp m) (g : fin m -> fin k) (s : exp n) :
rmap g (rbind f s) = rbind (f >> rmap g) 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 : fin n -> exp m) (g : fin m -> exp k) :
upi f >>> upi g = upi (f >>> g).
Proof.
fext=>/=-[i|]//=. by rewrite/rcomp/= rbind_rmap_comp rmap_rbind_comp.
Qed.

Lemma rbindA n m k (f : fin n -> exp m) (g : fin 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 : fin n -> exp m) (g : fin m -> exp k) :
(s .: f) >>> g = s.[g] .: (f >>> g).
Proof. rewrite/rcomp. by fsimpl. Qed.

Lemma shift_scons n m (s : exp m) (f : fin n -> exp m) :
ren shift >>> (s .: f) = f.
Proof. by []. Qed.

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

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

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

Definition asimpl := (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 : fin n -> exp m) (s : exp n.+1) (t : exp m) :
s.[upi f].[t/] = s.[t .: f].
Proof. by rewrite !asimpl. Qed.

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