Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

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 x y : y<=x -> x<y -> False.x, y:t
y <= x -> x < y -> False
 Proof.x, y:t
y <= x -> x < y -> False
 intros H H'.x, y:t
H:y <= x
H':x < y
False
 apply (StrictOrder_Irreflexive x).x, y:t
H:y <= x
H':x < y
x < x
 rewrite le_lteq in *; destruct H as [H|H].x, y:t
H:y < x
H':x < y
x < x
x, y:t
H:y == x
H':x < y
x < x
 -x, y:t
H:y < x
H':x < y
x < x transitivity y; auto.
 -x, y:t
H:y == x
H':x < y
x < x rewrite H in H'; auto.
 Qed.

 Lemma max_l x y : y<=x -> max x y == x.x, y:t
y <= x -> max x y == x
 Proof.x, y:t
y <= x -> max x y == x
 intros.x, y:t
H:y <= x
max x y == x unfold max, gmax.x, y:t
H:y <= x
match x ?= y with
| Lt => y
| _ => x
end == x case compare_spec; auto with relations.x, y:t
H:y <= x
x < y -> y == x
 intros; elim (ge_not_lt x y); auto.
 Qed.

 Lemma max_r x y : x<=y -> max x y == y.x, y:t
x <= y -> max x y == y
 Proof.x, y:t
x <= y -> max x y == y
 intros.x, y:t
H:x <= y
max x y == y unfold max, gmax.x, y:t
H:x <= y
match x ?= y with
| Lt => y
| _ => x
end == y case compare_spec; auto with relations.x, y:t
H:x <= y
y < x -> x == y
 intros; elim (ge_not_lt y x); auto.
 Qed.

 Lemma min_l x y : x<=y -> min x y == x.x, y:t
x <= y -> min x y == x
 Proof.x, y:t
x <= y -> min x y == x
 intros.x, y:t
H:x <= y
min x y == x unfold min, gmin.x, y:t
H:x <= y
match x ?= y with
| Gt => y
| _ => x
end == x case compare_spec; auto with relations.x, y:t
H:x <= y
y < x -> y == x
 intros; elim (ge_not_lt y x); auto.
 Qed.

 Lemma min_r x y : y<=x -> min x y == y.x, y:t
y <= x -> min x y == y
 Proof.x, y:t
y <= x -> min x y == y
 intros.x, y:t
H:y <= x
min x y == y unfold min, gmin.x, y:t
H:y <= x
match x ?= y with
| Gt => y
| _ => x
end == y case compare_spec; auto with relations.x, y:t
H:y <= x
x < y -> x == y
 intros; elim (ge_not_lt x y); auto.
 Qed.

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

Lemma max_spec n m :
  (n < m /\ max n m == m) \/ (m <= n /\ max n m == n).n, m:t
n < m /\ max n m == m \/ m <= n /\ max n m == n
Proof.n, m:t
n < m /\ max n m == m \/ m <= n /\ max n m == n
 destruct (lt_total n m); [left|right].n, m:t
H:n < m
n < m /\ max n m == m
n, m:t
H:n == m \/ m < n
m <= n /\ max n m == n
 -n, m:t
H:n < m
n < m /\ max n m == m split; auto.n, m:t
H:n < m
max n m == m apply max_r.n, m:t
H:n < m
n <= m rewrite le_lteq; auto.
 -n, m:t
H:n == m \/ m < n
m <= n /\ max n m == n assert (m <= n) by (rewrite le_lteq; intuition).n, m:t
H:n == m \/ m < n
H0:m <= n
m <= n /\ max n m == n
   split; auto.n, m:t
H:n == m \/ m < n
H0:m <= n
max n m == n now apply max_l.
Qed.

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).n, m:t
n <= m /\ max n m == m \/ m <= n /\ max n m == n
Proof.n, m:t
n <= m /\ max n m == m \/ m <= n /\ max n m == n
 destruct (max_spec n m); [left|right]; intuition; order.
Qed.

Instance : Proper (eq==>eq==>iff) le.Proper (eq ==> eq ==> iff) le
Proof.Proper (eq ==> eq ==> iff) le repeat red.forall x y : t,
x == y ->
forall x0 y0 : t,
x0 == y0 ->
(x <= x0 -> y <= y0) /\ (y <= y0 -> x <= x0) intuition order. Qed.

Instance max_compat : Proper (eq==>eq==>eq) max.Proper (eq ==> eq ==> eq) max
Proof.Proper (eq ==> eq ==> eq) max
 intros x x' Hx y y' Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
max x y == max x' y'
 assert (H1 := max_spec x y).x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
H1:x < y /\ max x y == y \/ y <= x /\ max x y == x
max x y == max x' y' assert (H2 := max_spec x' y').x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
H1:x < y /\ max x y == y \/ y <= x /\ max x y == x
H2:x' < y' /\ max x' y' == y' \/
y' <= x' /\ max x' y' == x'
max x y == max x' y'
 set (m := max x y) in *; set (m' := max x' y') in *; clearbody m m'.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
m:t
H1:x < y /\ m == y \/ y <= x /\ m == x
m':t
H2:x' < y' /\ m' == y' \/ y' <= x' /\ m' == x'
m == m'
 rewrite <- Hx, <- Hy in *.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
m:t
H1:x < y /\ m == y \/ y <= x /\ m == x
m':t
H2:x < y /\ m' == y \/ y <= x /\ m' == x
m == m' 
 destruct (lt_total x y); intuition order.
Qed.

A function satisfying the same specification is equal to max.

Lemma max_unicity n m p :
 ((n < m /\ p == m) \/ (m <= n /\ p == n)) -> p == max n m.n, m, p:t
n < m /\ p == m \/ m <= n /\ p == n -> p == max n m
Proof.n, m, p:t
n < m /\ p == m \/ m <= n /\ p == n -> p == max n m
 assert (Hm := max_spec n m).n, m, p:t
Hm:n < m /\ max n m == m \/ m <= n /\ max n m == n
n < m /\ p == m \/ m <= n /\ p == n -> p == max n m
 destruct (lt_total n m); intuition; order.
Qed.

Lemma max_unicity_ext 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).f:t -> t -> t
(forall n m : t,
 n < m /\ f n m == m \/ m <= n /\ f n m == n) ->
