semantics.ord.mono

Monotone functions

The predicate monotone f is convertible to Proper (ord_op ++> ord_op) f, but comes with different typeclass resolution behavior. If no Proper instance can be found for f, monotonicity gets turned into an additional subgoal.

Require Import base protype ordtype clat frame.

Definition monotone {X Y : proType} (f : X -> Y) :=
  forall x y : X, x ≤ y -> f x ≤ f y.
Existing Class monotone.
Hint Mode monotone - - ! : typeclass_instances.

Instance proper_monotone {X Y : proType} (f : X -> Y)
  {H : Proper (ord_op ++> ord_op) f} : monotone f | 1 := H.
Instance shelve_monotone {X Y : proType} (f : X -> Y) (H : forall x y, x ≤ y -> f x ≤ f y)
`{phantom (forall x y, x ≤ y -> f x ≤ f y) H} : monotone f | 1000 := H.

Instance monotone_proper {X Y : proType} (f : X -> Y) {H : monotone f} :
  Proper (ord_op ++> ord_op) f | 10 := H.
Hint Cut [_* proper_monotone monotone_proper] : typeclass_instances.
Hint Cut [_* monotone_proper proper_monotone] : typeclass_instances.

Lemma mono {X Y : proType} (f : X -> Y) {H : monotone f} (x y : X) :
  x ≤ y -> f x ≤ f y.
Proof. exact: H. Qed.

Laws

Section MonoCLat.
  Variables (X Y : clat) (f : X -> Y).
  Context {fP : monotone f}.
  Implicit Types (x y : X).

  Lemma monoM x y : f (x ∧ y) ≤ f x ∧ f y.
  Proof. focus; apply: mono; by [exact: meetEl|exact: meetEr]. Qed.

  Lemma monoJ x y : f x ∨ f y ≤ f (x ∨ y).
  Proof. focus; apply: mono; by [exact: joinIl|exact: joinIr]. Qed.

  Lemma monoA I (F : I -> X) : f (∀ i, F i) ≤ ∀ i, f (F i).
  Proof. focus=> i. apply: mono. exact: allE. Qed.

  Lemma monoE I (F : I -> X) : ∃ i, f (F i) ≤ f (∃ i, F i).
  Proof. focus=> i. apply: mono. exact: exI. Qed.

  Lemma monoAc I (P : I -> Prop) (F : I -> X) :
    f (∀ i | P i , F i) ≤ ∀ i | P i , f (F i).
  Proof. focus=> i pi. apply: mono. exact: allEc pi _. Qed.

  Lemma monoEc I (P : I -> Prop) (F : I -> X) :
    ∃ i | P i , f (F i) ≤ f (∃ i | P i , F i).
  Proof. focus=> i pi. apply: mono. exact: exIc pi _. Qed.
End MonoCLat.