Library Coq.Numbers.DecimalR
DecimalR
Proofs that conversions between decimal numbers and
R
are bijections.
Require
Import
Decimal
DecimalFacts
DecimalPos
DecimalZ
DecimalQ
Rdefinitions
.
Lemma
of_IQmake_to_decimal
num
den
:
match
IQmake_to_decimal
num
den
with
|
None
=>
True
|
Some
(
DecimalExp
_
_
_
) =>
False
|
Some
(
Decimal
i
f
) =>
of_decimal
(
Decimal
i
f
)
=
IRQ
(
QArith_base.Qmake
num
den
)
end
.
Lemma
of_to
(
q
:
IR
) :
forall
d
,
to_decimal
q
=
Some
d
->
of_decimal
d
=
q
.
Lemma
to_of
(
d
:
decimal
) :
to_decimal
(
of_decimal
d
)
=
Some
(
dnorm
d
).
Some consequences
Lemma
to_decimal_inj
q
q'
:
to_decimal
q
<>
None
->
to_decimal
q
=
to_decimal
q'
->
q
=
q'
.
Lemma
to_decimal_surj
d
:
exists
q
,
to_decimal
q
=
Some
(
dnorm
d
).
Lemma
of_decimal_dnorm
d
:
of_decimal
(
dnorm
d
)
=
of_decimal
d
.
Lemma
of_inj
d
d'
:
of_decimal
d
=
of_decimal
d'
->
dnorm
d
=
dnorm
d'
.
Lemma
of_iff
d
d'
:
of_decimal
d
=
of_decimal
d'
<->
dnorm
d
=
dnorm
d'
.