forall n m : t, f n m == max n m
Proof.f:t -> t -> t
(forall n m : t,
 n < m /\ f n m == m \/ m <= n /\ f n m == n) ->
forall n m : t, f n m == max n m
 intros.f:t -> t -> t
H:forall n0 m0 : t,
n0 < m0 /\ f n0 m0 == m0 \/
m0 <= n0 /\ f n0 m0 == n0
n, m:t
f n m == max n m apply max_unicity; auto.
Qed.

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).f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> le) f ->
forall x y : t, max (f x) (f y) == f (max x y)
Proof.f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> le) f ->
forall x y : t, max (f x) (f y) == f (max x y)
 intros Eqf Lef x y.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
max (f x) (f y) == f (max x y)
 destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
  destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:max x y == y
H':f y <= f x
E':max (f x) (f y) == f x
max (f x) (f y) == f y
f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:max x y == x
H':f x < f y
E':max (f x) (f y) == f y
max (f x) (f y) == f x
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:max x y == y
H':f y <= f x
E':max (f x) (f y) == f x
max (f x) (f y) == f y assert (f x <= f y) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:max x y == y
H':f y <= f x
E':max (f x) (f y) == f x
H0:f x <= f y
max (f x) (f y) == f y order.
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:max x y == x
H':f x < f y
E':max (f x) (f y) == f y
max (f x) (f y) == f x assert (f y <= f x) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:max x y == x
H':f x < f y
E':max (f x) (f y) == f y
H0:f y <= f x
max (f x) (f y) == f x order.
Qed.

Semi-lattice algebraic properties of max

Lemma max_id n : max n n == n.n:t
max n n == n
Proof.n:t
max n n == n
 apply max_l; order.
Qed.

Notation max_idempotent := max_id (only parsing).

