Library Coq.Structures.GenericMinMax
A Generic construction of min and max
First, an interface for types with max and/or min
Any OrderedTypeFull can be equipped by max and min
based on the compare function.
Consequences of the minimalist interface: facts about max.
An alternative caracterisation 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.
A function satisfying the same specification is equal to max.
max commutes with monotone functions.
Semi-lattice algebraic properties of max
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
Distributivity
Modularity
Disassociativity
Anti-monotonicity swaps the role of min and max
Properties requiring a decidable order
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.
Idem for min
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.
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 ?