# Strong Bisimilarity in CCS with Replication

Require Import prelim companion companion_rel ccs_rep_lang.

Implicit Types (R S : Rel exp) (s t : exp).

## Bisimiliarity

Simulation functor

Definition Fsim (R : Rel exp) (s t : exp) : Prop :=
forall a s', step s a s' -> exists2 t', step t a t' & R s' t'.

Bisimulation is the gfp of the symmetric simulation functor

Definition Fbisim := sceil Fsim.

Notation Bisim := (t Fbisim).
Notation bisim := (Bisim bot).
Notation "'○' R" := (Fbisim (Bisim R))
(at level 100, format "○ R") : type_scope.

Notation "R '|-' s '~' t" := (Bisim R s t) (at level 60).
Notation "s ~~ t" := (bisim s t) (at level 60).

## Monotonicity of the definitions

Instance Fsim_mono : monotone Fsim.
Proof.
move=> R S le_r_s s t h a s' /h[t' st rst].
exists t' => //. exact: le_r_s.
Qed.

Instance Fbisim_mono : monotone Fbisim.
Proof. exact _. Qed.

Instance Bisim_mono : monotone Bisim.
Proof. exact _. Qed.

## Lemma 13

Lemma bisim_coind (s t : exp) :
(forall R : Rel exp, Bisim R s t -> Bisim (R) s t) ->
bisim s t.
Proof.
move=> st. apply tower_ind => [T F h i//|/=R /st]. by rewrite -t_f.
Qed.

## Fact 14

We define bisim as Bisim bot, so the first part of Fact 14 is trivial.

Lemma bisim_fold (R : Rel exp) s t : Bisim (R) s t -> Bisim R s t.
Proof. rewrite -t_f. exact: (@t_fold _ Fbisim). Qed.

Lemma bisim_unfold s t : bisim s t -> Fbisim bisim s t.
Proof. by rewrite -nu_t nu_fp. Qed.

Lemma bisim_bisim R s t : bisim s t -> Bisim R s t.
Proof. apply: (t_monotone Fbisim). exact: botE. Qed.

Lemma r_bisim (R : Rel exp) s t : R s t -> Bisim R s t.
Proof. exact: (t_inc Fbisim). Qed.

Lemma bisim_left R s t : Bisim (R) s t -> Fsim (Bisim R) s t.
Proof. by rewrite -t_f => -[]. Qed.

## Lemma 15

Relative bisimilarity is an equivalence relation.

Instance bisim_rewrite (R : Rel exp) : RewriteRelation (Bisim R).

Instance bisim_refl (R : Rel exp) : Reflexive (Bisim R).
Proof.
apply: t_refl. apply: freflexive_sceil => {R} R rxx s a t st. by exists t.
Qed.

Instance bisim_sym (R : Rel exp) : Symmetric (Bisim R).
Proof. exact: symmetric_t_sceil. Qed.

Instance bisim_trans (R : Rel exp) : Transitive (Bisim R).
Proof.
apply: t_trans. apply: ftransitive_sceil => {R} R tR s t u rst rtu.
move=> a s' /rst[t'/rtu[u' st rtu'] rst']. exists u' => //.
exact: tR rst' rtu'.
Qed.

Instance rbisim_subrel R : subrelation bisim (Bisim R).
Proof. exact: bisim_bisim. Qed.

Instance rbisim_fold_subrel R : subrelation (Bisim (R)) (Bisim R).
Proof. exact: bisim_fold. Qed.

## Compatibility Lemmas

### Specializing the upto lemma for bisimilarity.

Lemma bisim_upto g :
monotone g -> fsymmetric g ->
(forall R, g (Bisim R) <= Bisim R -> g (Bisim (R)) <= Fsim (Bisim R)) ->
forall R, g (Bisim R) <= Bisim R.
Proof.
move=> h1 h2 h3. apply: upto => /= R /h3 h4.
apply: sceil_pre h2 _. by rewrite t_f.
Qed.

### Lemma 17: Compatibility with Action Prefixes

Inductive cAct (R : Rel exp) : Rel exp :=
| CAct a s t : R s t -> cAct R (Act a s) (Act a t).

Lemma cAct_step R :
cAct R <= Fbisim R.
Proof.
move=> s t [{s t}a s t rst]. split; rewrite/Fsim; apply step_act_inv;
eexists; by [exact: step_act|exact: rst].
Qed.

Lemma upto_act_s R a s t :
Bisim R s t -> Bisim (R) (Act a s) (Act a t).
Proof.
move=> h. rewrite -t_f. apply: cAct_step. by constructor.
Qed.

Lemma upto_act R a s t :
Bisim R s t -> Bisim R (Act a s) (Act a t).
Proof.
move=> h. apply: bisim_fold. exact: upto_act_s.
Qed.

### Lemma 18: Compatibility with Choice

Inductive cSum (R : Rel exp) : Rel exp :=
| CSum s1 s2 t1 t2 : R s1 t1 -> R s2 t2 -> cSum R (Sum s1 s2) (Sum t1 t2).

Instance cSum_mono : monotone cSum.
Proof. move=> R S le_r_s s t h. inv h. apply: CSum; exact: le_r_s. Qed.

Lemma cSum_symmetric : fsymmetric cSum.
Proof. move=> R Rh ??[]; eauto using cSum. Qed.

Lemma upto_sum' R :
cSum (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R ch]. exact: cSum_symmetric.
move=> s t [{s t}s1 s2 t1 t2 /bisim_left h1 /bisim_left h2] a.
apply step_sum_inv => [u/h1|u/h2] [t' st r];
exists t'; eauto using step_suml, step_sumr.
Qed.

Lemma upto_sum R s1 s2 t1 t2 :
Bisim R s1 s2 -> Bisim R t1 t2 -> Bisim R (Sum s1 t1) (Sum s2 t2).
Proof. move=> h1 h2. apply: upto_sum'. by constructor. Qed.

### Lemma 19: Compatibility with Parallel Composition

Inductive cPar (R : Rel exp) : Rel exp :=
| CPar s1 s2 t1 t2 : R s1 t1 -> R s2 t2 -> cPar R (Par s1 s2) (Par t1 t2).

Instance cPar_mono : monotone cPar.
Proof. move=> R S le_r_s s t h. inv h. apply: CPar; exact: le_r_s. Qed.

Lemma cPar_symmetric : fsymmetric cPar.
Proof. move=> R Rh ??[]; eauto using cPar. Qed.

Lemma upto_par' R :
cPar (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R h]. exact: cPar_symmetric.
move=> s t [{s t}s1 s2 t1 t2 h1 h2].
apply: step_par_inv => [a u st|a u st|a u v ob].
- move: (st) => /(bisim_left h1)[u' st' ru]. exists (Par u' t2).
exact: step_parl. apply: h. constructor. exact: ru. exact: bisim_fold.
- move: (st) => /(bisim_left h2)[u' st' ru]. exists (Par t1 u').
exact: step_parr. apply: h. constructor. exact: bisim_fold. exact: ru.
- move=> /(bisim_left h1)[u1 st1 r1] /(bisim_left h2)[u2 st2 r2].
exists (Par u1 u2). exact: step_comm st1 st2. apply: h. by constructor.
Qed.

Lemma upto_par R s1 s2 t1 t2 :
Bisim R s1 s2 -> Bisim R t1 t2 -> Bisim R (Par s1 t1) (Par s2 t2).
Proof.
move=> h1 h2. apply: upto_par'. by constructor.
Qed.

### Lemma 20: Compatibility with Restriction

Inductive cNew (R : Rel exp) : Rel exp :=
| CNew n s t : R s t -> cNew R (New n s) (New n t).

Instance cNew_mono : monotone cNew.
Proof. move=> R S/(_ _ _)???[]; firstorder using cNew. Qed.

Lemma cNew_symmetric : fsymmetric cNew.
Proof. move=>????[]; eauto using cNew. Qed.

Lemma upto_new' R :
cNew (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R ch]. exact: cNew_symmetric.
move=> s t [{s t}n s1 s2 /bisim_left h].
apply: step_new_inv => b t1 g /h[t2 st rst].
exists (New n t2). exact: step_new. exact: ch.
Qed.

Lemma upto_new R n s t :
Bisim R s t -> Bisim R (New n s) (New n t).
Proof.
move=> h. apply: upto_new'. by constructor.
Qed.

### Lemma 21: Compatibility with Repetition

Inductive cRep (R : Rel exp) : Rel exp :=
| CRep s t : R s t -> cRep R (Rep s) (Rep t).

Instance cRep_mono : monotone cRep.
Proof. move=> R S le_r_s s t h. inv h. apply: CRep. exact: le_r_s. Qed.

Lemma cRep_symmetric : fsymmetric cRep.
Proof. move=>????[]; eauto using cRep. Qed.

Lemma upto_rep' R :
cRep (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R ch]. exact: cRep_symmetric.
move=> s t [{s t}s t rst]. apply: step_rep_ind.
- move=> a s' st1 [t' st2 rst']. exists (Par t' t).
apply: step_rep. exact: step_parl.
apply: upto_par. exact: rst'. exact: bisim_fold.
- move=> a s' /(bisim_left rst)[t' st rst']. exists (Par (Rep t) t').
apply: step_rep. exact: step_parr. apply: upto_par.
apply: ch. constructor. exact: bisim_fold. exact: rst'.
- move=> a u1 u2 ob st1 [v1 st2 ruv1] /(bisim_left rst)[v2 st3 ruv2].
exists (Par v1 v2). apply: step_rep. exact: step_comm ob st2 st3.
exact: upto_par.
Qed.

Lemma upto_rep R s t :
Bisim R s t -> Bisim R (Rep s) (Rep t).
Proof.
move=> h. apply: upto_rep'. by constructor.
Qed.

## Theorem 22: Relative Bisimilarity is a Congruence

Instance bisim_equiv R : Equivalence (Bisim R).
Proof. constructor; exact _. Qed.

Instance act_proper R : Proper (eq ==> Bisim R ==> Bisim (R)) Act.
Proof. move=> a b ->. exact: upto_act_s. Qed.

Instance act_proper_l R : Proper (eq ==> Bisim R ==> Bisim R) Act.
Proof. move=> a b -> s1 s2 rs. rewrite rs. reflexivity. Qed.

Instance sum_proper R : Proper (Bisim R ==> Bisim R ==> Bisim R) Sum.
Proof. move=> s1 s2 rs t1 t2 rt. exact: upto_sum. Qed.

Instance par_proper R : Proper (Bisim R ==> Bisim R ==> Bisim R) Par.
Proof. move=> s1 s2 rs t1 t2 rt. exact: upto_par. Qed.

Instance new_proper R : Proper (eq ==> Bisim R ==> Bisim R) New.
Proof. move=> m n ->. exact: upto_new. Qed.

Instance rep_proper R : Proper (Bisim R ==> Bisim R) Rep.
Proof. exact: upto_rep. Qed.

## Unique Solutions

Inductive ctx :=
| THole
| TExp (s : exp)
| TAct (a : act) (c : ctx)
| TSum (c1 c2 : ctx)
| TPar (c1 c2 : ctx)
| TRep (c : ctx)
| TNew (n : nat) (c : ctx).

Inductive gctx :=
| GExp (s : exp)
| GAct (a : act) (c : ctx)
| GSum (c1 c2 : gctx)
| GPar (c1 c2 : gctx)
| GRep (c : gctx)
| GNew (n : nat) (c : gctx).

Fixpoint fill (c : ctx) (s : exp) : exp :=
match c with
| THole => s
| TExp t => t
| TAct a c => Act a (fill c s)
| TSum c1 c2 => Sum (fill c1 s) (fill c2 s)
| TPar c1 c2 => Par (fill c1 s) (fill c2 s)
| TRep c => Rep (fill c s)
| TNew n c => New n (fill c s)
end.

Fixpoint gfill (c : gctx) (s : exp) : exp :=
match c with
| GExp t => t
| GAct a c => Act a (fill c s)
| GSum c1 c2 => Sum (gfill c1 s) (gfill c2 s)
| GPar c1 c2 => Par (gfill c1 s) (gfill c2 s)
| GRep c => Rep (gfill c s)
| GNew n c => New n (gfill c s)
end.

Lemma fill_proper R c s t :
Bisim R s t -> Bisim R (fill c s) (fill c t).
Proof.
move=> rst. elim: c => //=[u|a c->|c1 ch c2->|c1 ch c2->|c->|n c->];
rewrite ?ch; reflexivity.
Qed.

### Lemma 23

Lemma gfill_proper R c s t :
Bisim R s t -> Bisim (R) (gfill c s) (gfill c t).
Proof.
move=> rst. elim: c => //=[u|a c|c1 ch c2->|c1 ch c2->|c->|n c->];
rewrite ?ch; try reflexivity. apply: upto_act_s. exact: fill_proper.
Qed.

### Theorem 24

Theorem unique_solutions c s t :
bisim s (gfill c s) ->
bisim t (gfill c t) ->
bisim s t.
Proof.
move=> h1 h2. apply: bisim_coind => R ch. etransitivity.
apply: bisim_bisim. exact: h1. etransitivity. exact: gfill_proper.
apply: bisim_bisim. by symmetry.
Qed.

## Bisimilarity Example

Lemma parC R s t :
Bisim R (Par s t) (Par t s).
Proof.
move: s t. apply tower_ind => {R} /= [T F ch s t i|R ch]; first by exact: ch.
wlog suff: / forall s t, Fsim (Bisim R) (Par s t) (Par t s).
move=> h. split. exact: h. rewrite flip_symmetric. exact: h. exact: bisim_sym.
move=> s t. apply: step_par_inv.
- move=> a u st. exists (Par t u). exact: step_parr. exact: ch.
- move=> a u st. exists (Par u s). exact: step_parl. exact: ch.
- move=> a u v ob st1 st2. exists (Par v u). case: a ob st1 st2 => //=a ob st1 st2;
exact: step_comm st2 st1. exact: ch.
Qed.

Section Example.
Variable A B : exp.
Let ai : act := ActRecv 0.
Let ao : act := dual (ai).
Hypothesis A_def : bisim A (Par (Act ao (Rep A)) (Act ai B)).
Hypothesis B_def : bisim B (Par (Act ao (Rep B)) (Act ai A)).

Lemma AB :
bisim A B.
Proof.
apply: bisim_coind => R ch.
etransitivity. apply: bisim_bisim. exact: A_def.
etransitivity; last first. apply: bisim_bisim. symmetry. exact: B_def.
apply: upto_par; apply: upto_act_s. exact: upto_rep. by symmetry.
Qed.
End Example.