HOcore.Bis

Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
HOcore.HoCore
HOcore.Multiset.

This file contains the definitions of all bisimulation functionals and basic properties about them

Definitions of bisimilarity components through their functionals

Definition s_tau: relation process -> relation process :=
  fun x p q => forall p',
                 step_tau p p' ->
               exists q',
                 step_tau q q' /\
                 x p' q'.

Definition s_ho_out: relation process -> relation process :=
  fun x p q => forall a p'' p',
                 step_out a p'' p p' ->
               exists q'' q',
                 step_out a q'' q q' /\
                 x p' q' /\
                 x p'' q''.

Definition s_ho_in: relation process -> relation process :=
  fun x p q => forall a p',
                 step_in a p p' ->
               exists q',
                 step_in a q q' /\
                 x p' q'.

Definition s_var_cxt: relation process -> relation process :=
  fun x p q => forall n p',
                 step_var_cxt n p p' ->
               exists q',
                 step_var_cxt n q q' /\
                 x p' q'.

Definition s_var_rem: relation process -> relation process :=
  fun x p q => forall n p',
                 step_var_rem n p p' ->
               exists q',
                 step_var_rem n q q' /\
                 x p' q'.

Definition s_var_multi: relation process -> relation process :=
  fun x p q => mle (count p) (count q).

Notation "'s_tau_sym'" := (symmetrize_fun s_tau).

Notation "'s_io_cxt'" := (s_ho_out /2\^ s_ho_in /2\^ s_var_cxt).
Notation "'s_io_cxt_sym'" := (symmetrize_fun s_io_cxt).

Notation "'s_io_multi'" := (s_ho_out /2\^ s_ho_in /2\^ s_var_multi).
Notation "'s_io_multi_sym'" := (symmetrize_fun s_io_multi).

Notation "'s_io_rem'" := (s_ho_out /2\^ s_ho_in /2\^ s_var_rem).
Notation "'s_io_rem_sym'" := (symmetrize_fun s_io_rem).

Monotonicity of functionals

Global Instance s_tau_mono: Mono s_tau.
Proof.
  intros p q x x' H1 H2 p' H3.
  destruct (H1 p' H3) as [q' [H4 H5]].
  exists q'. split.
  - exact H4.
  - now apply H2.
Qed.
Hint Resolve s_tau_mono.

Global Instance s_ho_out_mono: Mono s_ho_out.
Proof.
  intros p q x x' H1 H2 p' a p'' H3.
  specialize (H1 p' a p'' H3). decompose [ex and] H1; clear H1.
  repeat eexists; eauto.
Qed.

Global Instance s_ho_in_mono: Mono s_ho_in.
Proof.
  intros p q x x' H1 H2 p' a H3.
  specialize (H1 p' a H3). decompose [ex and] H1; clear H1.
  repeat eexists; eauto.
Qed.

Global Instance s_var_rem_mono: Mono s_var_rem.
  intros p q x x' H1 H2 n p' H3.
  specialize (H1 n p' H3). decompose [ex and] H1; clear H1.
  repeat eexists; eauto.
Qed.

Global Instance s_var_cxt_mono: Mono s_var_cxt.
Proof.
  intros p q x x' H1 H2 n p' H3.
  specialize (H1 n p' H3). decompose [ex and] H1; clear H1.
  repeat eexists; eauto.
Qed.

Global Instance s_var_multi_mono: Mono s_var_multi.
Proof.
  intros p q x x' H1 H2. exact H1.
Qed.

Global Instance s_io_cxt_mono: Mono s_io_cxt.
Proof.
  eapply intersect_fun_bin_preserv_mono.
Qed.

Global Instance s_io_cxt_sym_mono: Mono s_io_cxt_sym.
Proof.
  eapply intersect_fun_bin_preserv_mono.
Qed.

Preservation of the monoid (part 1): 1 <2= s(1)

Global Instance s_tau_preserv_monoid_refl:
  PreservMonoidRefl s_tau.
Proof.
  intros p q H1 p' H2. subst q.
  exists p'. now split.
Qed.

Global Instance s_ho_out_preserv_monoid_refl:
  PreservMonoidRefl s_ho_out.
Proof.
  intros p q H1. destruct H1.
  repeat intro. eauto.
Qed.

Global Instance s_ho_in_preserv_monoid_refl:
  PreservMonoidRefl s_ho_in.
Proof.
  intros p q H1. destruct H1.
  repeat intro. eauto.
Qed.

Global Instance s_var_cxt_preserv_monoid_refl:
  PreservMonoidRefl s_var_cxt.
Proof.
  intros p q H1. destruct H1.
  repeat intro. eauto.
Qed.

Global Instance s_var_multi_preserv_monoid_refl:
  PreservMonoidRefl s_var_multi.
Proof.
  intros p q H1. destruct H1. hnf.
  repeat intro. omega.
Qed.

Preservation of the monoid (part 2): s x ° s y <2= s(x ° y)

Global Instance s_tau_preserv_monoid_trans:
  PreservMonoidTrans s_tau.
Proof.
  intros x y p q [p' [H1 H2]] p1 H3.
  destruct (H1 p1 H3) as [p1' [H4 H5]].
  destruct (H2 p1' H4) as [q1 [H6 H7]].
  exists q1. split.
  - exact H6.
  - now exists p1'.
Qed.

Global Instance s_ho_out_preserv_monoid_trans:
  PreservMonoidTrans s_ho_out.
Proof.
  intros x y p q [p2 [H11 H12]] a p'' p' H2.
  destruct (H11 a p'' p' H2) as [p2'' [p2' [H31 [H32 H33]]]].
  destruct (H12 a p2'' p2' H31) as [q'' [q' [H41 [H42 H43]]]].
  repeat eexists; eauto.
Qed.

Global Instance s_ho_in_preserv_monoid_trans:
  PreservMonoidTrans s_ho_in.
Proof.
  intros x y p q [p2 [H11 H12]] a p' H2.
  destruct (H11 a p' H2) as [p2' [H31 H32]].
  destruct (H12 a p2' H31) as [q' [H41 H42]].
  eexists. split; eauto.
  eexists. eauto.
Qed.

Global Instance s_var_cxt_preserv_monoid_trans:
  PreservMonoidTrans s_var_cxt.
Proof.
  intros x y p q [p2 [H11 H12]] n p' H2.
  destruct (H11 n p' H2) as [p2' [H31 H32]].
  destruct (H12 n p2' H31) as [q' [H41 H42]].
  eexists. split; eauto.
  eexists. eauto.
Qed.

Global Instance s_var_multi_preserv_monoid_trans:
  PreservMonoidTrans s_var_multi.
Proof.
  intros x y p q [p2 [H1 H2]].
  hnf. intros n. specialize (H1 n). specialize (H2 n). omega.
Qed.