Library Settings

General setting for behavioural equivalences


Require Export Functions.
Require Export Reductions.

Section Global.

  Variable A: Type.

  Section Sim.

    Variables X Y: Type.
    Variable TX: reduction_t A X.
    Variable TY: reduction_t A Y.

More or less generic evolution predicates (Definitions 1.2)
    Definition evolve_1 l R S := diagram (TX l) R (Weak TY l) S.
    Definition evolve_t R S := evolve_1 (T A) R S.
    Definition evolve_a R S := forall a, evolve_1 (L a) R S .
    Definition evolve R S := forall l, evolve_1 l R S.

(Silent) simulation, expansion (Definitions 1.3)
    Definition simulation_t R := evolve_t R R.
    Definition simulation R := evolve R R.

(Relaxed) expansion (on one side only)
    Definition expansion1 R := diagram_r TX R (EWeak TY) R.
    Definition wexpansion1 R := diagram_r TX R (REWeak TY) R.

    Variable F: function X Y.

Monotonicity: Definition 1.5
    Record monotonic: Prop := mkmon {
      mon_m:> increasing F;
      mon_t: forall R S, evolve_t R S -> incl R S -> evolve_t (F R) (F S);
      mon_a: forall R S, evolve R S -> incl R S -> evolve_a (F R) (F S)
    }.
Weak monotonicity: Definition 2.1
    Record wmonotonic: Prop := mkwmon {
      wmon_m:> increasing F;
      wmon_t: forall R, simulation_t R -> simulation_t (F R);
      wmon_a: forall R S, simulation_t R -> simulation_t S -> evolve_a R S -> incl R S -> evolve_a (F R) (F S)
    }.

Controlled relations: Definition 3.1
    Variable B: relation X.
    Record controlled: Prop := mkctrl {
      ctrl_t: forall R, evolve_t R (comp (star B) R) -> simulation_t (comp (star B) R);
      ctrl_a: forall R S, evolve_t R (comp (star B) R) -> simulation_t S ->
                          evolve_a R S -> incl R S -> evolve_a (comp (star B) R) (comp (star B) S)
    }.
Lemma 1.4 (1)
    Lemma weak_strong_t: forall R, simulation_t R -> diagram (Weak TX (T A)) R (Weak TY (T A)) R.
    Lemma weak_strong: forall R, simulation R -> diagram_r (Weak TX) R (Weak TY) R.

Lemma 1.4 (2) (splitted into several practical results)
    Lemma union2_evolve: forall l R R' S, evolve_1 l R S -> evolve_1 l R' S -> evolve_1 l (union2 R R') S.
    Lemma union2_evolve_left: forall l R S S', evolve_1 l R S -> evolve_1 l R (union2 S S').
    Lemma union2_evolve_right: forall l R S S', evolve_1 l R S' -> evolve_1 l R (union2 S S').
    Lemma union_evolve: forall l I R S,
      (forall i:I, evolve_1 l (R i) S) -> evolve_1 l (union R) S.
    Lemma evolve_union: forall l J R S,
      (exists j:J, evolve_1 l R (S j)) -> evolve_1 l R (union S).

Evolutions behave like functional arrows (contra/co-variance)
    Lemma incl_evolve: forall l R R' S, incl R R' -> evolve_1 l R' S -> evolve_1 l R S.
    Lemma evolve_incl: forall l S R S', incl S S' -> evolve_1 l R S -> evolve_1 l R S'.

(Silent) simulations are insensitive to extensional equality
    Lemma simulation_eeq: forall R S, eeq R S -> simulation R -> simulation S.
    Lemma simulation_t_eeq: forall R S, eeq R S -> simulation_t R -> simulation_t S.

  End Sim.

  Section Bi.

    Variables X Y: Type.
    Variable TX: reduction_t A X.
    Variable TY: reduction_t A Y.

Quantifications on both sides of a relation
    Definition bisimulation R := simulation TX TY R /\ simulation TY TX (trans R).
    Definition expansion R := expansion1 TX TY R /\ simulation TY TX (trans R).
    Definition wexpansion R := wexpansion1 TX TY R /\ simulation TY TX (trans R).

Definition of the co-inductive relations as `greatest relations such that'
    Definition bisim := union_st bisimulation.
    Definition expand := union_st expansion.
    Definition wexpand := union_st wexpansion.

Validity of previous definitions
    Lemma bisimulation_bisim: bisimulation bisim.
    Lemma expansion_expand: expansion expand.
    Lemma wexpansion_wexpand: wexpansion wexpand.

Inclusions
    Lemma expand_wexpand: incl expand wexpand.
    Lemma wexpand_bisim: incl wexpand bisim.

  End Bi.

Composition of simulation, expansion1, wexpansion1 relations

  Section Composition.

    Variables X Y Z: Type.
    Variable TX: reduction_t A X.
    Variable TY: reduction_t A Y.
    Variable TZ: reduction_t A Z.

    Variable R: relation2 X Y.
    Variable S: relation2 Y Z.

    Lemma simulation_comp: simulation TX TY R -> simulation TY TZ S -> simulation TX TZ (comp R S).

    Lemma expansion1_comp: expansion1 TX TY R -> expansion1 TY TZ S -> expansion1 TX TZ (comp R S).

    Let wexpansion1_t: wexpansion1 TY TZ S ->
      forall x x' y, star (TY (T _)) x x' -> S x y -> exists2 y', star (TZ (T _)) y y' & S x' y'.

    Lemma wexpansion1_comp: wexpansion1 TX TY R -> wexpansion1 TY TZ S -> wexpansion1 TX TZ (comp R S).

  End Composition.


Composition of bisimulation, expansion, wexpansion relations

  Section BiComposition.

    Variables X Y Z: Type.
    Variable TX: reduction_t A X.
    Variable TY: reduction_t A Y.
    Variable TZ: reduction_t A Z.

    Variable R: relation2 X Y.
    Variable S: relation2 Y Z.

    Lemma bisimulation_comp: bisimulation TX TY R -> bisimulation TY TZ S -> bisimulation TX TZ (comp R S).

    Lemma expansion_comp: expansion TX TY R -> expansion TY TZ S -> expansion TX TZ (comp R S).

    Lemma wexpansion_comp: wexpansion TX TY R -> wexpansion TY TZ S -> wexpansion TX TZ (comp R S).

  End BiComposition.


Bisimilarity is an equivalence relation, Expansion and Weak expansion are preorders

  Section Properties.

    Variable X: Type.
    Variable TX: reduction_t A X.

Symmetry of Bisimilarity
    Lemma bisim_sym: symmetric (bisim TX TX).

Reflexivity of Bisimilarity
    Lemma bisim_refl: reflexive (bisim TX TX).

Transitivity of Bisimilarity
    Lemma bisim_trans: transitive (bisim TX TX).

Definition of Controlled Bisimulations
    Definition bicontrolled R := controlled TX TX R /\ incl R (bisim TX TX).

Reflexivity of Expansion
    Lemma expand_refl: reflexive (expand TX TX).

Transitivity of Expansion
    Lemma expand_trans: transitive (expand TX TX).

Reflexivity of Weak Expansion
    Lemma wexpand_refl: reflexive (wexpand TX TX).

Transitivity of Weak Expansion
    Lemma wexpand_trans: transitive (wexpand TX TX).

  End Properties.

End Global.

Ltac union_evolve n := unfold UIter, simulation_t, evolve_t; apply union_evolve; intro n; apply evolve_union.