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 x y : y<=x -> x<y -> False.

Lemma max_l x y : y<=x -> max x y == x.

Lemma max_r x y : x<=y -> max 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.

End GenericMinMax.

Consequences of the minimalist interface: facts about max and min.

Module MinMaxLogicalProperties (Import O:TotalOrder')(Import M:HasMinMax O).
Module Import Private_Tac := !MakeOrderTac O O.

An alternative characterisation of max, equivalent to max_l /\ max_r
A more symmetric version of max_spec, based only on le. Beware that left and right alternatives overlap.

Lemma max_spec_le n m :
(n <= m /\ max n m == m) \/ (m <= n /\ max n m == n).

#[global]
Instance : Proper (eq==>eq==>iff) le.

#[global]
Instance max_compat : Proper (eq==>eq==>eq) max.

A function satisfying the same specification is equal to max.
max commutes with monotone functions.

Lemma max_mono 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 n : max n n == n.

Notation max_idempotent := max_id (only parsing).

Lemma max_assoc m n p : max m (max n p) == max (max m n) p.

Lemma max_comm n m : max n m == max m n.

Ltac solve_max :=
match goal with |- context [max ?n ?m] =>
destruct (max_spec n m); intuition; order
end.

Least-upper bound properties of max

Properties of min

Lemma min_spec n m :
(n < m /\ min n m == n) \/ (m <= n /\ min n m == m).

Lemma min_spec_le n m :
(n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).

#[global]
Instance min_compat : Proper (eq==>eq==>eq) min.

Lemma min_unicity n m p :
((n < m /\ p == n) \/ (m <= n /\ p == m)) -> p == min n m.

Lemma min_unicity_ext 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_mono f :
(Proper (eq ==> eq) f) ->
(Proper (le ==> le) f) ->
forall x y, min (f x) (f y) == f (min x y).

Lemma min_id n : min n n == n.

Notation min_idempotent := min_id (only parsing).

Lemma min_assoc m n p : min m (min n p) == min (min m n) p.

Lemma min_comm n m : min n m == min m n.

Ltac solve_min :=
match goal with |- context [min ?n ?m] =>
destruct (min_spec n m); intuition; order
end.

Lemma le_min_r n m : min n m <= m.

Lemma le_min_l n m : min n m <= n.

Lemma min_l_iff n m : min n m == n <-> n <= m.

Lemma min_r_iff n m : min n m == m <-> m <= n.

Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p.

Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p.

Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p.

Lemma min_glb_l n m p : p <= min n m -> p <= n.

Lemma min_glb_r n m p : p <= min n m -> p <= m.

Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m.

Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m.

Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.

Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m.

Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m.

Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p.

Lemma min_le_compat n m p q : n <= m -> p <= q ->
min n p <= min m q.

Combined properties of min and max

Lemma min_max_absorption n m : max n (min n m) == n.

Lemma max_min_absorption n m : min n (max n m) == n.

Distributivity

Lemma max_min_distr n m p :
max n (min m p) == min (max n m) (max n p).

Lemma min_max_distr n m p :
min n (max m p) == max (min n m) (min n p).

Modularity

Lemma max_min_modular n m p :
max n (min m (max n p)) == min (max n m) (max n p).

Lemma min_max_modular n m p :
min n (max m (min n p)) == max (min n m) (min n p).

Disassociativity

Lemma max_min_disassoc 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 f :
Proper (eq==>eq) f ->
Proper (le==>flip le) f ->
forall x y, max (f x) (f y) == f (min x y).

Lemma min_max_antimono f :
Proper (eq==>eq) f ->
Proper (le==>flip 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 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 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.
Idem for min

Lemma min_case_strong 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 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 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 f : Proper (le ==> le) f ->
forall x y, max (f x) (f y) = f (max x y).

Lemma min_monotone f : Proper (le ==> le) f ->
forall x y, min (f x) (f y) = f (min x y).

Lemma min_max_antimonotone f : Proper (le ==> flip le) f ->
forall x y, min (f x) (f y) = f (max x y).

Lemma max_min_antimonotone f : Proper (le ==> flip 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 Import Private_Dec := 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 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 ?