Library WeakMonotonic
Require Export Monotonic.
Section Global.
Variable A: Type.
Section A.
Variables X Y: Type.
Variable TX: reduction_t A X.
Variable TY: reduction_t A Y.
weak monotonicity entails monotonicity
Lemma monotonic_wmonotonic: forall F, monotonic TX TY F -> wmonotonic TX TY F.
transitive, reflexive closure respects weak monotonicity
Lemma star_wmon: wmonotonic TX TX (star (X:=X)).
Variables F G: function X Y.
Hypothesis HF: wmonotonic TX TY F.
Hypothesis HG: wmonotonic TX TY G.
Composition respects weak monotonicity
Lemma Comp_wmon: wmonotonic TX TY (Comp G F).
Binary union respects weak monotonicity
Lemma Union2_wmon: wmonotonic TX TY (Union2 F G).
Section Union.
Variable I: Type.
Variable H: I -> function X Y.
Hypothesis HH: forall i, wmonotonic TX TY (H i).
Union respects weak monotonicity
Lemma Union_wmon: wmonotonic TX TY (Union H).
End Union.
End A.
Section B.
Variables X Y: Type.
Variable TX: reduction_t A X.
Variable TY: reduction_t A Y.
Variables F G: function X Y.
Hypothesis HF: wmonotonic TX TY F.
Hypothesis HG: wmonotonic TX TY G.
Iteration respects weak monotonicity
Lemma UExp_wmon: forall n, wmonotonic TX TY (fun R => UExp F R n).
Lemma UIter_wmon: wmonotonic TX TY (UIter F).
End B.
Section C.
Variables X Y: Type.
Variable TX: reduction_t A X.
Variable TY: reduction_t A Y.
Variables F G: function X X.
Hypothesis HF: wmonotonic TX TX F.
Hypothesis HG: wmonotonic TX TX G.
Chaining respects weak monotonicity
Lemma Chaining_wmon: wmonotonic TX TX (Chain F G).
Variable L: relation Y.
Hypothesis HL: simulation TY TY L.
The following lemma is not a consequence of the previous one, for typing reasons
Lemma chaing_l_wmon: wmonotonic TY TX (chaining_l L).
End C.
End Global.