Library Coq.Numbers.HexadecimalR
HexadecimalR
Proofs that conversions between hexadecimal numbers and
R
are bijections.
Require
Import
Decimal
DecimalFacts
.
Require
Import
Hexadecimal
HexadecimalFacts
HexadecimalPos
HexadecimalZ
.
Require
Import
HexadecimalQ
Rdefinitions
.
Lemma
of_IQmake_to_hexadecimal
num
den
:
match
IQmake_to_hexadecimal
num
den
with
|
None
=>
True
|
Some
(
HexadecimalExp
_
_
_
) =>
False
|
Some
(
Hexadecimal
i
f
) =>
of_hexadecimal
(
Hexadecimal
i
f
)
=
IRQ
(
QArith_base.Qmake
num
den
)
end
.
Lemma
of_to
(
q
:
IR
) :
forall
d
,
to_hexadecimal
q
=
Some
d
->
of_hexadecimal
d
=
q
.
Lemma
to_of
(
d
:
hexadecimal
) :
to_hexadecimal
(
of_hexadecimal
d
)
=
Some
(
dnorm
d
).
Some consequences
Lemma
to_hexadecimal_inj
q
q'
:
to_hexadecimal
q
<>
None
->
to_hexadecimal
q
=
to_hexadecimal
q'
->
q
=
q'
.
Lemma
to_hexadecimal_surj
d
:
exists
q
,
to_hexadecimal
q
=
Some
(
dnorm
d
).
Lemma
of_hexadecimal_dnorm
d
:
of_hexadecimal
(
dnorm
d
)
=
of_hexadecimal
d
.
Lemma
of_inj
d
d'
:
of_hexadecimal
d
=
of_hexadecimal
d'
->
dnorm
d
=
dnorm
d'
.
Lemma
of_iff
d
d'
:
of_hexadecimal
d
=
of_hexadecimal
d'
<->
dnorm
d
=
dnorm
d'
.