Library Monotonic
Require Export Settings.
Section Global.
Variable A: Type.
Section A.
Variables X Y: Type.
Variable TX: reduction_t A X.
Variable TY: reduction_t A Y.
Section A'.
Variable R: relation2 X Y.
Variable E: relation2 X X.
Variable T: relation2 Y Y.
identity is monotonic
Lemma identity_mon: monotonic TX TY (identity (X:=X) (Y:=Y)).
constant-to-simulation is monotonic
Lemma constant_mon: simulation TX TY R -> monotonic TX TY (constant R).
simulation-right-chaining is monotonic
Lemma chaining_r_mon: simulation TY TY T -> monotonic TX TY (chaining_r T).
expansion-left-chaining is monotonic
Lemma chaining_l_mon: expansion1 TX TX E -> monotonic TX TY (chaining_l E).
End A'.
Variables F G: function X Y.
Hypothesis HF: monotonic TX TY F.
Hypothesis HG: monotonic TX TY G.
Composition respect monotonicity
Lemma Comp_mon: monotonic TX TY (Comp G F).
Binary union respect monotonicity
Lemma Union2_mon: monotonic TX TY (Union2 F G).
Section Union.
Variable I: Type.
Variable H: I -> function X Y.
Hypothesis HH: forall i, monotonic TX TY (H i).
Union respect monotonicity
Lemma Union_mon: monotonic 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: monotonic TX TY F.
Hypothesis HG: monotonic TX TY G.
Iteration respect monotonicity
Lemma UExp_mon: forall n, monotonic TX TY (fun R => UExp F R n).
Lemma UIter_mon: monotonic TX TY (UIter F).
End B.
End Global.