Bisimilarity in CCS with Recursive Processes

Require Import base ord tower.tarski tower.tower data.fintype ccs.syntax ccs.semantics.

Implicit Types (R S : Rel cexp).

Definition 8.1

(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 flip {X} (R : Rel X) : Rel X :=
fun x y => R y x.

Definition sceil {X} (F : Rel X -> Rel X) (R : Rel X) : Rel X :=
fun x y => F R x y /\ F (flip R) y x.

Lemma flip_symmetric {X} (R : Rel X) : Symmetric R -> flip R = R.
Proof. move=> h. apply: le_eq; hnf=> x; hnf=> y; exact: h. Qed.

Instance sceil_mono {X} (F : Rel X -> Rel X) {fP : monotone F} :
monotone (sceil F).
Proof.
move=> /= R S le_r_s x y [h1 h2]. split. exact: fP h1.
apply: fP y x {h1} h2 => y x /=. exact: le_r_s.
Qed.

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

Lemma 8.2

Lemma bisim_coind (s t : cexp) :
(forall R, Bisim R s t -> Bisim (R) s t) ->
bisim s t.
Proof.
move=> st. apply tower_induction. move=> T F ih. exact: ih.
move=> /= R ch. rewrite t_f. apply: st. exact: ch.
Qed.

Definition 8.3

Definition OBisim {n} (R : Rel cexp) : Rel (exp n) :=
fun s t => forall f : fin 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.

Fact 8.4

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

Lemma bisim_unfold s t : bisim s t -> Fbisim bisim s t.
Proof. by rewrite t_gfp gfpE. Qed.

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

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

Lemma 8.5

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_induction. move=> T F ch f i. exact: ch.
move=> /= R ch f. rewrite t_f. apply: st. exact: ch.
Qed.

Lemma 8.6: (Open) Relative Bisimilarity is an Equivalence Relation

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

Global Instance bisim_equiv R : Equivalence (Bisim R).
Proof.
apply tower_induction.
- move=> I/= F ih. constructor. move=> s i. reflexivity.
move=> s t h i. symmetry. exact: h. move=> s t u h1 h2 i.
by transitivity t.
- move=> /= {R}R equiv_R. constructor.
+ move=> s. suff: Fsim (Bisim R) s s. split=> //. by rewrite flip_symmetric.
move=> a t st. exists t => //. reflexivity.
+ move=> s t [h1 h2]. split=> a u st. case: (h2 a u) => // v st' h.
exists v => //. symmetry. exact: h. case: (h1 a u) => // v st' h.
exists v => //. unfold flip. symmetry. exact: h.
+ move=> s t u [hst hts] [htu hut]. split=> a v st.
case: (hst a v st) => v' /htu[v'' st' /=h1] h2. exists v'' => //. by etransitivity.
case: (hut a v st) => v' /hts[v'' st' /=h1] h2. exists v'' => //.
unfold flip in *. by etransitivity.
Qed.

Global Instance obisim_equiv n R : Equivalence (@OBisim n R).
Proof.
constructor. move=> s f. reflexivity. move=> s t h f. symmetry. exact: h.
move=> s t u h1 h2 f. by transitivity t.[f].
Qed.

Lemma 8.7

Lemma obisim_unfold_mu n (P : exp n.+1) :
obisim (Fix P) P.[Fix P/].
Proof.
move=> f /=. rewrite !asimpl. apply: bisim_fold. rewrite -t_f. split.
- move=> a s st. inv st. move: H0. rewrite !asimpl/=upE => st.
exists s => //. reflexivity.
- move=> a s /=. rewrite upE => st. exists s; last first. unfold flip. reflexivity.
constructor. by rewrite !asimpl/=.
Qed.

Congruence properties of open relative bisimilarity

Class CcsCongruence (R : Rel cexp) :=
{ ccs_congruence_sum :> Proper (R ==> R ==> R) (@Sum 0)
; ccs_congruence_par :> Proper (R ==> R ==> R) (@Par 0)
; ccs_congruence_new :> forall a, Proper (R ==> R) (@New 0 a)
; ccs_congruence_fix : forall (P Q : exp 1), (forall u : cexp, R P.[u/] Q.[u/]) -> R (Fix P) (Fix Q)
}.

