Library Coq.Reals.Rminmax
Require
Import
Orders
Rbase
Rbasic_fun
ROrderedType
GenericMinMax
.
Maximum and Minimum of two real numbers
Local
Open
Scope
R_scope
.
The functions
Rmax
and
Rmin
implement indeed a maximum and a minimum
Lemma
Rmax_l
:
forall
x
y
,
y
<=
x
->
Rmax
x
y
=
x
.
Lemma
Rmax_r
:
forall
x
y
,
x
<=
y
->
Rmax
x
y
=
y
.
Lemma
Rmin_l
:
forall
x
y
,
x
<=
y
->
Rmin
x
y
=
x
.
Lemma
Rmin_r
:
forall
x
y
,
y
<=
x
->
Rmin
x
y
=
y
.
Module
RHasMinMax
<:
HasMinMax
R_as_OT
.
Definition
max
:=
Rmax
.
Definition
min
:=
Rmin
.
Definition
max_l
:=
Rmax_l
.
Definition
max_r
:=
Rmax_r
.
Definition
min_l
:=
Rmin_l
.
Definition
min_r
:=
Rmin_r
.
End
RHasMinMax
.
Module
R
.
We obtain hence all the generic properties of max and min.
Include
UsualMinMaxProperties
R_as_OT
RHasMinMax
.
Properties specific to the
R
domain
Compatibilities (consequences of monotonicity)
Lemma
plus_max_distr_l
:
forall
n
m
p
,
Rmax
(
p
+
n
) (
p
+
m
)
=
p
+
Rmax
n
m
.
Lemma
plus_max_distr_r
:
forall
n
m
p
,
Rmax
(
n
+
p
) (
m
+
p
)
=
Rmax
n
m
+
p
.
Lemma
plus_min_distr_l
:
forall
n
m
p
,
Rmin
(
p
+
n
) (
p
+
m
)
=
p
+
Rmin
n
m
.
Lemma
plus_min_distr_r
:
forall
n
m
p
,
Rmin
(
n
+
p
) (
m
+
p
)
=
Rmin
n
m
+
p
.
Anti-monotonicity swaps the role of
min
and
max
Lemma
opp_max_distr
:
forall
n
m
:
R
,
-(
Rmax
n
m
)
=
Rmin
(
-
n
) (
-
m
).
Lemma
opp_min_distr
:
forall
n
m
:
R
,
-
(
Rmin
n
m
)
=
Rmax
(
-
n
) (
-
m
).
Lemma
minus_max_distr_l
:
forall
n
m
p
,
Rmax
(
p
-
n
) (
p
-
m
)
=
p
-
Rmin
n
m
.
Lemma
minus_max_distr_r
:
forall
n
m
p
,
Rmax
(
n
-
p
) (
m
-
p
)
=
Rmax
n
m
-
p
.
Lemma
minus_min_distr_l
:
forall
n
m
p
,
Rmin
(
p
-
n
) (
p
-
m
)
=
p
-
Rmax
n
m
.
Lemma
minus_min_distr_r
:
forall
n
m
p
,
Rmin
(
n
-
p
) (
m
-
p
)
=
Rmin
n
m
-
p
.
End
R
.