Library Coq.Numbers.HexadecimalPos
HexadecimalPos
Proofs that conversions between hexadecimal numbers and
positive
are bijections.
Require
Import
Hexadecimal
HexadecimalFacts
PArith
NArith
.
Module
Unsigned
.
Local Open
Scope
N
.
A direct version of
of_little_uint
Fixpoint
of_lu
(
d
:
uint
) :
N
:=
match
d
with
|
Nil
=> 0
|
D0
d
=> 0
x10
*
of_lu
d
|
D1
d
=> 0
x1
+
0
x10
*
of_lu
d
|
D2
d
=> 0
x2
+
0
x10
*
of_lu
d
|
D3
d
=> 0
x3
+
0
x10
*
of_lu
d
|
D4
d
=> 0
x4
+
0
x10
*
of_lu
d
|
D5
d
=> 0
x5
+
0
x10
*
of_lu
d
|
D6
d
=> 0
x6
+
0
x10
*
of_lu
d
|
D7
d
=> 0
x7
+
0
x10
*
of_lu
d
|
D8
d
=> 0
x8
+
0
x10
*
of_lu
d
|
D9
d
=> 0
x9
+
0
x10
*
of_lu
d
|
Da
d
=> 0
xa
+
0
x10
*
of_lu
d
|
Db
d
=> 0
xb
+
0
x10
*
of_lu
d
|
Dc
d
=> 0
xc
+
0
x10
*
of_lu
d
|
Dd
d
=> 0
xd
+
0
x10
*
of_lu
d
|
De
d
=> 0
xe
+
0
x10
*
of_lu
d
|
Df
d
=> 0
xf
+
0
x10
*
of_lu
d
end
.
Definition
hd
d
:=
match
d
with
|
Nil
=> 0
x0
|
D0
_
=> 0
x0
|
D1
_
=> 0
x1
|
D2
_
=> 0
x2
|
D3
_
=> 0
x3
|
D4
_
=> 0
x4
|
D5
_
=> 0
x5
|
D6
_
=> 0
x6
|
D7
_
=> 0
x7
|
D8
_
=> 0
x8
|
D9
_
=> 0
x9
|
Da
_
=> 0
xa
|
Db
_
=> 0
xb
|
Dc
_
=> 0
xc
|
Dd
_
=> 0
xd
|
De
_
=> 0
xe
|
Df
_
=> 0
xf
end
.
Definition
tl
d
:=
match
d
with
|
Nil
=>
d
|
D0
d
|
D1
d
|
D2
d
|
D3
d
|
D4
d
|
D5
d
|
D6
d
|
D7
d
|
D8
d
|
D9
d
|
Da
d
|
Db
d
|
Dc
d
|
Dd
d
|
De
d
|
Df
d
=>
d
end
.
Lemma
of_lu_eqn
d
:
of_lu
d
=
hd
d
+
0
x10
*
(
of_lu
(
tl
d
)
)
.
Ltac
simpl_of_lu
:=
match
goal
with
| |-
context
[
of_lu
(?
f
?
x
) ] =>
rewrite
(
of_lu_eqn
(
f
x
));
simpl
hd
;
simpl
tl
end
.
Fixpoint
usize
(
d
:
uint
) :
N
:=
match
d
with
|
Nil
=> 0
|
D0
d
=>
N.succ
(
usize
d
)
|
D1
d
=>
N.succ
(
usize
d
)
|
D2
d
=>
N.succ
(
usize
d
)
|
D3
d
=>
N.succ
(
usize
d
)
|
D4
d
=>
N.succ
(
usize
d
)
|
D5
d
=>
N.succ
(
usize
d
)
|
D6
d
=>
N.succ
(
usize
d
)
|
D7
d
=>
N.succ
(
usize
d
)
|
D8
d
=>
N.succ
(
usize
d
)
|
D9
d
=>
N.succ
(
usize
d
)
|
Da
d
=>
N.succ
(
usize
d
)
|
Db
d
=>
N.succ
(
usize
d
)
|
Dc
d
=>
N.succ
(
usize
d
)
|
Dd
d
=>
N.succ
(
usize
d
)
|
De
d
=>
N.succ
(
usize
d
)
|
Df
d
=>
N.succ
(
usize
d
)
end
.
Lemma
of_lu_revapp
d
d'
:
of_lu
(
revapp
d
d'
)
=
of_lu
(
rev
d
)
+
of_lu
d'
*
0
x10
^
usize
d
.
Definition
Nadd
n
p
:=
match
n
with
|
N0
=>
p
|
Npos
p0
=> (
p0
+
p
)%
positive
end
.
Lemma
Nadd_simpl
n
p
q
:
Npos
(
Nadd
n
(
p
*
q
))
=
n
+
Npos
p
*
Npos
q
.
Lemma
of_uint_acc_eqn
d
acc
:
d
<>
Nil
->
Pos.of_hex_uint_acc
d
acc
=
Pos.of_hex_uint_acc
(
tl
d
) (
Nadd
(
hd
d
) (0
x10
*
acc
)).
Lemma
of_uint_acc_rev
d
acc
:
Npos
(
Pos.of_hex_uint_acc
d
acc
)
=
of_lu
(
rev
d
)
+
(
Npos
acc
)
*
0
x10
^
usize
d
.
Lemma
of_uint_alt
d
:
Pos.of_hex_uint
d
=
of_lu
(
rev
d
).
Lemma
of_lu_rev
d
:
Pos.of_hex_uint
(
rev
d
)
=
of_lu
d
.
Lemma
of_lu_double_gen
d
:
of_lu
(
Little.double
d
)
=
N.double
(
of_lu
d
)
/\
of_lu
(
Little.succ_double
d
)
=
N.succ_double
(
of_lu
d
).
Lemma
of_lu_double
d
:
of_lu
(
Little.double
d
)
=
N.double
(
of_lu
d
).
Lemma
of_lu_succ_double
d
:
of_lu
(
Little.succ_double
d
)
=
N.succ_double
(
of_lu
d
).
First bijection result
Lemma
of_to
(
p
:
positive
) :
Pos.of_hex_uint
(
Pos.to_hex_uint
p
)
=
Npos
p
.
The other direction
Definition
to_lu
n
:=
match
n
with
|
N0
=>
Hexadecimal.zero
|
Npos
p
=>
Pos.to_little_hex_uint
p
end
.
Lemma
succ_double_alt
d
:
Little.succ_double
d
=
Little.succ
(
Little.double
d
).
Lemma
double_succ
d
:
Little.double
(
Little.succ
d
)
=
Little.succ
(
Little.succ_double
d
).
Lemma
to_lu_succ
n
:
to_lu
(
N.succ
n
)
=
Little.succ
(
to_lu
n
).
Lemma
nat_iter_S
n
{
A
} (
f
:
A
->
A
)
i
:
Nat.iter
(
S
n
)
f
i
=
f
(
Nat.iter
n
f
i
).
Lemma
nat_iter_0
{
A
} (
f
:
A
->
A
)
i
:
Nat.iter
0
f
i
=
i
.
Lemma
to_lhex_tenfold
p
:
to_lu
(0
x10
*
Npos
p
)
=
D0
(
to_lu
(
Npos
p
)).
Lemma
of_lu_0
d
:
of_lu
d
=
0
<->
nztail
d
=
Nil
.
Lemma
to_of_lu_tenfold
d
:
to_lu
(
of_lu
d
)
=
lnorm
d
->
to_lu
(0
x10
*
of_lu
d
)
=
lnorm
(
D0
d
).
Lemma
Nadd_alt
n
m
:
n
+
m
=
Nat.iter
(
N.to_nat
n
)
N.succ
m
.
Ltac
simpl_to_nat
:=
simpl
N.to_nat
;
unfold
Pos.to_nat
;
simpl
Pos.iter_op
.
Lemma
to_of_lu
d
:
to_lu
(
of_lu
d
)
=
lnorm
d
.
Second bijection result
Lemma
to_of
(
d
:
uint
) :
N.to_hex_uint
(
Pos.of_hex_uint
d
)
=
unorm
d
.
Some consequences
Lemma
to_uint_nonzero
p
:
Pos.to_hex_uint
p
<>
zero
.
Lemma
to_uint_nonnil
p
:
Pos.to_hex_uint
p
<>
Nil
.
Lemma
to_uint_inj
p
p'
:
Pos.to_hex_uint
p
=
Pos.to_hex_uint
p'
->
p
=
p'
.
Lemma
to_uint_pos_surj
d
:
unorm
d
<>
zero
->
exists
p
,
Pos.to_hex_uint
p
=
unorm
d
.
Lemma
of_uint_norm
d
:
Pos.of_hex_uint
(
unorm
d
)
=
Pos.of_hex_uint
d
.
Lemma
of_inj
d
d'
:
Pos.of_hex_uint
d
=
Pos.of_hex_uint
d'
->
unorm
d
=
unorm
d'
.
Lemma
of_iff
d
d'
:
Pos.of_hex_uint
d
=
Pos.of_hex_uint
d'
<->
unorm
d
=
unorm
d'
.
Lemma
nztail_to_hex_uint
p
:
let
(
h
,
n
) :=
Hexadecimal.nztail
(
Pos.to_hex_uint
p
)
in
Npos
p
=
Pos.of_hex_uint
h
*
0
x10
^(
N.of_nat
n
)
.
Definition
double
d
:=
rev
(
Little.double
(
rev
d
)).
Lemma
double_unorm
d
:
double
(
unorm
d
)
=
unorm
(
double
d
).
Lemma
double_nzhead
d
:
double
(
nzhead
d
)
=
nzhead
(
double
d
).
Lemma
of_hex_uint_double
d
:
Pos.of_hex_uint
(
double
d
)
=
N.double
(
Pos.of_hex_uint
d
).
End
Unsigned
.
Conversion from/to signed decimal numbers
Module
Signed
.
Lemma
of_to
(
p
:
positive
) :
Pos.of_hex_int
(
Pos.to_hex_int
p
)
=
Some
p
.
Lemma
to_of
(
d
:
int
)(
p
:
positive
) :
Pos.of_hex_int
d
=
Some
p
->
Pos.to_hex_int
p
=
norm
d
.
Lemma
to_int_inj
p
p'
:
Pos.to_hex_int
p
=
Pos.to_hex_int
p'
->
p
=
p'
.
Lemma
to_int_pos_surj
d
:
unorm
d
<>
zero
->
exists
p
,
Pos.to_hex_int
p
=
norm
(
Pos
d
).
Lemma
of_int_norm
d
:
Pos.of_hex_int
(
norm
d
)
=
Pos.of_hex_int
d
.
Lemma
of_inj_pos
d
d'
:
Pos.of_hex_int
(
Pos
d
)
=
Pos.of_hex_int
(
Pos
d'
)
->
unorm
d
=
unorm
d'
.
End
Signed
.