semantics.ccs.properties
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 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.
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.