Lemma max_assoc m n p : max m (max n p) == max (max m n) p.m, n, p:t
max m (max n p) == max (max m n) p
Proof.m, n, p:t
max m (max n p) == max (max m n) p
 destruct (max_spec n p) as [(H,E)|(H,E)]; rewrite E;
 destruct (max_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy.m, n, p:t
H:n < p
E:max n p == p
H':m < n
E':max m n == n
max m p == p
m, n, p:t
H:p <= n
E:max n p == n
H':n <= m
E':max m n == m
m == max m p
 -m, n, p:t
H:n < p
E:max n p == p
H':m < n
E':max m n == n
max m p == p apply max_r; order.
 -m, n, p:t
H:p <= n
E:max n p == n
H':n <= m
E':max m n == m
m == max m p symmetry.m, n, p:t
H:p <= n
E:max n p == n
H':n <= m
E':max m n == m
max m p == m apply max_l; order.
Qed.

Lemma max_comm n m : max n m == max m n.n, m:t
max n m == max m n
Proof.n, m:t
max n m == max m n
 destruct (max_spec m n) as [(H,E)|(H,E)]; rewrite E;
  (apply max_r || apply max_l); order.
Qed.

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

Least-upper bound properties of max

Lemma le_max_l n m : n <= max n m.n, m:t
n <= max n m
Proof.n, m:t
n <= max n m solve_max. Qed.

Lemma le_max_r n m : m <= max n m.n, m:t
m <= max n m
Proof.n, m:t
m <= max n m solve_max. Qed.

Lemma max_l_iff n m : max n m == n <-> m <= n.n, m:t
max n m == n <-> m <= n
Proof.n, m:t
max n m == n <-> m <= n solve_max. Qed.

Lemma max_r_iff n m : max n m == m <-> n <= m.n, m:t
max n m == m <-> n <= m
Proof.n, m:t
max n m == m <-> n <= m solve_max. Qed.

Lemma max_le n m p : p <= max n m -> p <= n \/ p <= m.n, m, p:t
p <= max n m -> p <= n \/ p <= m
Proof.n, m, p:t
p <= max n m -> p <= n \/ p <= m
 destruct (max_spec n m); [right|left]; intuition; order.
Qed.

Lemma max_le_iff n m p : p <= max n m <-> p <= n \/ p <= m.n, m, p:t
p <= max n m <-> p <= n \/ p <= m
Proof.n, m, p:t
p <= max n m <-> p <= n \/ p <= m
  split.n, m, p:t
p <= max n m -> p <= n \/ p <= m
n, m, p:t
p <= n \/ p <= m -> p <= max n m
  -n, m, p:t
p <= max n m -> p <= n \/ p <= m apply max_le.
  -n, m, p:t
p <= n \/ p <= m -> p <= max n m solve_max.
Qed.

Lemma max_lt_iff n m p : p < max n m <-> p < n \/ p < m.n, m, p:t
p < max n m <-> p < n \/ p < m
Proof.n, m, p:t
p < max n m <-> p < n \/ p < m
 destruct (max_spec n m); intuition;
  order || (right; order) || (left; order).
Qed.

Lemma max_lub_l n m p : max n m <= p -> n <= p.n, m, p:t
max n m <= p -> n <= p
Proof.n, m, p:t
max n m <= p -> n <= p solve_max. Qed.

Lemma max_lub_r n m p : max n m <= p -> m <= p.n, m, p:t
max n m <= p -> m <= p
Proof.n, m, p:t
max n m <= p -> m <= p solve_max. Qed.

Lemma max_lub n m p : n <= p -> m <= p -> max n m <= p.n, m, p:t
n <= p -> m <= p -> max n m <= p
Proof.n, m, p:t
n <= p -> m <= p -> max n m <= p solve_max. Qed.

Lemma max_lub_iff n m p : max n m <= p <-> n <= p /\ m <= p.n, m, p:t
max n m <= p <-> n <= p /\ m <= p
Proof.n, m, p:t
max n m <= p <-> n <= p /\ m <= p solve_max. Qed.

Lemma max_lub_lt n m p : n < p -> m < p -> max n m < p.n, m, p:t
n < p -> m < p -> max n m < p
Proof.n, m, p:t
n < p -> m < p -> max n m < p solve_max. Qed.

Lemma max_lub_lt_iff n m p : max n m < p <-> n < p /\ m < p.n, m, p:t
max n m < p <-> n < p /\ m < p
Proof.n, m, p:t
max n m < p <-> n < p /\ m < p solve_max. Qed.

Lemma max_le_compat_l n m p : n <= m -> max p n <= max p m.n, m, p:t
n <= m -> max p n <= max p m
Proof.n, m, p:t
n <= m -> max p n <= max p m intros.n, m, p:t
H:n <= m
max p n <= max p m apply max_lub_iff.n, m, p:t
H:n <= m
p <= max p m /\ n <= max p m solve_max. Qed.

Lemma max_le_compat_r n m p : n <= m -> max n p <= max m p.n, m, p:t
n <= m -> max n p <= max m p
Proof.n, m, p:t
n <= m -> max n p <= max m p intros.n, m, p:t
H:n <= m
max n p <= max m p apply max_lub_iff.n, m, p:t
H:n <= m
n <= max m p /\ p <= max m p solve_max. Qed.

Lemma max_le_compat n m p q : n <= m -> p <= q -> max n p <= max m q.n, m, p, q:t
n <= m -> p <= q -> max n p <= max m q
Proof.n, m, p, q:t
n <= m -> p <= q -> max n p <= max m q
 intros Hnm Hpq.n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
max n p <= max m q
 assert (LE := max_le_compat_l _ _ m Hpq).n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
LE:max m p <= max m q
max n p <= max m q
 assert (LE' := max_le_compat_r _ _ p Hnm).n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
LE:max m p <= max m q
LE':max n p <= max m p
max n p <= max m q
 order.
Qed.

Properties of min

Lemma min_spec n m :
 (n < m /\ min n m == n) \/ (m <= n /\ min n m == m).n, m:t
n < m /\ min n m == n \/ m <= n /\ min n m == m
Proof.n, m:t
n < m /\ min n m == n \/ m <= n /\ min n m == m
 destruct (lt_total n m); [left|right].n, m:t
H:n < m
n < m /\ min n m == n
n, m:t
H:n == m \/ m < n
m <= n /\ min n m == m
 -n, m:t
H:n < m
n < m /\ min n m == n split; auto.n, m:t
H:n < m
min n m == n apply min_l.n, m:t
H:n < m
n <= m rewrite le_lteq; auto.
 -n, m:t
H:n == m \/ m < n
m <= n /\ min n m == m assert (m <= n) by (rewrite le_lteq; intuition).n, m:t
H:n == m \/ m < n
H0:m <= n
m <= n /\ min n m == m
   split; auto.n, m:t
H:n == m \/ m < n
H0:m <= n
min n m == m now apply min_r.
Qed.

Lemma min_spec_le n m :
 (n <= m /\ min n m == n) \/ (m <= n /\ min n m == m).n, m:t
n <= m /\ min n m == n \/ m <= n /\ min n m == m
Proof.n, m:t
n <= m /\ min n m == n \/ m <= n /\ min n m == m
 destruct (min_spec n m); [left|right]; intuition; order.
Qed.

Instance min_compat : Proper (eq==>eq==>eq) min.Proper (eq ==> eq ==> eq) min
Proof.Proper (eq ==> eq ==> eq) min
intros x x' Hx y y' Hy.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
min x y == min x' y'
assert (H1 := min_spec x y).x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
H1:x < y /\ min x y == x \/ y <= x /\ min x y == y
min x y == min x' y' assert (H2 := min_spec x' y').x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
H1:x < y /\ min x y == x \/ y <= x /\ min x y == y
H2:x' < y' /\ min x' y' == x' \/
y' <= x' /\ min x' y' == y'
min x y == min x' y'
set (m := min x y) in *; set (m' := min x' y') in *; clearbody m m'.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
m:t
H1:x < y /\ m == x \/ y <= x /\ m == y
m':t
H2:x' < y' /\ m' == x' \/ y' <= x' /\ m' == y'
m == m'
rewrite <- Hx, <- Hy in *.x, x':t
Hx:x == x'
y, y':t
Hy:y == y'
m:t
H1:x < y /\ m == x \/ y <= x /\ m == y
m':t
H2:x < y /\ m' == x \/ y <= x /\ m' == y
m == m'
destruct (lt_total x y); intuition order.
Qed.

Lemma min_unicity n m p :
 ((n < m /\ p == n) \/ (m <= n /\ p == m)) ->  p == min n m.n, m, p:t
n < m /\ p == n \/ m <= n /\ p == m -> p == min n m
Proof.n, m, p:t
n < m /\ p == n \/ m <= n /\ p == m -> p == min n m
 assert (Hm := min_spec n m).n, m, p:t
Hm:n < m /\ min n m == n \/ m <= n /\ min n m == m
n < m /\ p == n \/ m <= n /\ p == m -> p == min n m
 destruct (lt_total n m); intuition; order.
Qed.

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).f:t -> t -> t
(forall n m : t,
 n < m /\ f n m == n \/ m <= n /\ f n m == m) ->
forall n m : t, f n m == min n m
Proof.f:t -> t -> t
(forall n m : t,
 n < m /\ f n m == n \/ m <= n /\ f n m == m) ->
forall n m : t, f n m == min n m
 intros.f:t -> t -> t
H:forall n0 m0 : t,
n0 < m0 /\ f n0 m0 == n0 \/
m0 <= n0 /\ f n0 m0 == m0
n, m:t
f n m == min n m apply min_unicity; auto.
Qed.

Lemma min_mono f :
 (Proper (eq ==> eq) f) ->
 (Proper (le ==> le) f) ->
 forall x y, min (f x) (f y) == f (min x y).f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> le) f ->
forall x y : t, min (f x) (f y) == f (min x y)
Proof.f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> le) f ->
forall x y : t, min (f x) (f y) == f (min x y)
 intros Eqf Lef x y.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
