Library Coq.Reals.Abstract.ConstructiveMinMax
Require
Import
QArith
.
Require
Import
Qabs
.
Require
Import
ConstructiveReals
.
Require
Import
ConstructiveAbs
.
Require
Import
ConstructiveRealsMorphisms
.
Local Open
Scope
ConstructiveReals
.
Definition and properties of minimum and maximum.
WARNING: this file is experimental and likely to change in future releases.
Definition
CRmin
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
) :
CRcarrier
R
:=
(
x
+
y
-
CRabs
_
(
y
-
x
)
)
*
CR_of_Q
_
(1
#
2).
Lemma
CRmin_lt_r
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRmin
x
y
<
y
->
CRmin
x
y
==
x
.
Add
Parametric
Morphism
{
R
:
ConstructiveReals
} :
CRmin
with
signature
(
CReq
R
)
==>
(
CReq
R
)
==>
(
CReq
R
)
as
CRmin_morph
.
Instance
CRmin_morphT
:
forall
{
R
:
ConstructiveReals
},
CMorphisms.Proper
(
CMorphisms.respectful
(
CReq
R
) (
CMorphisms.respectful
(
CReq
R
) (
CReq
R
))) (@
CRmin
R
).
Lemma
CRmin_l
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRmin
x
y
<=
x
.
Lemma
CRmin_r
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRmin
x
y
<=
y
.
Lemma
CRnegPartAbsMin
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
CRmin
0
x
==
(
x
-
CRabs
_
x
)
*
(
CR_of_Q
_
(1
#
2)
)
.
Lemma
CRmin_sym
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRmin
x
y
==
CRmin
y
x
.
Lemma
CRmin_mult
:
forall
{
R
:
ConstructiveReals
} (
p
q
r
:
CRcarrier
R
),
0
<=
r
->
CRmin
(
r
*
p
) (
r
*
q
)
==
r
*
CRmin
p
q
.
Lemma
CRmin_plus
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
x
+
CRmin
y
z
==
CRmin
(
x
+
y
) (
x
+
z
).
Lemma
CRmin_left
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
x
<=
y
->
CRmin
x
y
==
x
.
Lemma
CRmin_right
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
y
<=
x
->
CRmin
x
y
==
y
.
Lemma
CRmin_lt
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
z
<
x
->
z
<
y
->
z
<
CRmin
x
y
.
Lemma
CRmin_contract
:
forall
{
R
:
ConstructiveReals
} (
x
y
a
:
CRcarrier
R
),
CRabs
_
(
CRmin
x
a
-
CRmin
y
a
)
<=
CRabs
_
(
x
-
y
).
Lemma
CRmin_glb
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
z
<=
x
->
z
<=
y
->
z
<=
CRmin
x
y
.
Lemma
CRmin_assoc
:
forall
{
R
:
ConstructiveReals
} (
a
b
c
:
CRcarrier
R
),
CRmin
a
(
CRmin
b
c
)
==
CRmin
(
CRmin
a
b
)
c
.
Lemma
CRlt_min
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
z
<
CRmin
x
y
->
prod
(
z
<
x
) (
z
<
y
).
Definition
CRmax
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
) :
CRcarrier
R
:=
(
x
+
y
+
CRabs
_
(
y
-
x
)
)
*
CR_of_Q
_
(1
#
2).
Add
Parametric
Morphism
{
R
:
ConstructiveReals
} :
CRmax
with
signature
(
CReq
R
)
==>
(
CReq
R
)
==>
(
CReq
R
)
as
CRmax_morph
.
Instance
CRmax_morphT
:
forall
{
R
:
ConstructiveReals
},
CMorphisms.Proper
(
CMorphisms.respectful
(
CReq
R
) (
CMorphisms.respectful
(
CReq
R
) (
CReq
R
))) (@
CRmax
R
).
Lemma
CRmax_lub
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
x
<=
z
->
y
<=
z
->
CRmax
x
y
<=
z
.
Lemma
CRmax_l
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
x
<=
CRmax
x
y
.
Lemma
CRmax_r
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
y
<=
CRmax
x
y
.
Lemma
CRposPartAbsMax
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
CRmax
0
x
==
(
x
+
CRabs
_
x
)
*
(
CR_of_Q
R
(1
#
2)
)
.
Lemma
CRmax_sym
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRmax
x
y
==
CRmax
y
x
.
Lemma
CRmax_plus
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
x
+
CRmax
y
z
==
CRmax
(
x
+
y
) (
x
+
z
).
Lemma
CRmax_left
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
y
<=
x
->
CRmax
x
y
==
x
.
Lemma
CRmax_right
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
x
<=
y
->
CRmax
x
y
==
y
.
Lemma
CRmax_contract
:
forall
{
R
:
ConstructiveReals
} (
x
y
a
:
CRcarrier
R
),
CRabs
_
(
CRmax
x
a
-
CRmax
y
a
)
<=
CRabs
_
(
x
-
y
).
Lemma
CRmax_lub_lt
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
x
<
z
->
y
<
z
->
CRmax
x
y
<
z
.
Lemma
CRmax_assoc
:
forall
{
R
:
ConstructiveReals
} (
a
b
c
:
CRcarrier
R
),
CRmax
a
(
CRmax
b
c
)
==
CRmax
(
CRmax
a
b
)
c
.
Lemma
CRmax_min_mult_neg
:
forall
{
R
:
ConstructiveReals
} (
p
q
r
:
CRcarrier
R
),
r
<=
0
->
CRmax
(
r
*
p
) (
r
*
q
)
==
r
*
CRmin
p
q
.
Lemma
CRlt_max
:
forall
{
R
:
ConstructiveReals
} (
x
y
z
:
CRcarrier
R
),
CRmax
x
y
<
z
->
prod
(
x
<
z
) (
y
<
z
).
Lemma
CRmax_mult
:
forall
{
R
:
ConstructiveReals
} (
p
q
r
:
CRcarrier
R
),
0
<=
r
->
CRmax
(
r
*
p
) (
r
*
q
)
==
r
*
CRmax
p
q
.
Lemma
CRmin_max_mult_neg
:
forall
{
R
:
ConstructiveReals
} (
p
q
r
:
CRcarrier
R
),
r
<=
0
->
CRmin
(
r
*
p
) (
r
*
q
)
==
r
*
CRmax
p
q
.
Lemma
CRmorph_min
:
forall
{
R1
R2
:
ConstructiveReals
}
(
f
: @
ConstructiveRealsMorphism
R1
R2
)
(
a
b
:
CRcarrier
R1
),
CRmorph
f
(
CRmin
a
b
)
==
CRmin
(
CRmorph
f
a
) (
CRmorph
f
b
).