Lemma 8.8

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. wlog suff: s t h / Fsim (Bisim R) (Act a s) (Act a t).
move=> h'. split; [|rewrite flip_symmetric]; apply: h' => //. by symmetry.

apply: step_act_inv. exists t => //. by constructor.
Qed.

Lemma upto_act_s_open n R a s t :
@OBisim n R s t -> OBisim (R) (Act a s) (Act a t).
Proof.
move=> rst f /=. apply: upto_act_s. exact: rst.
Qed.

Global Instance upto_act R a : Proper (Bisim R ==> Bisim R) (Act a).
Proof.
move=> s t rst. apply: bisim_fold. exact: upto_act_s.
Qed.

Global Instance upto_act_open n R a : Proper (@OBisim n R ==> OBisim R) (Act a).
Proof.
move=> s t rst f /=. apply: upto_act. exact: rst.
Qed.

Lemma 8.9

Global Instance upto_sum_o R :
Proper (Bisim (R) ==> Bisim (R) ==> Bisim (R)) (@Sum 0).
Proof.
move=> s1 s2 rs t1 t2 rt. rewrite -t_f.
wlog suff h: s1 s2 t1 t2 rs rt / Fsim (Bisim R) (Sum s1 t1) (Sum s2 t2).
split; [|rewrite flip_symmetric]; apply: h=> //; by symmetry.

apply bisim_left in rs. apply bisim_left in rt.
move=> a. apply: step_sum_inv => [u/rs[v st]|u/rt[v st]] h; exists v=> //.
by constructor. by constructor 3.
Qed.

Section CongruenceProofs.

Variable (R : Rel cexp).
Variable (congruence_properties : CcsCongruence (Bisim R)).

Lemma 8.10

Lemma upto_par_o :
Proper (Bisim (R) ==> Bisim (R) ==> Bisim (R)) (@Par 0).
Proof with eauto using @step.
move=> s1 s2 rs t1 t2 rt. rewrite -t_f.
wlog suff h: s1 s2 t1 t2 rs rt / Fsim (Bisim R) (Par s1 t1) (Par s2 t2).
split; [|rewrite flip_symmetric]; apply: h => //; by symmetry.

