# Bisimilarity in CCS with Recursive Processes

Require Import prelim companion companion_rel companion_mu fin ccs_mu_syn ccs_mu_sem.

Implicit Types (R S : Rel cexp).

(Closed) Simulation functor

Definition Fsim (R : Rel cexp) (s t : cexp) : 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).

## Open Bisimulation

Definition OBisim {n} (R : Rel cexp) : Rel (exp n) :=
fun s t => forall f : 'I_n -> cexp, Bisim R s.[f] t.[f].

Notation obisim := (@OBisim _ bot).

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

Lemma obisim_coind n (s t : exp n) :
(forall R, OBisim R s t -> OBisim (R) s t) ->
obisim s t.
Proof.
move=> st. rewrite/OBisim. apply tower_ind. move=> T F ch f i. exact: ch.
move=> /= R ch f. rewrite t_f. apply: st. exact: ch.
Qed.

## Boilerplate

Lemma bisim_fold (R : Rel cexp) 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 bisim_left R s t : Bisim (R) s t -> Fsim (Bisim R) s t.
Proof. by rewrite -t_f => -[]. Qed.

## (Open) Relative Bisimilarity is an Equivalence Relation

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

Instance bisim_refl (R : Rel cexp) : 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 cexp) : Symmetric (Bisim R).
Proof. exact: symmetric_t_sceil. Qed.

Instance bisim_trans (R : Rel cexp) : 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 obisim_refl n (R : Rel cexp) : Reflexive (@OBisim n R).
Proof. move=> s f /=. reflexivity. Qed.

Instance obisim_sym n (R : Rel cexp) : Symmetric (@OBisim n R).
Proof. move=> s t h f /=. symmetry. exact: h. Qed.

Instance obisim_trans n (R : Rel cexp) : Transitive (@OBisim n R).
Proof.
move=> s t u h1 h2 f /=. transitivity (t.[f]).
exact: h1. exact: h2.
Qed.

## Compatibility with Act/Sum/Par/New

This is copied from ccs_rep_bisim.v

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

### Compatibility with Action Prefixes

Inductive cAct R : Rel cexp :=
| 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.

### Compatibility with Choice

Inductive cSum R : Rel cexp :=
| 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.

### Compatibility with Parallel Composition

Inductive cPar R : Rel cexp :=
| 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.

### Compatibility with Restriction

Inductive cNew R : Rel cexp :=
| 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.

## Compatibility with Fixed Points and Instantiation

We use the dual companion construction to simplify the proof from the paper.

Inductive cFix (R : Rel cexp) : Rel cexp :=
| CFix (s1 s2 : exp 1) :
(forall u : cexp, R s1.[u/] s2.[u/]) ->
cFix R (Fix s1) (Fix s2).

