orders.minmax

Require Import
  RelationClasses
  abstract_algebra interfaces.orders orders.orders theory.setoids.

Section contents.
  Context `{Setoid A} `{Le A} `{ x y: A, Decision (x y)} `{!PartialOrder (≤)} `{!TotalRelation (≤)}.

  Definition sort (x y: A) : A * A := if decide_rel (≤) x y then (x, y) else (y, x).

  Definition min (x y: A) := fst (sort x y).
  Definition max (x y: A) := snd (sort x y).

  Lemma min_lb_l x y : min x y x.

  Lemma min_lb_r x y : min x y y.

  Lemma min_l x y : x y min x y = x.

  Lemma min_r x y : y x min x y = y.

  Lemma min_diag x: min x x = x.

  Lemma max_ub_l x y : x max x y.

  Lemma max_ub_r x y : y max x y.

  Lemma max_l x y : y x max x y = x.

  Lemma max_r x y : x y max x y = y.

  Lemma max_diag x: max x x = x.

  Global Instance sort_proper `{!Proper ((=) ==> (=) ==> iff) (≤)} : Proper ((=) ==> (=) ==> (=)) sort.

  Global Instance min_proper `{!Proper ((=) ==> (=) ==> iff) (≤)} : Proper ((=) ==> (=) ==> (=)) min.

  Global Instance max_proper `{!Proper ((=) ==> (=) ==> iff) (≤)} : Proper ((=) ==> (=) ==> (=)) max.

  Global Instance min_commutative: Commutative min.

  Global Instance max_commutative: Commutative max.

  Global Instance min_associative: Associative min.

  Global Instance max_associative `{!AntiSymmetric (≤)} `{!Transitive (≤)} `{!TotalOrder (≤)} : Associative max.
End contents.

Instance: Params (@sort) 3.
Instance: Params (@min) 3.
Instance: Params (@max) 3.

Section order_preserving.
  Context `{PartialOrder A} `{PartialOrder B} {f : A B} `{!OrderPreserving f}
    `{!TotalRelation (A:=A) (≤)} `{!TotalRelation (A:=B) (≤)}
    `{ x y: A, Decision (x y)} `{ x y: B, Decision (x y)}.

  Instance: Setoid A := po_setoid.
  Instance: Setoid B := po_setoid.

  Lemma preserves_min x y : f (min x y) = min (f x) (f y).

  Lemma preserves_max x y : f (max x y) = max (f x) (f y).
End order_preserving.