min (f x) (f y) == f (min x y)
 destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
  destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:min x y == x
H':f y <= f x
E':min (f x) (f y) == f y
min (f x) (f y) == f x
f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:min x y == y
H':f x < f y
E':min (f x) (f y) == f x
min (f x) (f y) == f y
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:min x y == x
H':f y <= f x
E':min (f x) (f y) == f y
min (f x) (f y) == f x assert (f x <= f y) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:x < y
E:min x y == x
H':f y <= f x
E':min (f x) (f y) == f y
H0:f x <= f y
min (f x) (f y) == f x order.
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:min x y == y
H':f x < f y
E':min (f x) (f y) == f x
min (f x) (f y) == f y assert (f y <= f x) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> le) f
x, y:t
H:y <= x
E:min x y == y
H':f x < f y
E':min (f x) (f y) == f x
H0:f y <= f x
min (f x) (f y) == f y order.
Qed.

Lemma min_id n : min n n == n.n:t
min n n == n
Proof.n:t
min n n == n
 apply min_l; order.
Qed.

Notation min_idempotent := min_id (only parsing).

Lemma min_assoc m n p : min m (min n p) == min (min m n) p.m, n, p:t
min m (min n p) == min (min m n) p
Proof.m, n, p:t
min m (min n p) == min (min m n) p
 destruct (min_spec n p) as [(H,E)|(H,E)]; rewrite E;
 destruct (min_spec m n) as [(H',E')|(H',E')]; rewrite E', ?E; try easy.m, n, p:t
H:n < p
E:min n p == n
H':m < n
E':min m n == m
m == min m p
m, n, p:t
H:p <= n
E:min n p == p
H':n <= m
E':min m n == n
min m p == p
 -m, n, p:t
H:n < p
E:min n p == n
H':m < n
E':min m n == m
m == min m p symmetry.m, n, p:t
H:n < p
E:min n p == n
H':m < n
E':min m n == m
min m p == m apply min_l; order.
 -m, n, p:t
H:p <= n
E:min n p == p
H':n <= m
E':min m n == n
min m p == p apply min_r; order.
Qed.

Lemma min_comm n m : min n m == min m n.n, m:t
min n m == min m n
Proof.n, m:t
min n m == min m n
 destruct (min_spec m n) as [(H,E)|(H,E)]; rewrite E;
  (apply min_r || apply min_l); order.
Qed.

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.n, m:t
min n m <= m
Proof.n, m:t
min n m <= m solve_min. Qed.

Lemma le_min_l n m : min n m <= n.n, m:t
min n m <= n
Proof.n, m:t
min n m <= n solve_min. Qed.

Lemma min_l_iff n m : min n m == n <-> n <= m.n, m:t
min n m == n <-> n <= m
Proof.n, m:t
min n m == n <-> n <= m solve_min. Qed.

Lemma min_r_iff n m : min n m == m <-> m <= n.n, m:t
min n m == m <-> m <= n
Proof.n, m:t
min n m == m <-> m <= n solve_min. Qed.

Lemma min_le n m p : min n m <= p -> n <= p \/ m <= p.n, m, p:t
min n m <= p -> n <= p \/ m <= p
Proof.n, m, p:t
min n m <= p -> n <= p \/ m <= p
 destruct (min_spec n m); [left|right]; intuition; order.
Qed.

Lemma min_le_iff n m p : min n m <= p <-> n <= p \/ m <= p.n, m, p:t
min n m <= p <-> n <= p \/ m <= p
Proof.n, m, p:t
min n m <= p <-> n <= p \/ m <= p
  split.n, m, p:t
min n m <= p -> n <= p \/ m <= p
n, m, p:t
n <= p \/ m <= p -> min n m <= p
  -n, m, p:t
min n m <= p -> n <= p \/ m <= p apply min_le.
  -n, m, p:t
