Library Coq.Numbers.HexadecimalZ
HexadecimalZ
Proofs that conversions between hexadecimal numbers and
Z
are bijections.
Require
Import
Hexadecimal
HexadecimalFacts
HexadecimalPos
HexadecimalN
ZArith
.
Lemma
of_to
(
z
:
Z
) :
Z.of_hex_int
(
Z.to_hex_int
z
)
=
z
.
Lemma
to_of
(
d
:
int
) :
Z.to_hex_int
(
Z.of_hex_int
d
)
=
norm
d
.
Some consequences
Lemma
to_int_inj
n
n'
:
Z.to_hex_int
n
=
Z.to_hex_int
n'
->
n
=
n'
.
Lemma
to_int_surj
d
:
exists
n
,
Z.to_hex_int
n
=
norm
d
.
Lemma
of_int_norm
d
:
Z.of_hex_int
(
norm
d
)
=
Z.of_hex_int
d
.
Lemma
of_inj
d
d'
:
Z.of_hex_int
d
=
Z.of_hex_int
d'
->
norm
d
=
norm
d'
.
Lemma
of_iff
d
d'
:
Z.of_hex_int
d
=
Z.of_hex_int
d'
<->
norm
d
=
norm
d'
.
Various lemmas
Lemma
of_hex_uint_iter_D0
d
n
:
Z.of_hex_uint
(
app
d
(
Nat.iter
n
D0
Nil
))
=
Nat.iter
n
(
Z.mul
0
x10
) (
Z.of_hex_uint
d
).
Lemma
of_hex_int_iter_D0
d
n
:
Z.of_hex_int
(
app_int
d
(
Nat.iter
n
D0
Nil
))
=
Nat.iter
n
(
Z.mul
0
x10
) (
Z.of_hex_int
d
).
Definition
double
d
:=
match
d
with
|
Pos
u
=>
Pos
(
Unsigned.double
u
)
|
Neg
u
=>
Neg
(
Unsigned.double
u
)
end
.
Lemma
double_norm
d
:
double
(
norm
d
)
=
norm
(
double
d
).
Lemma
of_hex_int_double
d
:
Z.of_hex_int
(
double
d
)
=
Z.double
(
Z.of_hex_int
d
).
Lemma
double_to_hex_int
n
:
double
(
Z.to_hex_int
n
)
=
Z.to_hex_int
(
Z.double
n
).