Library Coq.Reals.Abstract.ConstructiveAbs
Require
Import
QArith
.
Require
Import
Qabs
.
Require
Import
ConstructiveReals
.
Local Open
Scope
ConstructiveReals
.
Properties of constructive absolute value (defined in ConstructiveReals.CRabs). Definition of minimum, maximum and their properties.
WARNING: this file is experimental and likely to change in future releases.
Instance
CRabs_morph
:
forall
{
R
:
ConstructiveReals
},
CMorphisms.Proper
(
CMorphisms.respectful
(
CReq
R
) (
CReq
R
)) (
CRabs
R
).
Add
Parametric
Morphism
{
R
:
ConstructiveReals
} : (
CRabs
R
)
with
signature
CReq
R
==>
CReq
R
as
CRabs_morph_prop
.
Lemma
CRabs_right
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
0
<=
x
->
CRabs
R
x
==
x
.
Lemma
CRabs_opp
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
CRabs
R
(
-
x
)
==
CRabs
R
x
.
Lemma
CRabs_minus_sym
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
R
(
x
-
y
)
==
CRabs
R
(
y
-
x
).
Lemma
CRabs_left
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
x
<=
0
->
CRabs
R
x
==
-
x
.
Lemma
CRabs_triang
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
R
(
x
+
y
)
<=
CRabs
R
x
+
CRabs
R
y
.
Lemma
CRabs_le
:
forall
{
R
:
ConstructiveReals
} (
a
b
:
CRcarrier
R
),
(
-
b
<=
a
/\
a
<=
b
)
->
CRabs
R
a
<=
b
.
Lemma
CRabs_triang_inv
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
R
x
-
CRabs
R
y
<=
CRabs
R
(
x
-
y
).
Lemma
CRabs_triang_inv2
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
R
(
CRabs
R
x
-
CRabs
R
y
)
<=
CRabs
R
(
x
-
y
).
Lemma
CR_of_Q_abs
:
forall
{
R
:
ConstructiveReals
} (
q
:
Q
),
CRabs
R
(
CR_of_Q
R
q
)
==
CR_of_Q
R
(
Qabs
q
).
Lemma
CRle_abs
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
x
<=
CRabs
R
x
.
Lemma
CRabs_pos
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
0
<=
CRabs
R
x
.
Lemma
CRabs_appart_0
:
forall
{
R
:
ConstructiveReals
} (
x
:
CRcarrier
R
),
0
<
CRabs
R
x
->
x
≶
0.
Lemma
CRabs_mult
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
R
(
x
*
y
)
==
CRabs
R
x
*
CRabs
R
y
.
Lemma
CRabs_lt
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
CRabs
_
x
<
y
->
prod
(
x
<
y
) (
-
x
<
y
).
Lemma
CRabs_def1
:
forall
{
R
:
ConstructiveReals
} (
x
y
:
CRcarrier
R
),
x
<
y
->
-
x
<
y
->
CRabs
_
x
<
y
.
Lemma
CRabs_def2
:
forall
{
R
:
ConstructiveReals
} (
x
a
:
CRcarrier
R
),
CRabs
_
x
<=
a
->
(
x
<=
a
)
/\
(
-
a
<=
x
)
.