# 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.