``` ```

# 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. ```