n <= p \/ m <= p -> min n m <= p solve_min.
Qed.

Lemma min_lt_iff n m p : min n m < p <-> n < p \/ m < p.n, m, p:t
min n m < p <-> n < p \/ m < p
Proof.n, m, p:t
min n m < p <-> n < p \/ m < p
 destruct (min_spec n m); intuition;
  order || (right; order) || (left; order).
Qed.

Lemma min_glb_l n m p : p <= min n m -> p <= n.n, m, p:t
p <= min n m -> p <= n
Proof.n, m, p:t
p <= min n m -> p <= n solve_min. Qed.

Lemma min_glb_r n m p : p <= min n m -> p <= m.n, m, p:t
p <= min n m -> p <= m
Proof.n, m, p:t
p <= min n m -> p <= m solve_min. Qed.

Lemma min_glb n m p : p <= n -> p <= m -> p <= min n m.n, m, p:t
p <= n -> p <= m -> p <= min n m
Proof.n, m, p:t
p <= n -> p <= m -> p <= min n m solve_min. Qed.

Lemma min_glb_iff n m p : p <= min n m <-> p <= n /\ p <= m.n, m, p:t
p <= min n m <-> p <= n /\ p <= m
Proof.n, m, p:t
p <= min n m <-> p <= n /\ p <= m solve_min. Qed.

Lemma min_glb_lt n m p : p < n -> p < m -> p < min n m.n, m, p:t
p < n -> p < m -> p < min n m
Proof.n, m, p:t
p < n -> p < m -> p < min n m solve_min. Qed.

Lemma min_glb_lt_iff n m p : p < min n m <-> p < n /\ p < m.n, m, p:t
p < min n m <-> p < n /\ p < m
Proof.n, m, p:t
p < min n m <-> p < n /\ p < m solve_min. Qed.

Lemma min_le_compat_l n m p : n <= m -> min p n <= min p m.n, m, p:t
n <= m -> min p n <= min p m
Proof.n, m, p:t
n <= m -> min p n <= min p m intros.n, m, p:t
H:n <= m
min p n <= min p m apply min_glb_iff.n, m, p:t
H:n <= m
min p n <= p /\ min p n <= m solve_min. Qed.

Lemma min_le_compat_r n m p : n <= m -> min n p <= min m p.n, m, p:t
n <= m -> min n p <= min m p
Proof.n, m, p:t
n <= m -> min n p <= min m p intros.n, m, p:t
H:n <= m
min n p <= min m p apply min_glb_iff.n, m, p:t
H:n <= m
min n p <= m /\ min n p <= p solve_min. Qed.

Lemma min_le_compat n m p q : n <= m -> p <= q ->
 min n p <= min m q.n, m, p, q:t
n <= m -> p <= q -> min n p <= min m q
Proof.n, m, p, q:t
n <= m -> p <= q -> min n p <= min m q
 intros Hnm Hpq.n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
min n p <= min m q
 assert (LE := min_le_compat_l _ _ m Hpq).n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
