Library Settings
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.
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.
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.
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.