Library Monotonic

Study of the class of monotonic functions (Lemma 1.7 and 1.8)


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.