LE:min m p <= min m q
min n p <= min m q
 assert (LE' := min_le_compat_r _ _ p Hnm).n, m, p, q:t
Hnm:n <= m
Hpq:p <= q
LE:min m p <= min m q
LE':min n p <= min m p
min n p <= min m q
 order.
Qed.

Combined properties of min and max

Lemma min_max_absorption n m : max n (min n m) == n.n, m:t
max n (min n m) == n
Proof.n, m:t
max n (min n m) == n
 intros.n, m:t
max n (min n m) == n
 destruct (min_spec n m) as [(C,E)|(C,E)]; rewrite E.n, m:t
C:n < m
E:min n m == n
max n n == n
n, m:t
C:m <= n
E:min n m == m
max n m == n
 -n, m:t
C:n < m
E:min n m == n
max n n == n apply max_l.n, m:t
C:n < m
E:min n m == n
n <= n order.
 -n, m:t
C:m <= n
E:min n m == m
max n m == n destruct (max_spec n m); intuition; order.
Qed.

Lemma max_min_absorption n m : min n (max n m) == n.n, m:t
min n (max n m) == n
Proof.n, m:t
min n (max n m) == n
 intros.n, m:t
min n (max n m) == n
 destruct (max_spec n m) as [(C,E)|(C,E)]; rewrite E.n, m:t
C:n < m
E:max n m == m
min n m == n
n, m:t
C:m <= n
E:max n m == n
min n n == n
 -n, m:t
C:n < m
E:max n m == m
min n m == n destruct (min_spec n m) as [(C',E')|(C',E')]; auto.n, m:t
C:n < m
E:max n m == m
C':m <= n
E':min n m == m
min n m == n order.
 -n, m:t
C:m <= n
E:max n m == n
min n n == n apply min_l; auto.n, m:t
C:m <= n
E:max n m == n
n <= n order.
Qed.

Distributivity

Lemma max_min_distr n m p :
 max n (min m p) == min (max n m) (max n p).n, m, p:t
max n (min m p) == min (max n m) (max n p)
Proof.n, m, p:t
max n (min m p) == min (max n m) (max n p)
 symmetry.n, m, p:t
min (max n m) (max n p) == max n (min m p) apply min_mono.n, m, p:t
Proper (eq ==> eq) (max n)
n, m, p:t
Proper (le ==> le) (max n)
 -n, m, p:t
Proper (eq ==> eq) (max n) eauto with *.
 -n, m, p:t
Proper (le ==> le) (max n) repeat red; intros.n, m, p, x, y:t
H:x <= y
max n x <= max n y apply max_le_compat_l; auto.
Qed.

Lemma min_max_distr n m p :
 min n (max m p) == max (min n m) (min n p).n, m, p:t
min n (max m p) == max (min n m) (min n p)
Proof.n, m, p:t
min n (max m p) == max (min n m) (min n p)
 symmetry.n, m, p:t
max (min n m) (min n p) == min n (max m p) apply max_mono.n, m, p:t
Proper (eq ==> eq) (min n)
n, m, p:t
Proper (le ==> le) (min n)
 -n, m, p:t
Proper (eq ==> eq) (min n) eauto with *.
 -n, m, p:t
Proper (le ==> le) (min n) repeat red; intros.n, m, p, x, y:t
H:x <= y
min n x <= min n y apply min_le_compat_l; auto.
Qed.

Modularity

Lemma max_min_modular n m p :
 max n (min m (max n p)) == min (max n m) (max n p).n, m, p:t
max n (min m (max n p)) == min (max n m) (max n p)
Proof.n, m, p:t
max n (min m (max n p)) == min (max n m) (max n p)
 rewrite <- max_min_distr.n, m, p:t
max n (min m (max n p)) == max n (min m p)
 destruct (max_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.n, m, p:t
C:p <= n
E:max n p == n
max n (min m n) == max n (min m p)
 destruct (min_spec m n) as [(C',E')|(C',E')]; rewrite E'.n, m, p:t
C:p <= n
E:max n p == n
C':m < n
E':min m n == m
max n m == max n (min m p)
n, m, p:t
C:p <= n
E:max n p == n
C':n <= m
E':min m n == n
max n n == max n (min m p)
 -n, m, p:t
C:p <= n
E:max n p == n
C':m < n
E':min m n == m
max n m == max n (min m p) rewrite 2 max_l; try order.n, m, p:t
C:p <= n
E:max n p == n
C':m < n
E':min m n == m
min m p <= n rewrite min_le_iff; auto.
 -n, m, p:t
C:p <= n
E:max n p == n
C':n <= m
E':min m n == n
max n n == max n (min m p) rewrite 2 max_l; try order.n, m, p:t
C:p <= n
E:max n p == n
C':n <= m
E':min m n == n
min m p <= n rewrite min_le_iff; auto.
Qed.

Lemma min_max_modular n m p :
 min n (max m (min n p)) == max (min n m) (min n p).n, m, p:t
min n (max m (min n p)) == max (min n m) (min n p)
Proof.n, m, p:t
min n (max m (min n p)) == max (min n m) (min n p)
 intros.n, m, p:t
min n (max m (min n p)) == max (min n m) (min n p) rewrite <- min_max_distr.n, m, p:t
min n (max m (min n p)) == min n (max m p)
 destruct (min_spec n p) as [(C,E)|(C,E)]; rewrite E; auto with *.n, m, p:t
C:n < p
E:min n p == n
min n (max m n) == min n (max m p)
 destruct (max_spec m n) as [(C',E')|(C',E')]; rewrite E'.n, m, p:t
C:n < p
E:min n p == n
C':m < n
E':max m n == n
min n n == min n (max m p)
n, m, p:t
C:n < p
E:min n p == n
C':n <= m
E':max m n == m
min n m == min n (max m p)
 -n, m, p:t
C:n < p
E:min n p == n
C':m < n
E':max m n == n
min n n == min n (max m p) rewrite 2 min_l; try order.n, m, p:t
C:n < p
E:min n p == n
C':m < n
E':max m n == n
n <= max m p rewrite max_le_iff; right; order.
 -n, m, p:t
C:n < p
E:min n p == n
C':n <= m
E':max m n == m
min n m == min n (max m p) rewrite 2 min_l; try order.n, m, p:t
C:n < p
E:min n p == n
C':n <= m
E':max m n == m
n <= max m p rewrite max_le_iff; auto.
Qed.

Disassociativity

Lemma max_min_disassoc n m p :
 min n (max m p) <= max (min n m) p.n, m, p:t
min n (max m p) <= max (min n m) p
Proof.n, m, p:t
min n (max m p) <= max (min n m) p
 intros.n, m, p:t
min n (max m p) <= max (min n m) p rewrite min_max_distr.n, m, p:t
max (min n m) (min n p) <= max (min n m) p
 auto using max_le_compat_l, le_min_r.
Qed.

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).f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> flip le) f ->
forall x y : t, max (f x) (f y) == f (min x y)
Proof.f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> flip le) f ->
forall x y : t, max (f x) (f y) == f (min x y)
 intros Eqf Lef x y.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
max (f x) (f y) == f (min x y)
 destruct (min_spec x y) as [(H,E)|(H,E)]; rewrite E;
  destruct (max_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:min x y == x
H':f x < f y
E':max (f x) (f y) == f y
max (f x) (f y) == f x
f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:min x y == y
H':f y <= f x
E':max (f x) (f y) == f x
max (f x) (f y) == f y
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:min x y == x
H':f x < f y
E':max (f x) (f y) == f y
max (f x) (f y) == f x assert (f y <= f x) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:min x y == x
H':f x < f y
E':max (f x) (f y) == f y
H0:f y <= f x
max (f x) (f y) == f x order.
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:min x y == y
H':f y <= f x
E':max (f x) (f y) == f x
max (f x) (f y) == f y assert (f x <= f y) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:min x y == y
H':f y <= f x
E':max (f x) (f y) == f x
H0:f x <= f y
max (f x) (f y) == f y order.
Qed.

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).f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> flip le) f ->
forall x y : t, min (f x) (f y) == f (max x y)
Proof.f:t -> t
Proper (eq ==> eq) f ->
Proper (le ==> flip le) f ->
forall x y : t, min (f x) (f y) == f (max x y)
 intros Eqf Lef x y.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
