Library Coq.Numbers.HexadecimalQ
HexadecimalQ
Proofs that conversions between hexadecimal numbers and
Q
are bijections.
Require
Import
Decimal
DecimalFacts
DecimalPos
DecimalN
DecimalZ
.
Require
Import
Hexadecimal
HexadecimalFacts
HexadecimalPos
HexadecimalN
HexadecimalZ
QArith
.
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
)
=
IQmake
(
IZ_of_Z
num
)
den
end
.
Lemma
IZ_of_Z_IZ_to_Z
z
z'
:
IZ_to_Z
z
=
Some
z'
->
IZ_of_Z
z'
=
z
.
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
)
=
IQmake
num
den
end
.
Lemma
of_to
(
q
:
IQ
) :
forall
d
,
to_hexadecimal
q
=
Some
d
->
of_hexadecimal
d
=
q
.
Definition
dnorm
(
d
:
hexadecimal
) :
hexadecimal
:=
let
norm_i
i
f
:=
match
i
with
|
Pos
i
=>
Pos
(
unorm
i
)
|
Neg
i
=>
match
nzhead
(
app
i
f
)
with
Nil
=>
Pos
zero
|
_
=>
Neg
(
unorm
i
)
end
end
in
match
d
with
|
Hexadecimal
i
f
=>
Hexadecimal
(
norm_i
i
f
)
f
|
HexadecimalExp
i
f
e
=>
match
Decimal.norm
e
with
|
Decimal.Pos
Decimal.zero
=>
Hexadecimal
(
norm_i
i
f
)
f
|
e
=>
HexadecimalExp
(
norm_i
i
f
)
f
e
end
end
.
Lemma
dnorm_spec_i
d
:
let
(
i
,
f
) :=
match
d
with
Hexadecimal
i
f
=>
(
i
,
f
)
|
HexadecimalExp
i
f
_
=>
(
i
,
f
)
end
in
let
i'
:=
match
dnorm
d
with
Hexadecimal
i
_
=>
i
|
HexadecimalExp
i
_
_
=>
i
end
in
match
i
with
|
Pos
i
=>
i'
=
Pos
(
unorm
i
)
|
Neg
i
=>
(
i'
=
Neg
(
unorm
i
)
/\
(
nzhead
i
<>
Nil
\/
nzhead
f
<>
Nil
)
)
\/
(
i'
=
Pos
zero
/\
(
nzhead
i
=
Nil
/\
nzhead
f
=
Nil
)
)
end
.
Lemma
dnorm_spec_f
d
:
let
f
:=
match
d
with
Hexadecimal
_
f
=>
f
|
HexadecimalExp
_
f
_
=>
f
end
in
let
f'
:=
match
dnorm
d
with
Hexadecimal
_
f
=>
f
|
HexadecimalExp
_
f
_
=>
f
end
in
f'
=
f
.
Lemma
dnorm_spec_e
d
:
match
d
,
dnorm
d
with
|
Hexadecimal
_
_
,
Hexadecimal
_
_
=>
True
|
HexadecimalExp
_
_
e
,
Hexadecimal
_
_
=>
Decimal.norm
e
=
Decimal.Pos
Decimal.zero
|
HexadecimalExp
_
_
e
,
HexadecimalExp
_
_
e'
=>
e'
=
Decimal.norm
e
/\
e'
<>
Decimal.Pos
Decimal.zero
|
Hexadecimal
_
_
,
HexadecimalExp
_
_
_
=>
False
end
.
Lemma
dnorm_involutive
d
:
dnorm
(
dnorm
d
)
=
dnorm
d
.
Lemma
IZ_to_Z_IZ_of_Z
z
:
IZ_to_Z
(
IZ_of_Z
z
)
=
Some
z
.
Lemma
dnorm_i_exact
i
f
:
(
nb_digits
f
<
nb_digits
(
unorm
(
app
(
abs
i
)
f
)))%
nat
->
match
i
with
|
Pos
i
=>
Pos
(
unorm
i
)
|
Neg
i
=>
match
nzhead
(
app
i
f
)
with
|
Nil
=>
Pos
zero
|
_
=>
Neg
(
unorm
i
)
end
end
=
norm
i
.
Lemma
dnorm_i_exact'
i
f
:
(
nb_digits
(
unorm
(
app
(
abs
i
)
f
))
<=
nb_digits
f
)%
nat
->
match
i
with
|
Pos
i
=>
Pos
(
unorm
i
)
|
Neg
i
=>
match
nzhead
(
app
i
f
)
with
|
Nil
=>
Pos
zero
|
_
=>
Neg
(
unorm
i
)
end
end
=
match
norm
(
app_int
i
f
)
with
|
Pos
_
=>
Pos
zero
|
Neg
_
=>
Neg
zero
end
.
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'
.