Inductive cSubst (R : Rel cexp) : Rel cexp :=
| CSubst n (f g : 'I_n -> cexp) (s : exp n) :
(forall x, R (f x) (g x)) -> cSubst R s.[f] s.[g].

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

Lemma cFix_symmetric : fsymmetric cFix.
Proof. move=>????[]; eauto using cFix. Qed.

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

Lemma cSubst_symmetric : fsymmetric cSubst.
Proof. move=>????[]; eauto using cSubst. Qed.

Lemma step_subst_sim R n (f g : 'I_n -> cexp) :
(forall s, Bisim R s.[f] s.[g]) ->
(forall S : lts,
(forall s a t, Step S s.[f] a t -> exists2 t', step s.[g] a t' & Bisim R t t') ->
forall x a t, Fstep (Step S) (f x) a t -> exists2 t', step (g x) a t' & Bisim R t t') ->
forall s a t, step s.[f] a t -> exists2 t', step s.[g] a t' & Bisim R t t'.
Proof.
move=> ch H. pattern step at 1. apply: ind => /=.
move=> T F ih s a s' [i st]. exact: (ih i).
move=> S ih [b s|s1 s2|s1 s2|b s|s|x] a s' st.
- inv st. eexists; [apply: step_act|exact: ch].
- inv st.
+ move: H4 => /ih[s1' st bs]. eexists; [exact: step_suml st|exact: bs].
+ move: H4 => /ih[s2' st bs]. eexists; [exact: step_sumr st|exact: bs].
- inv st.
+ move: H4 => /ih[t'' p q]. eexists. apply: step_parl. exact: p. exact: upto_par.
+ move: H4 => /ih[t'' p q]. eexists. apply: step_parr. exact: p. exact: upto_par.
+ move: H3 => /ih[t1' p1 q1]. move: H6 => /ih[t2' p2 q2].
exists (Par t1' t2'). exact: step_comm p1 p2. exact: upto_par.
- inv st. move: H5 => /ih[s' st bs]. eexists. apply: step_new => //. exact: st.
apply: upto_new. exact: bs.
- inv st. move: H1. rewrite (@subst_up _ _ _ (Fix s)) => /ih[t' st bs].
eexists; [|exact: bs]. apply: step_fix. rewrite (@subst_up _ _ _ (Fix s)). exact: st.
- move: st => /=. apply: H. exact: ih.
Qed.

Lemma upto_inst' R :
cSubst (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R ch]. exact: cSubst_symmetric.
move=> s t [{s t}n f g s h_subst] a s' st.
(* Coinductive hypothesis *)
have {ch}ch: forall s : exp n, Bisim R s.[f] s.[g].
move=> t. apply: ch. constructor=> x. apply: bisim_fold. exact: h_subst.
(* Induction on the step relation *)
apply: step_subst_sim ch _ s a s' st. move=> S _ x a t.
move=> /ffstep_step/(bisim_left (h_subst x)). exact.
Qed.

Lemma upto_inst_w R n (s : exp n) (f g : 'I_n -> cexp) :
(forall x, Bisim R (f x) (g x)) -> Bisim R s.[f] s.[g].
Proof.
move=> h. apply: upto_inst'. by constructor.
Qed.

Lemma upto_beta R (s t : cexp) u :
Bisim R s t -> Bisim R u.[s/] u.[t/].
Proof.
move=> bs. apply: upto_inst_w.
apply: ord_inv => [|x]; rewrite ?asimpl //. reflexivity.
Qed.

Lemma upto_fix' R :
cFix (Bisim R) <= Bisim R.
Proof.
apply: bisim_upto R => [|R ch]. exact: cFix_symmetric.
move=> s t [{s t}s t h] a s' /step_fix_inv st.
case: (step_subst_sim (R := R) (g := Fix t .: ids) _ _ st).
- move=> {a s' st} u. apply: upto_beta. apply: ch. constructor => v. apply: bisim_fold. exact: h.
- move=> {a s' st} S ih. apply: ord_inv => [|[]//] a s'.
rewrite !scons0 => st. inv st. move: H0 => /ih[t' st bs].
move: st => /(bisim_left (h (Fix t)))[t'' st' bs'].
exists t''. exact: step_fix. by transitivity t'.
- move=> s'' st' bs. move: st' => /(bisim_left (h (Fix t)))[t'' st'' bs''].
exists t''. exact: step_fix. by transitivity s''.
Qed.

Lemma upto_fix R (s t : exp 1) :
(forall u, Bisim R s.[u/] t.[u/]) -> Bisim R (Fix s) (Fix t).
Proof.
move=> h. apply: upto_fix'. by constructor.
Qed.

## Theorem 28: Open Relative Bisimilarity is a Congruence

Instance bisim_equiv n R : Equivalence (@OBisim n R).
Proof. constructor; exact _. Qed.

Instance act_proper n R : Proper (eq ==> OBisim R ==> OBisim (R)) (@Act n).
Proof. move=> a b -> s t rst f /=. exact: upto_act_s. Qed.

Instance act_proper_l n R : Proper (eq ==> OBisim R ==> OBisim R) (@Act n).
Proof. move=> a b -> s1 s2 rs f /=. exact: upto_act. Qed.

Instance sum_proper n R : Proper (OBisim R ==> OBisim R ==> OBisim R) (@Sum n).
Proof. move=> s1 s2 rs t1 t2 rt f /=. exact: upto_sum. Qed.

Instance par_proper n R : Proper (OBisim R ==> OBisim R ==> OBisim R) (@Par n).
Proof. move=> s1 s2 rs t1 t2 rt f /=. exact: upto_par. Qed.

Instance new_proper n R : Proper (eq ==> OBisim R ==> OBisim R) (@New n).
Proof. move=> a b -> s t rst f /=. exact: upto_new. Qed.

Instance fix_proper n R : Proper (OBisim R ==> OBisim R) (@Fix n).
Proof.
move=> s t rst f /=. apply: upto_fix => u. rewrite !asimpl. exact: rst.
Qed.

## Theorem 29: Open Relative Bisimilarity is Compatible with Instantiation

Theorem upto_inst m n R (f g : 'I_m -> exp n) (s t : exp m) :
(forall x, OBisim R (f x) (g x)) -> OBisim R s t -> OBisim R s.[f] t.[g].
Proof.
move=> h1 h2 k /=. rewrite !asimpl. etransitivity. apply: h2.
apply: upto_inst'. constructor => /= x. exact: h1.
Qed.