semantics.ccs.properties

Properties of Strong Bisimilarity in CCS with Recursive Processes

Corollary 8.16 is immediate since we defined obisim as OBisim ⊥

Lemma 8.17


Fixpoint weakly_guarded {n} (s : exp n) : bool :=
  match s with
  | Act _ _ => true
  | Sum s t => weakly_guarded s && weakly_guarded t
  | Par s t => weakly_guarded s && weakly_guarded t
  | New _ s => weakly_guarded s
  | Fix s => weakly_guarded s
  | Var _ => false
  end.

Lemma weakly_guarded_inst R m n (f g : fin m -> exp n) (s : exp m) :
  weakly_guarded s -> (forall x, OBisim R (f x) (g x)) -> OBisim (R) s.[f] s.[g].
Proof.
  elim: s n f g => //={m}[m a s ihs|m s ihs t iht|m s ihs t iht|m a s ihs|m s ihs] n f g.
  - move=> _ h. apply: act_proper => //. apply: upto_inst => //. reflexivity.
  - move=>/andP[/ihs h1/iht h2] h3. f_equiv. exact: h1. exact: h2.
  - move=>/andP[/ihs h1/iht h2] h3. f_equiv. exact: h1. exact: h2.
  - move=>/ihs h1 h2. f_equiv. exact: h1.
  - move=>/ihs h1 h2. f_equiv. rewrite !upE. apply: h1 => /=-[]//=; last by reflexivity.
    move=> i. rewrite/rcomp/=. apply: upto_inst=> j. reflexivity. exact: h2.
Qed.

Corollary 8.18


Corollary unique_solutions m n (f g : fin m -> exp n) (h : fin m -> exp m) :
  (forall i, weakly_guarded (h i)) ->
  (forall i, obisim (f i) (h i).[f]) ->
  (forall i, obisim (g i) (h i).[g]) ->
  (forall i, obisim (f i) (g i)).
Proof.
  move=> h1 h2 h3. rewrite/obisim. apply tower_induction.
  - move=> I F ih /= x t i. exact: ih.
  - move=> /=R h4 i ff. rewrite t_f. move: ff. change (OBisim (R) (f i) (g i)).
    transitivity (h i).[f]. move=> ff. apply bisim_bisim. apply: h2.
    transitivity (h i).[g]; last first. symmetry=> ff. apply: bisim_bisim. apply: h3.
    apply: weakly_guarded_inst. exact: h1. exact: h4.
Qed.

Corollary unique_solutions1 (s t : cexp) (u : exp 1) :
  weakly_guarded u -> s ~~ u.[s/] -> t ~~ u.[t/] -> s ~~ t.
Proof.
  move=> h1 h2 h3. case/(_ _ _ _)/Wrap: (@unique_solutions 1 0 (s.:ids) (t.:ids) (u.:null) _ _ _).
  by case. case=>//= ff. have E: ff = @Var 0 by fext. subst. rewrite !asimpl. exact: h2.
  case=>//= ff. have E: ff = @Var 0 by fext. subst. rewrite !asimpl. exact: h3.
  move=> H. move: (H bound ids) => /=. by rewrite !asimpl.
Qed.

Corollary 8.19


Inductive C (R : Rel cexp) : Rel cexp :=
| C_R s t : R s t -> C R s t
| C_bisim s t : s ~~ t -> C R s t
| C_sym s t : C R s t -> C R t s
| C_trans s t u : C R s t -> C R t u -> C R s u
| C_ctx n (f g : fin n -> cexp) (u : exp n) :
    (forall i, C R (f i) (g i)) ->
    C R u.[f] u.[g].

Lemma C_upto : C Bisim.
Proof.
  move=> R s t. hnf. elim=> {s t}.
  - move=> s t. exact: (t_inc Fbisim).
  - move=> s t. exact: bisim_bisim.
  - move=> s t _ h. by symmetry.
  - move=> s t u _ h1 _ h2. by transitivity t.
  - move=> n f g u _ h. exact: upto_inst'.
Qed.