Library Coq.Numbers.HexadecimalFacts
HexadecimalFacts : some facts about Hexadecimal numbers
Require
Import
Hexadecimal
Arith
ZArith
.
Variant
digits
:=
|
d0
|
d1
|
d2
|
d3
|
d4
|
d5
|
d6
|
d7
|
d8
|
d9
|
da
|
db
|
dc
|
dd
|
de
|
df
.
Fixpoint
to_list
(
u
:
uint
) :
list
digits
:=
match
u
with
|
Nil
=>
nil
|
D0
u
=>
cons
d0
(
to_list
u
)
|
D1
u
=>
cons
d1
(
to_list
u
)
|
D2
u
=>
cons
d2
(
to_list
u
)
|
D3
u
=>
cons
d3
(
to_list
u
)
|
D4
u
=>
cons
d4
(
to_list
u
)
|
D5
u
=>
cons
d5
(
to_list
u
)
|
D6
u
=>
cons
d6
(
to_list
u
)
|
D7
u
=>
cons
d7
(
to_list
u
)
|
D8
u
=>
cons
d8
(
to_list
u
)
|
D9
u
=>
cons
d9
(
to_list
u
)
|
Da
u
=>
cons
da
(
to_list
u
)
|
Db
u
=>
cons
db
(
to_list
u
)
|
Dc
u
=>
cons
dc
(
to_list
u
)
|
Dd
u
=>
cons
dd
(
to_list
u
)
|
De
u
=>
cons
de
(
to_list
u
)
|
Df
u
=>
cons
df
(
to_list
u
)
end
.
Fixpoint
of_list
(
l
:
list
digits
) :
uint
:=
match
l
with
|
nil
=>
Nil
|
cons
d0
l
=>
D0
(
of_list
l
)
|
cons
d1
l
=>
D1
(
of_list
l
)
|
cons
d2
l
=>
D2
(
of_list
l
)
|
cons
d3
l
=>
D3
(
of_list
l
)
|
cons
d4
l
=>
D4
(
of_list
l
)
|
cons
d5
l
=>
D5
(
of_list
l
)
|
cons
d6
l
=>
D6
(
of_list
l
)
|
cons
d7
l
=>
D7
(
of_list
l
)
|
cons
d8
l
=>
D8
(
of_list
l
)
|
cons
d9
l
=>
D9
(
of_list
l
)
|
cons
da
l
=>
Da
(
of_list
l
)
|
cons
db
l
=>
Db
(
of_list
l
)
|
cons
dc
l
=>
Dc
(
of_list
l
)
|
cons
dd
l
=>
Dd
(
of_list
l
)
|
cons
de
l
=>
De
(
of_list
l
)
|
cons
df
l
=>
Df
(
of_list
l
)
end
.
Lemma
of_list_to_list
u
:
of_list
(
to_list
u
)
=
u
.
Lemma
to_list_of_list
l
:
to_list
(
of_list
l
)
=
l
.
Lemma
to_list_inj
u
u'
:
to_list
u
=
to_list
u'
->
u
=
u'
.
Lemma
of_list_inj
u
u'
:
of_list
u
=
of_list
u'
->
u
=
u'
.
Lemma
nb_digits_spec
u
:
nb_digits
u
=
length
(
to_list
u
).
Fixpoint
lnzhead
l
:=
match
l
with
|
nil
=>
nil
|
cons
d
l'
=>
match
d
with
|
d0
=>
lnzhead
l'
|
_
=>
l
end
end
.
Lemma
nzhead_spec
u
:
to_list
(
nzhead
u
)
=
lnzhead
(
to_list
u
).
Definition
lzero
:=
cons
d0
nil
.
Definition
lunorm
l
:=
match
lnzhead
l
with
|
nil
=>
lzero
|
d
=>
d
end
.
Lemma
unorm_spec
u
:
to_list
(
unorm
u
)
=
lunorm
(
to_list
u
).
Lemma
revapp_spec
d
d'
:
to_list
(
revapp
d
d'
)
=
List.rev_append
(
to_list
d
) (
to_list
d'
).
Lemma
rev_spec
d
:
to_list
(
rev
d
)
=
List.rev
(
to_list
d
).
Lemma
app_spec
d
d'
:
to_list
(
app
d
d'
)
=
Datatypes.app
(
to_list
d
) (
to_list
d'
).
Definition
lnztail
l
:=
let
fix
aux
l_rev
:=
match
l_rev
with
|
cons
d0
l_rev
=>
let
(
r
,
n
) :=
aux
l_rev
in
pair
r
(
S
n
)
|
_
=>
pair
l_rev
O
end
in
let
(
r
,
n
) :=
aux
(
List.rev
l
)
in
pair
(
List.rev
r
)
n
.
Lemma
nztail_spec
d
:
let
(
r
,
n
) :=
nztail
d
in
let
(
r'
,
n'
) :=
lnztail
(
to_list
d
)
in
to_list
r
=
r'
/\
n
=
n'
.
Lemma
del_head_spec_0
d
:
del_head
0
d
=
d
.
Lemma
del_head_spec_small
n
d
:
n
<=
length
(
to_list
d
)
->
to_list
(
del_head
n
d
)
=
List.skipn
n
(
to_list
d
).
Lemma
del_head_spec_large
n
d
:
length
(
to_list
d
)
<
n
->
del_head
n
d
=
zero
.
Lemma
nb_digits_0
d
:
nb_digits
d
=
0
->
d
=
Nil
.
Lemma
nb_digits_n0
d
:
nb_digits
d
<>
0
->
d
<>
Nil
.
Lemma
nb_digits_iter_D0
n
d
:
nb_digits
(
Nat.iter
n
D0
d
)
=
n
+
nb_digits
d
.
Lemma
length_lnzhead
l
:
length
(
lnzhead
l
)
<=
length
l
.
Lemma
nb_digits_nzhead
u
:
nb_digits
(
nzhead
u
)
<=
nb_digits
u
.
Lemma
unorm_nzhead
u
:
nzhead
u
<>
Nil
->
unorm
u
=
nzhead
u
.
Lemma
nb_digits_unorm
u
:
u
<>
Nil
->
nb_digits
(
unorm
u
)
<=
nb_digits
u
.
Lemma
nb_digits_rev
d
:
nb_digits
(
rev
d
)
=
nb_digits
d
.
Lemma
nb_digits_del_head_sub
d
n
:
n
<=
nb_digits
d
->
nb_digits
(
del_head
(
nb_digits
d
-
n
)
d
)
=
n
.
Lemma
unorm_D0
u
:
unorm
(
D0
u
)
=
unorm
u
.
Lemma
app_nil_l
d
:
app
Nil
d
=
d
.
Lemma
app_nil_r
d
:
app
d
Nil
=
d
.
Lemma
abs_app_int
d
d'
:
abs
(
app_int
d
d'
)
=
app
(
abs
d
)
d'
.
Lemma
abs_norm
d
:
abs
(
norm
d
)
=
unorm
(
abs
d
).
Lemma
iter_D0_nzhead
d
:
Nat.iter
(
nb_digits
d
-
nb_digits
(
nzhead
d
))
D0
(
nzhead
d
)
=
d
.
Lemma
iter_D0_unorm
d
:
d
<>
Nil
->
Nat.iter
(
nb_digits
d
-
nb_digits
(
unorm
d
))
D0
(
unorm
d
)
=
d
.
Lemma
nzhead_app_l
d
d'
:
nb_digits
d'
<
nb_digits
(
nzhead
(
app
d
d'
))
->
nzhead
(
app
d
d'
)
=
app
(
nzhead
d
)
d'
.
Lemma
nzhead_app_r
d
d'
:
nb_digits
(
nzhead
(
app
d
d'
))
<=
nb_digits
d'
->
nzhead
(
app
d
d'
)
=
nzhead
d'
.
Lemma
nzhead_app_nil_r
d
d'
:
nzhead
(
app
d
d'
)
=
Nil
->
nzhead
d'
=
Nil
.
Lemma
nzhead_app_nil
d
d'
:
nb_digits
(
nzhead
(
app
d
d'
))
<=
nb_digits
d'
->
nzhead
d
=
Nil
.
Lemma
nzhead_app_nil_l
d
d'
:
nzhead
(
app
d
d'
)
=
Nil
->
nzhead
d
=
Nil
.
Lemma
unorm_app_zero
d
d'
:
nb_digits
(
unorm
(
app
d
d'
))
<=
nb_digits
d'
->
unorm
d
=
zero
.
Lemma
app_int_nil_r
d
:
app_int
d
Nil
=
d
.
Lemma
unorm_app_l
d
d'
:
nb_digits
d'
<
nb_digits
(
unorm
(
app
d
d'
))
->
unorm
(
app
d
d'
)
=
app
(
unorm
d
)
d'
.
Lemma
unorm_app_r
d
d'
:
nb_digits
(
unorm
(
app
d
d'
))
<=
nb_digits
d'
->
unorm
(
app
d
d'
)
=
unorm
d'
.
Lemma
norm_app_int
d
d'
:
nb_digits
d'
<
nb_digits
(
unorm
(
app
(
abs
d
)
d'
))
->
norm
(
app_int
d
d'
)
=
app_int
(
norm
d
)
d'
.
Lemma
del_head_nb_digits
d
:
del_head
(
nb_digits
d
)
d
=
Nil
.
Lemma
del_tail_nb_digits
d
:
del_tail
(
nb_digits
d
)
d
=
Nil
.
Lemma
del_head_app
n
d
d'
:
n
<=
nb_digits
d
->
del_head
n
(
app
d
d'
)
=
app
(
del_head
n
d
)
d'
.
Lemma
del_tail_app
n
d
d'
:
n
<=
nb_digits
d'
->
del_tail
n
(
app
d
d'
)
=
app
d
(
del_tail
n
d'
).
Lemma
del_tail_app_int
n
d
d'
:
n
<=
nb_digits
d'
->
del_tail_int
n
(
app_int
d
d'
)
=
app_int
d
(
del_tail
n
d'
).
Lemma
app_del_tail_head
n
(
d
:
uint
) :
n
<=
nb_digits
d
->
app
(
del_tail
n
d
) (
del_head
(
nb_digits
d
-
n
)
d
)
=
d
.
Lemma
app_int_del_tail_head
n
(
d
:
int
) :
n
<=
nb_digits
(
abs
d
)
->
app_int
(
del_tail_int
n
d
) (
del_head
(
nb_digits
(
abs
d
)
-
n
) (
abs
d
))
=
d
.
Lemma
del_head_app_int_exact
i
f
:
nb_digits
f
<
nb_digits
(
unorm
(
app
(
abs
i
)
f
))
->
del_head
(
nb_digits
(
unorm
(
app
(
abs
i
)
f
))
-
nb_digits
f
) (
unorm
(
app
(
abs
i
)
f
))
=
f
.
Lemma
del_tail_app_int_exact
i
f
:
nb_digits
f
<
nb_digits
(
unorm
(
app
(
abs
i
)
f
))
->
del_tail_int
(
nb_digits
f
) (
norm
(
app_int
i
f
))
=
norm
i
.
Normalization on little-endian numbers
Fixpoint
nztail
d
:=
match
d
with
|
Nil
=>
Nil
|
D0
d
=>
match
nztail
d
with
Nil
=>
Nil
|
d'
=>
D0
d'
end
|
D1
d
=>
D1
(
nztail
d
)
|
D2
d
=>
D2
(
nztail
d
)
|
D3
d
=>
D3
(
nztail
d
)
|
D4
d
=>
D4
(
nztail
d
)
|
D5
d
=>
D5
(
nztail
d
)
|
D6
d
=>
D6
(
nztail
d
)
|
D7
d
=>
D7
(
nztail
d
)
|
D8
d
=>
D8
(
nztail
d
)
|
D9
d
=>
D9
(
nztail
d
)
|
Da
d
=>
Da
(
nztail
d
)
|
Db
d
=>
Db
(
nztail
d
)
|
Dc
d
=>
Dc
(
nztail
d
)
|
Dd
d
=>
Dd
(
nztail
d
)
|
De
d
=>
De
(
nztail
d
)
|
Df
d
=>
Df
(
nztail
d
)
end
.
Definition
lnorm
d
:=
match
nztail
d
with
|
Nil
=>
zero
|
d
=>
d
end
.
Lemma
nzhead_revapp_0
d
d'
:
nztail
d
=
Nil
->
nzhead
(
revapp
d
d'
)
=
nzhead
d'
.
Lemma
nzhead_revapp
d
d'
:
nztail
d
<>
Nil
->
nzhead
(
revapp
d
d'
)
=
revapp
(
nztail
d
)
d'
.
Lemma
nzhead_rev
d
:
nztail
d
<>
Nil
->
nzhead
(
rev
d
)
=
rev
(
nztail
d
).
Lemma
rev_rev
d
:
rev
(
rev
d
)
=
d
.
Lemma
rev_nztail_rev
d
:
rev
(
nztail
(
rev
d
))
=
nzhead
d
.
Lemma
nzhead_D0
u
:
nzhead
(
D0
u
)
=
nzhead
u
.
Lemma
nzhead_iter_D0
n
u
:
nzhead
(
Nat.iter
n
D0
u
)
=
nzhead
u
.
Lemma
revapp_nil_inv
d
d'
:
revapp
d
d'
=
Nil
->
d
=
Nil
/\
d'
=
Nil
.
Lemma
rev_nil_inv
d
:
rev
d
=
Nil
->
d
=
Nil
.
Lemma
rev_lnorm_rev
d
:
rev
(
lnorm
(
rev
d
))
=
unorm
d
.
Lemma
nzhead_nonzero
d
d'
:
nzhead
d
<>
D0
d'
.
Lemma
unorm_0
d
:
unorm
d
=
zero
<->
nzhead
d
=
Nil
.
Lemma
unorm_nonnil
d
:
unorm
d
<>
Nil
.
Lemma
unorm_iter_D0
n
u
:
unorm
(
Nat.iter
n
D0
u
)
=
unorm
u
.
Lemma
del_head_nonnil
n
u
:
n
<
nb_digits
u
->
del_head
n
u
<>
Nil
.
Lemma
del_tail_nonnil
n
u
:
n
<
nb_digits
u
->
del_tail
n
u
<>
Nil
.
Lemma
nzhead_involutive
d
:
nzhead
(
nzhead
d
)
=
nzhead
d
.
#[
deprecated
(
since
="8.13",
note
="Use nzhead_involutive instead.")]
Notation
nzhead_invol
:=
nzhead_involutive
(
only
parsing
).
Lemma
nztail_involutive
d
:
nztail
(
nztail
d
)
=
nztail
d
.
#[
deprecated
(
since
="8.13",
note
="Use nztail_involutive instead.")]
Notation
nztail_invol
:=
nztail_involutive
(
only
parsing
).
Lemma
unorm_involutive
d
:
unorm
(
unorm
d
)
=
unorm
d
.
#[
deprecated
(
since
="8.13",
note
="Use unorm_involutive instead.")]
Notation
unorm_invol
:=
unorm_involutive
(
only
parsing
).
Lemma
norm_involutive
d
:
norm
(
norm
d
)
=
norm
d
.
#[
deprecated
(
since
="8.13",
note
="Use norm_involutive instead.")]
Notation
norm_invol
:=
norm_involutive
(
only
parsing
).
Lemma
lnzhead_neq_d0_head
l
l'
:
~(
lnzhead
l
=
cons
d0
l'
)
.
Lemma
lnzhead_head_nd0
h
t
:
h
<>
d0
->
lnzhead
(
cons
h
t
)
=
cons
h
t
.
Lemma
nzhead_del_tail_nzhead_eq
n
u
:
nzhead
u
=
u
->
n
<
nb_digits
u
->
nzhead
(
del_tail
n
u
)
=
del_tail
n
u
.
Lemma
nzhead_del_tail_nzhead
n
u
:
n
<
nb_digits
(
nzhead
u
)
->
nzhead
(
del_tail
n
(
nzhead
u
))
=
del_tail
n
(
nzhead
u
).
Lemma
unorm_del_tail_unorm
n
u
:
n
<
nb_digits
(
unorm
u
)
->
unorm
(
del_tail
n
(
unorm
u
))
=
del_tail
n
(
unorm
u
).
Lemma
norm_del_tail_int_norm
n
d
:
n
<
nb_digits
(
match
norm
d
with
Pos
d
|
Neg
d
=>
d
end
)
->
norm
(
del_tail_int
n
(
norm
d
))
=
del_tail_int
n
(
norm
d
).
Lemma
nzhead_app_nzhead
d
d'
:
nzhead
(
app
(
nzhead
d
)
d'
)
=
nzhead
(
app
d
d'
).
Lemma
unorm_app_unorm
d
d'
:
unorm
(
app
(
unorm
d
)
d'
)
=
unorm
(
app
d
d'
).
Lemma
norm_app_int_norm
d
d'
:
unorm
d'
=
zero
->
norm
(
app_int
(
norm
d
)
d'
)
=
norm
(
app_int
d
d'
).