Library WeakMonotonic

Study of the class of weakly monotonic functions (Lemma 2.3)


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.