# Library Coq.Structures.GenericMinMax

Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics.

# A Generic construction of min and max

## First, an interface for types with max and/or min

Module Type HasMax (Import E:EqLe').
Parameter Inline max : t -> t -> t.
Parameter max_l : forall x y, y <= x -> max x y == x.
Parameter max_r : forall x y, x <= y -> max x y == y.
End HasMax.
Module Type HasMin (Import E:EqLe').
Parameter Inline min : t -> t -> t.
Parameter min_l : forall x y, x <= y -> min x y == x.
Parameter min_r : forall x y, y <= x -> min x y == y.
End HasMin.
Module Type HasMinMax (E:EqLe) := HasMax E <+ HasMin E.

## Any OrderedTypeFull can be equipped by max and min

based on the compare function.
Definition gmax {A} (cmp : A->A->comparison) x y :=
match cmp x y with Lt => y | _ => x end.
Definition gmin {A} (cmp : A->A->comparison) x y :=
match cmp x y with Gt => y | _ => x end.
Module GenericMinMax (Import O:OrderedTypeFull') <: HasMinMax O.
Definition max := gmax O.compare.
Definition min := gmin O.compare.
Lemma ge_not_lt : forall x y, y <= x -> x < y -> False.
Lemma max_l : forall x y, y <= x -> max x y == x.
Lemma max_r : forall x y, x <= y -> max x y == y.
Lemma min_l : forall x y, x <= y -> min x y == x.
Lemma min_r : forall x y, y <= x -> min x y == y.
End GenericMinMax.

## Consequences of the minimalist interface: facts about max.

Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
Module Import T := !MakeOrderTac O.
An alternative caracterisation of max, equivalent to max_l /\ max_r
Lemma max_spec : forall n m,
( n < m /\ max n m == m ) \/ ( m <= n /\ max n m == n ).
A more symmetric version of max_spec, based only on le. Beware that left and right alternatives overlap.
Lemma max_spec_le : forall n m,
( n <= m /\ max n m == m ) \/ ( m <= n /\ max n m == n ).
Instance : Proper (eq ==> eq ==> iff) le.
Instance max_compat : Proper (eq ==> eq ==> eq) max.
A function satisfying the same specification is equal to max.
Lemma max_unicity : forall n m p,
(( n < m /\ p == m ) \/ ( m <= n /\ p == n )) -> p == max n m.
Lemma max_unicity_ext : forall f,
(forall n m, ( n < m /\ f n m == m ) \/ ( m <= n /\ f n m == n )) ->
(forall n m, f n m == max n m).
max commutes with monotone functions.
Lemma max_mono: forall f,
(Proper (eq ==> eq) f) ->
(Proper (le ==> le) f) ->
forall x y, max (f x) (f y) == f (max x y).

### Semi-lattice algebraic properties of max

Lemma max_id : forall n, max n n == n.
Notation max_idempotent := max_id (only parsing).
Lemma max_assoc : forall m n p, max m (max n p) == max (max m n) p.
Lemma max_comm : forall n m, max n m == max m n.

### Least-upper bound properties of max

Lemma le_max_l : forall n m, n <= max n m.
Lemma le_max_r : forall n m, m <= max n m.
Lemma max_l_iff : forall n m, max n m == n <-> m <= n.
Lemma max_r_iff : forall n m, max n m == m <-> n <= m.
Lemma max_le : forall n m p, p <= max n m -> p <= n \/ p <= m.
Lemma max_le_iff : forall n m p, p <= max n m <-> p <= n \/ p <= m.
Lemma max_lt_iff : forall n m p, p < max n m <-> p < n \/ p < m.
Lemma max_lub_l : forall n m p, max n m <= p -> n <= p.
Lemma max_lub_r : forall n m p, max n m <= p -> m <= p.
Lemma max_lub : forall n m p, n <= p -> m <= p -> max n m <= p.
Lemma max_lub_iff : forall n m p, max n m <= p <-> n <= p /\ m <= p.
Lemma max_lub_lt : forall n m p, n < p -> m < p -> max n m < p.
Lemma max_lub_lt_iff : forall n m p, max n m < p <-> n < p /\ m < p.
Lemma max_le_compat_l : forall n m p, n <= m -> max p n <= max p m.
Lemma max_le_compat_r : forall n m p, n <= m -> max n p <= max m p.
Lemma max_le_compat : forall n m p q, n <= m -> p <= q ->
max n p <= max m q.
End MaxLogicalProperties.

## Properties concernant min, then both min and max.

To avoid too much code duplication, we exploit that min can be seen as a max of the reversed order.
Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
Include MaxLogicalProperties O M.
Import T.
Module ORev := TotalOrderRev O.
Module MRev <: HasMax ORev.
Definition max x y := M.min y x.
Definition max_l x y := M.min_r y x.
Definition max_r x y := M.min_l y x.
End MRev.
Module MPRev := MaxLogicalProperties ORev MRev.
Instance min_compat : Proper (eq ==> eq ==> eq) min.
Lemma min_spec : forall n m,
( n < m /\ min n m == n ) \/ ( m <= n /\ min n m == m ).
Lemma min_spec_le : forall n m,
( n <= m /\ min n m == n ) \/ ( m <= n /\ min n m == m ).
Lemma min_mono: forall f,
(Proper (eq ==> eq) f) ->
(Proper (le ==> le) f) ->
forall x y, min (f x) (f y) == f (min x y).
Lemma min_unicity : forall n m p,
(( n < m /\ p == n ) \/ ( m <= n /\ p == m )) -> p == min n m.
Lemma min_unicity_ext : forall f,
(forall n m, ( n < m /\ f n m == n ) \/ ( m <= n /\ f n m == m )) ->
(forall n m, f n m == min n m).
Lemma min_id : forall n, min n n == n.
Notation min_idempotent := min_id (only parsing).
Lemma min_assoc : forall m n p, min m (min n p) == min (min m n) p.
Lemma min_comm : forall n m, min n m == min m n.
Lemma le_min_r : forall n m, min n m <= m.
Lemma le_min_l : forall n m, min n m <= n.
Lemma min_l_iff : forall n m, min n m == n <-> n <= m.
Lemma min_r_iff : forall n m, min n m == m <-> m <= n.
Lemma min_le : forall n m p, min n m <= p -> n <= p \/ m <= p.
Lemma min_le_iff : forall n m p, min n m <= p <-> n <= p \/ m <= p.
Lemma min_lt_iff : forall n m p, min n m < p <-> n < p \/ m < p.
Lemma min_glb_l : forall n m p, p <= min n m -> p <= n.
Lemma min_glb_r : forall n m p, p <= min n m -> p <= m.
Lemma min_glb : forall n m p, p <= n -> p <= m -> p <= min n m.
Lemma min_glb_iff : forall n m p, p <= min n m <-> p <= n /\ p <= m.
Lemma min_glb_lt : forall n m p, p < n -> p < m -> p < min n m.
Lemma min_glb_lt_iff : forall n m p, p < min n m <-> p < n /\ p < m.
Lemma min_le_compat_l : forall n m p, n <= m -> min p n <= min p m.
Lemma min_le_compat_r : forall n m p, n <= m -> min n p <= min m p.
Lemma min_le_compat : forall n m p q, n <= m -> p <= q ->
min n p <= min m q.

### Combined properties of min and max

Lemma min_max_absorption : forall n m, max n (min n m) == n.
Lemma max_min_absorption : forall n m, min n (max n m) == n.
Distributivity
Lemma max_min_distr : forall n m p,
max n (min m p) == min (max n m) (max n p).
Lemma min_max_distr : forall n m p,
min n (max m p) == max (min n m) (min n p).
Modularity
Lemma max_min_modular : forall n m p,
max n (min m (max n p)) == min (max n m) (max n p).
Lemma min_max_modular : forall n m p,
min n (max m (min n p)) == max (min n m) (min n p).
Disassociativity
Lemma max_min_disassoc : forall n m p,
min n (max m p) <= max (min n m) p.
Anti-monotonicity swaps the role of min and max
Lemma max_min_antimono : forall f,
Proper (eq ==> eq) f ->
Proper (le ==> inverse le) f ->
forall x y, max (f x) (f y) == f (min x y).
Lemma min_max_antimono : forall f,
Proper (eq ==> eq) f ->
Proper (le ==> inverse le) f ->
forall x y, min (f x) (f y) == f (max x y).
End MinMaxLogicalProperties.

## Properties requiring a decidable order

Module MinMaxDecProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
Induction principles for max.
Lemma max_case_strong : forall n m (P:t -> Type),
(forall x y, x == y -> P x -> P y) ->
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m).
Lemma max_case : forall n m (P:t -> Type),
(forall x y, x == y -> P x -> P y) ->
P n -> P m -> P (max n m).
max returns one of its arguments.
Lemma max_dec : forall n m, { max n m == n } + { max n m == m }.
Idem for min
Lemma min_case_strong : forall n m (P:O.t -> Type),
(forall x y, x == y -> P x -> P y) ->
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m).
Lemma min_case : forall n m (P:O.t -> Type),
(forall x y, x == y -> P x -> P y) ->
P n -> P m -> P (min n m).
Lemma min_dec : forall n m, { min n m == n } + { min n m == m }.
End MinMaxDecProperties.
Module MinMaxProperties (Import O:OrderedTypeFull')(Import M:HasMinMax O).
Module OT := OTF_to_TotalOrder O.
Include MinMaxLogicalProperties OT M.
Include MinMaxDecProperties O M.
Definition max_l := max_l.
Definition max_r := max_r.
Definition min_l := min_l.
Definition min_r := min_r.
Notation max_monotone := max_mono.
Notation min_monotone := min_mono.
Notation max_min_antimonotone := max_min_antimono.
Notation min_max_antimonotone := min_max_antimono.
End MinMaxProperties.

## When the equality is Leibniz, we can skip a few Proper precondition.

Module UsualMinMaxLogicalProperties
(Import O:UsualTotalOrder')(Import M:HasMinMax O).
Include MinMaxLogicalProperties O M.
Lemma max_monotone : forall f, Proper (le ==> le) f ->
forall x y, max (f x) (f y) = f (max x y).
Lemma min_monotone : forall f, Proper (le ==> le) f ->
forall x y, min (f x) (f y) = f (min x y).
Lemma min_max_antimonotone : forall f, Proper (le ==> inverse le) f ->
forall x y, min (f x) (f y) = f (max x y).
Lemma max_min_antimonotone : forall f, Proper (le ==> inverse le) f ->
forall x y, max (f x) (f y) = f (min x y).
End UsualMinMaxLogicalProperties.
Module UsualMinMaxDecProperties
(Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
Module P := MinMaxDecProperties O M.
Lemma max_case_strong : forall n m (P:t -> Type),
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m).
Lemma max_case : forall n m (P:t -> Type),
P n -> P m -> P (max n m).
Lemma max_dec : forall n m, { max n m = n } + { max n m = m }.
Lemma min_case_strong : forall n m (P:O.t -> Type),
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m).
Lemma min_case : forall n m (P:O.t -> Type),
P n -> P m -> P (min n m).
Lemma min_dec : forall n m, { min n m = n } + { min n m = m }.
End UsualMinMaxDecProperties.
Module UsualMinMaxProperties
(Import O:UsualOrderedTypeFull')(Import M:HasMinMax O).
Module OT := OTF_to_TotalOrder O.
Include UsualMinMaxLogicalProperties OT M.
Include UsualMinMaxDecProperties O M.
Definition max_l := max_l.
Definition max_r := max_r.
Definition min_l := min_l.
Definition min_r := min_r.
End UsualMinMaxProperties.
From TotalOrder and HasMax and HasEqDec, we can prove that the order is decidable and build an OrderedTypeFull.
Module TOMaxEqDec_to_Compare
(Import O:TotalOrder')(Import M:HasMax O)(Import E:HasEqDec O) <: HasCompare O.
Definition compare x y :=
if eq_dec x y then Eq
else if eq_dec (M.max x y) y then Lt else Gt.
Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
End TOMaxEqDec_to_Compare.
Module TOMaxEqDec_to_OTF (O:TotalOrder)(M:HasMax O)(E:HasEqDec O)
<: OrderedTypeFull
:= O <+ E <+ TOMaxEqDec_to_Compare O M E.
TODO: Some Remaining questions... --> Compare with a type-classes version ? --> Is max_unicity and max_unicity_ext really convenient to express that any possible definition of max will in fact be equivalent ? --> Is it possible to avoid copy-paste about min even more ?