min (f x) (f y) == f (max x y)
 destruct (max_spec x y) as [(H,E)|(H,E)]; rewrite E;
  destruct (min_spec (f x) (f y)) as [(H',E')|(H',E')]; auto.f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:max x y == y
H':f x < f y
E':min (f x) (f y) == f x
min (f x) (f y) == f y
f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:max x y == x
H':f y <= f x
E':min (f x) (f y) == f y
min (f x) (f y) == f x
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:max x y == y
H':f x < f y
E':min (f x) (f y) == f x
min (f x) (f y) == f y assert (f y <= f x) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:x < y
E:max x y == y
H':f x < f y
E':min (f x) (f y) == f x
H0:f y <= f x
min (f x) (f y) == f y order.
 -f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:max x y == x
H':f y <= f x
E':min (f x) (f y) == f y
min (f x) (f y) == f x assert (f x <= f y) by (apply Lef; order).f:t -> t
Eqf:Proper (eq ==> eq) f
Lef:Proper (le ==> flip le) f
x, y:t
H:y <= x
E:max x y == x
H':f y <= f x
E':min (f x) (f y) == f y
H0:f x <= f y
min (f x) (f y) == f x order.
Qed.

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).n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m)
Proof.n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m)
intros Compat Hl Hr.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
P (max n m)
destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
EQ:n == m
P (max n m)
n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
LT:n < m
P (max n m)
n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
GT:m < n
P (max n m)
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
EQ:n == m
P (max n m) assert (n<=m) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
EQ:n == m
H:n <= m
P (max n m)
  apply (Compat m), Hr; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
EQ:n == m
H:n <= m
m == max n m symmetry; apply max_r; auto.
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
LT:n < m
P (max n m) assert (n<=m) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
LT:n < m
H:n <= m
P (max n m)
  apply (Compat m), Hr; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
LT:n < m
H:n <= m
m == max n m symmetry; apply max_r; auto.
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
GT:m < n
P (max n m) assert (m<=n) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
GT:m < n
H:m <= n
P (max n m)
  apply (Compat n), Hl; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:m <= n -> P n
Hr:n <= m -> P m
GT:m < n
H:m <= n
n == max n m symmetry; apply max_l; auto.
Defined.

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).n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
P n -> P m -> P (max n m)
Proof.n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
P n -> P m -> P (max n m) intros.n, m:t
P:t -> Type
X:forall x y : t, x == y -> P x -> P y
X0:P n
X1:P m
P (max n m) apply max_case_strong; auto. Defined.

max returns one of its arguments.

Lemma max_dec n m : {max n m == n} + {max n m == m}.n, m:t
{max n m == n} + {max n m == m}
Proof.n, m:t
{max n m == n} + {max n m == m}
 apply max_case; auto with relations.n, m:t
forall x y : t,
x == y -> {x == n} + {x == m} -> {y == n} + {y == m}
 intros x y H [E|E]; [left|right]; rewrite <-H; auto.
Defined.

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).n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m)
Proof.n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m)
intros Compat Hl Hr.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
P (min n m)
destruct (CompSpec2Type (compare_spec n m)) as [EQ|LT|GT].n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
EQ:n == m
P (min n m)
n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
LT:n < m
P (min n m)
n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
GT:m < n
P (min n m)
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
EQ:n == m
P (min n m) assert (n<=m) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
EQ:n == m
H:n <= m
P (min n m)
  apply (Compat n), Hl; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
EQ:n == m
H:n <= m
n == min n m symmetry; apply min_l; auto.
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
LT:n < m
P (min n m) assert (n<=m) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
LT:n < m
H:n <= m
P (min n m)
  apply (Compat n), Hl; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
LT:n < m
H:n <= m
n == min n m symmetry; apply min_l; auto.
-n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
GT:m < n
P (min n m) assert (m<=n) by (rewrite le_lteq; auto).n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
GT:m < n
H:m <= n
P (min n m)
  apply (Compat m), Hr; auto.n, m:t
P:t -> Type
Compat:forall x y : t, x == y -> P x -> P y
Hl:n <= m -> P n
Hr:m <= n -> P m
GT:m < n
H:m <= n
m == min n m symmetry; apply min_r; auto.
Defined.

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).n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
P n -> P m -> P (min n m)
Proof.n, m:t
P:t -> Type
(forall x y : t, x == y -> P x -> P y) ->
P n -> P m -> P (min n m) intros.n, m:t
P:t -> Type
X:forall x y : t, x == y -> P x -> P y
X0:P n
X1:P m
P (min n m) apply min_case_strong; auto. Defined.

Lemma min_dec n m : {min n m == n} + {min n m == m}.n, m:t
{min n m == n} + {min n m == m}
Proof.n, m:t
{min n m == n} + {min n m == m}
 intros.n, m:t
{min n m == n} + {min n m == m} apply min_case; auto with relations.n, m:t
forall x y : t,
x == y -> {x == n} + {x == m} -> {y == n} + {y == m}
 intros x y H [E|E]; [left|right]; rewrite <- E; auto with relations.
Defined.

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).f:t -> t
Proper (le ==> le) f ->
forall x y : t, max (f x) (f y) = f (max x y)
 Proof.f:t -> t