apply: step_par_inv.
- move=> a u /(bisim_left rs)[s2' st ru]. eexists... f_equiv=> //. exact: bisim_fold.
- move=> a u /(bisim_left rt)[t2' st ru]. eexists... f_equiv=> //. exact: bisim_fold.
- move=> a u v oa /(bisim_left rs)[s2' st ru] /(bisim_left rt)[t2' st' rv].
exists (Par s2' t2'). exact: step_comm st'. by f_equiv.
Qed.

Lemma 8.11

Lemma upto_new_o a :
Proper (Bisim (R) ==> Bisim (R)) (@New 0 a).
Proof.
move=> s t rst. rewrite -t_f. wlog suff h: s t rst / Fsim (Bisim R) (New a s) (New a t).
split; [|rewrite flip_symmetric]; apply: h => //; by symmetry.

apply: step_new_inv => b s' guarded /(bisim_left rst)[t' st rst'].
exists (New a t'). by constructor. rewrite rst'. reflexivity.
Qed.

Lemma 8.12

Lemma upto_inst' n (f g : fin n -> cexp) (s : exp n) :
(forall i, Bisim R (f i) (g i)) -> Bisim R s.[f] s.[g].
Proof.
elim: s f g => {n}[n a s ih|n s ihs t iht|n s ihs t iht|n a s ih|n s ih|n x] f g h/=.
apply: upto_act. exact: ih. f_equiv. exact: ihs. exact: iht.
f_equiv. exact: ihs. exact: iht. apply ccs_congruence_new. exact: ih.
apply ccs_congruence_fix => u. rewrite !asimpl/=. apply: ih.
move=>/=-[a|]//=. reflexivity. exact: h.
Qed.

Lemma upto_inst_beta' (s t : cexp) (u : exp 1) :
Bisim R s t -> Bisim R u.[s/] u.[t/].
Proof.
move=> h. by apply: upto_inst' => /=-[].
Qed.

Lemma 8.13

Lemma upto_fix_gen (s t u : exp 1) :
(forall v : cexp, Bisim (R) s.[v/] t.[v/]) ->
Bisim (R) u.[Fix s/] u.[Fix t/].
Proof.
move=> rst. wlog suff h: s t rst / Fsim (Bisim R) u.[Fix s/] u.[Fix t/].
rewrite -t_f; split; [|rewrite flip_symmetric]; apply: h => v //; by symmetry.
move=> a v. move eqn:u.[Fix s/] => e st. elim: st u s t eqn rst => {e a v}.
- move=> a e -[]//=; last by case=> //. move=> a' s t u [e1 e2]; subst=> h.
eexists; eauto using @step. apply: upto_inst_beta'.
apply ccs_congruence_fix => u'. exact: bisim_fold.
- move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
case: (ih s' s'' _ erefl h) => u' st' h'. eexists; by eauto using @step.
- move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
case: (ih _ _ _ erefl h) => u' st' h'. eexists; by eauto using @step.
- move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
case: (ih _ _ _ erefl h) => u' st' h'. eexists; eauto using @step.
f_equiv=> //. apply: upto_inst_beta'. apply ccs_congruence_fix => u. exact: bisim_fold.
- move=> a s t u st ih -[]//=; last by case. move=> s' t' s'' t'' [e1 e2] h; subst.
case: (ih _ _ _ erefl h) => u' st' h'. eexists; eauto using @step.
f_equiv=> //. apply: upto_inst_beta'. apply ccs_congruence_fix => v. exact: bisim_fold.
- move=> a s t u v oa st1 ih1 st2 ih2 -[]//=; last by case.
move=> s' t' s'' t'' [e1 e2] h; subst.
case: (ih1 _ _ _ erefl h) => u1 st1' h1'.
case: (ih2 _ _ _ erefl h) => u2 st2' h2'.
exists (Par u1 u2). by eauto using @step. by f_equiv.
- move=> n a s t ga st ih -[]//=; last by case.
move=> b s' t' u' [e1 e2] h; subst.
case: (ih _ _ _ erefl h) => u st' h'. eexists; eauto using @step.
by apply ccs_congruence_new.
- move=> s a u st ih -[]//=.
+ move=> s' t' u' [e] h; subst.
case/(_ _)/Wrap: (ih s'.[Fix s'/] t' _ _ h). by rewrite -subst_up.
case=> v' st' h'. eexists. econstructor. rewrite (subst_up s' (Fix s')). eassumption.
exact: h'.
+ case=> //= s' t' [e] h; subst.
case: (ih _ _ _ erefl h) => u' st' h'.
case: (bisim_left (h (Fix t')) st') => u'' st'' h''.
exists u''. by constructor. by transitivity u'.
Qed.

Lemma upto_fix_o s t :
(forall u, Bisim (R) s.[u/] t.[u/]) -> Bisim (R) (Fix s) (Fix t).
Proof.
move=> /upto_fix_gen h. exact: (h (Var bound)).
Qed.

Lemma congruence_step : CcsCongruence (Bisim (R)).
Proof.
constructor. exact: upto_sum_o. exact: upto_par_o.
exact: upto_new_o. exact: upto_fix_o.
Qed.

End CongruenceProofs.

Theorem 8.14: Open Relative Bisimilarity is a Congruence

Global Instance ccs_congruence_bisim R : CcsCongruence (Bisim R).
Proof.
apply tower_induction => {R} /=.
- move=> I F ih. constructor.
+ move=> s1 s2 rs t1 t2 rt i. f_equiv. exact: rs. exact: rt.
+ move=> s1 s2 rs t1 t2 rt i. f_equiv. exact: rs. exact: rt.
+ move=> a s1 s2 rs i. apply ccs_congruence_new. exact: rs.
+ move=> s1 s2 rs i. apply ccs_congruence_fix => u. exact: rs.
- move=> R cR. rewrite t_f. exact: congruence_step.
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 /=. f_equiv. exact: rs. exact: rt. Qed.

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

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

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

Lemma 8.15: Open Relative Bisimilarity is Compatible with Instantiation

Theorem upto_inst m n R (f g : fin 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' => /= x. exact: h1.
Qed.