Library Coq.QArith.Qcabs
An absolute value for normalized rational numbers.
Contributed by Cédric Auger
Require
Import
Qabs
Qcanon
.
Lemma
Qred_abs
(
x
:
Q
) :
Qred
(
Qabs
x
)
=
Qabs
(
Qred
x
).
Lemma
Qcabs_canon
(
x
:
Q
) :
Qred
x
=
x
->
Qred
(
Qabs
x
)
=
Qabs
x
.
Definition
Qcabs
(
x
:
Qc
) :
Qc
:= {|
canon
:=
Qcabs_canon
x
(
canon
x
) |}.
Notation
"
[ q ]" := (
Qcabs
q
) :
Qc_scope
.
Ltac
Qc_unfolds
:=
unfold
Qcabs
,
Qcminus
,
Qcopp
,
Qcplus
,
Qcmult
,
Qcle
,
Q2Qc
,
this
.
Lemma
Qcabs_case
(
x
:
Qc
) (
P
:
Qc
->
Type
) :
(
0
<=
x
->
P
x
)
->
(
x
<=
0
->
P
(
-
x
)
)
->
P
[
x
]
.
Lemma
Qcabs_pos
x
: 0
<=
x
->
[
x
]
=
x
.
Lemma
Qcabs_neg
x
:
x
<=
0
->
[
x
]
=
-
x
.
Lemma
Qcabs_nonneg
x
: 0
<=
[
x
]
.
Lemma
Qcabs_opp
x
:
[(
-
x
)]
=
[
x
]
.
Lemma
Qcabs_triangle
x
y
:
[
x
+
y
]
<=
[
x
]
+
[
y
]
.
Lemma
Qcabs_Qcmult
x
y
:
[
x
*
y
]
=
[
x
]
*
[
y
]
.
Lemma
Qcabs_Qcminus
x
y
:
[
x
-
y
]
=
[
y
-
x
]
.
Lemma
Qcle_Qcabs
x
:
x
<=
[
x
]
.
Lemma
Qcabs_triangle_reverse
x
y
:
[
x
]
-
[
y
]
<=
[
x
-
y
]
.
Lemma
Qcabs_Qcle_condition
x
y
:
[
x
]
<=
y
<->
-
y
<=
x
<=
y
.
Lemma
Qcabs_diff_Qcle_condition
x
y
r
:
[
x
-
y
]
<=
r
<->
x
-
r
<=
y
<=
x
+
r
.
Lemma
Qcabs_null
x
:
[
x
]
=
0
->
x
=
0.