Proper (le ==> le) f ->
forall x y : t, max (f x) (f y) = f (max x y) intros; apply max_mono; auto.f:t -> t
H:Proper (le ==> le) f
x, y:t
Proper (Logic.eq ==> Logic.eq) f congruence. Qed.

 Lemma min_monotone f : Proper (le ==> le) f ->
  forall x y, min (f x) (f y) = f (min x y).f:t -> t
Proper (le ==> le) f ->
forall x y : t, min (f x) (f y) = f (min x y)
 Proof.f:t -> t
Proper (le ==> le) f ->
forall x y : t, min (f x) (f y) = f (min x y) intros; apply min_mono; auto.f:t -> t
H:Proper (le ==> le) f
x, y:t
Proper (Logic.eq ==> Logic.eq) f congruence. Qed.

 Lemma min_max_antimonotone f : Proper (le ==> flip le) f ->
  forall x y, min (f x) (f y) = f (max x y).f:t -> t
Proper (le ==> flip le) f ->
forall x y : t, min (f x) (f y) = f (max x y)
 Proof.f:t -> t
Proper (le ==> flip le) f ->
forall x y : t, min (f x) (f y) = f (max x y) intros; apply min_max_antimono; auto.f:t -> t
H:Proper (le ==> flip le) f
x, y:t
Proper (Logic.eq ==> Logic.eq) f congruence. Qed.

 Lemma max_min_antimonotone f : Proper (le ==> flip le) f ->
  forall x y, max (f x) (f y) = f (min x y).f:t -> t
Proper (le ==> flip le) f ->
forall x y : t, max (f x) (f y) = f (min x y)
 Proof.f:t -> t
Proper (le ==> flip le) f ->
forall x y : t, max (f x) (f y) = f (min x y) intros; apply max_min_antimono; auto.f:t -> t
H:Proper (le ==> flip le) f
x, y:t
Proper (Logic.eq ==> Logic.eq) f congruence. Qed.

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).forall (n m : t) (P : t -> Type),
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m)
 Proof.forall (n m : t) (P : t -> Type),
(m <= n -> P n) -> (n <= m -> P m) -> P (max n m) intros; apply max_case_strong; auto.n, m:t
P:t -> Type
X:m <= n -> P n
X0:n <= m -> P m
forall x y : t, x = y -> P x -> P y congruence. Defined.

 Lemma max_case : forall n m (P:t -> Type),
  P n -> P m -> P (max n m).forall (n m : t) (P : t -> Type),
P n -> P m -> P (max n m)
 Proof.forall (n m : t) (P : t -> Type),
P n -> P m -> P (max n m) intros; apply max_case_strong; auto. Defined.

 Lemma max_dec : forall n m, {max n m = n} + {max n m = m}.forall n m : t, {max n m = n} + {max n m = m}
 Proof.forall n m : t, {max n m = n} + {max n m = m} exact max_dec. Defined.

 Lemma min_case_strong : forall n m (P:O.t -> Type),
  (n<=m -> P n) -> (m<=n -> P m) -> P (min n m).forall (n m : t) (P : t -> Type),
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m)
 Proof.forall (n m : t) (P : t -> Type),
(n <= m -> P n) -> (m <= n -> P m) -> P (min n m) intros; apply min_case_strong; auto.n, m:t
P:t -> Type
X:n <= m -> P n
X0:m <= n -> P m
forall x y : t, x = y -> P x -> P y congruence. Defined.

 Lemma min_case : forall n m (P:O.t -> Type),
  P n -> P m -> P (min n m).forall (n m : t) (P : t -> Type),
P n -> P m -> P (min n m)
 Proof.forall (n m : t) (P : t -> Type),
P n -> P m -> P (min n m) intros.n, m:t
P:t -> Type
X:P n
X0:P m
P (min n m) apply min_case_strong; auto. Defined.

 Lemma min_dec : forall n m, {min n m = n} + {min n m = m}.forall n m : t, {min n m = n} + {min n m = m}
 Proof.forall n m : t, {min n m = n} + {min n m = m} exact min_dec. Defined.

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).forall x y : t, CompSpec eq lt x y (compare x y)
 Proof.forall x y : t, CompSpec eq lt x y (compare x y)
 intros; unfold compare; repeat destruct eq_dec; auto; constructor.x, y:t
n:x ~= y
e:max x y == y
x < y
x, y:t
n:x ~= y
n0:max x y ~= y
y < x
 -x, y:t
n:x ~= y
e:max x y == y
x < y destruct (lt_total x y); auto.x, y:t
n:x ~= y
e:max x y == y
H:x == y \/ y < x
x < y
   absurd (x==y); auto.x, y:t
n:x ~= y
e:max x y == y
H:x == y \/ y < x
x == y transitivity (max x y); auto.x, y:t
n:x ~= y
e:max x y == y
H:x == y \/ y < x
x == max x y
   symmetry.x, y:t
n:x ~= y
e:max x y == y
H:x == y \/ y < x
max x y == x apply max_l.x, y:t
n:x ~= y
e:max x y == y
H:x == y \/ y < x
y <= x rewrite le_lteq; intuition.
 -x, y:t
n:x ~= y
n0:max x y ~= y
y < x destruct (lt_total y x); auto.x, y:t
n:x ~= y
n0:max x y ~= y
H:y == x \/ x < y
y < x
   absurd (max x y == y); auto.x, y:t
n:x ~= y
n0:max x y ~= y
H:y == x \/ x < y
max x y == y apply max_r; rewrite le_lteq; intuition.
 Qed.

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 ?