Library Coq.Numbers.DecimalPos
DecimalPos
Proofs that conversions between decimal numbers and
positive
are bijections.
Require
Import
Decimal
DecimalFacts
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
=> 10
*
of_lu
d
|
D1
d
=> 1
+
10
*
of_lu
d
|
D2
d
=> 2
+
10
*
of_lu
d
|
D3
d
=> 3
+
10
*
of_lu
d
|
D4
d
=> 4
+
10
*
of_lu
d
|
D5
d
=> 5
+
10
*
of_lu
d
|
D6
d
=> 6
+
10
*
of_lu
d
|
D7
d
=> 7
+
10
*
of_lu
d
|
D8
d
=> 8
+
10
*
of_lu
d
|
D9
d
=> 9
+
10
*
of_lu
d
end
.
Definition
hd
d
:=
match
d
with
|
Nil
=> 0
|
D0
_
=> 0
|
D1
_
=> 1
|
D2
_
=> 2
|
D3
_
=> 3
|
D4
_
=> 4
|
D5
_
=> 5
|
D6
_
=> 6
|
D7
_
=> 7
|
D8
_
=> 8
|
D9
_
=> 9
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
=>
d
end
.
Lemma
of_lu_eqn
d
:
of_lu
d
=
hd
d
+
10
*
(
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
)
end
.
Lemma
of_lu_revapp
d
d'
:
of_lu
(
revapp
d
d'
)
=
of_lu
(
rev
d
)
+
of_lu
d'
*
10
^
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_uint_acc
d
acc
=
Pos.of_uint_acc
(
tl
d
) (
Nadd
(
hd
d
) (10
*
acc
)).
Lemma
of_uint_acc_rev
d
acc
:
Npos
(
Pos.of_uint_acc
d
acc
)
=
of_lu
(
rev
d
)
+
(
Npos
acc
)
*
10
^
usize
d
.
Lemma
of_uint_alt
d
:
Pos.of_uint
d
=
of_lu
(
rev
d
).
Lemma
of_lu_rev
d
:
Pos.of_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_uint
(
Pos.to_uint
p
)
=
Npos
p
.
The other direction
Definition
to_lu
n
:=
match
n
with
|
N0
=>
Decimal.zero
|
Npos
p
=>
Pos.to_little_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_ldec_tenfold
p
:
to_lu
(10
*
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
(10
*
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_uint
(
Pos.of_uint
d
)
=
unorm
d
.
Some consequences
Lemma
to_uint_nonzero
p
:
Pos.to_uint
p
<>
zero
.
Lemma
to_uint_nonnil
p
:
Pos.to_uint
p
<>
Nil
.
Lemma
to_uint_inj
p
p'
:
Pos.to_uint
p
=
Pos.to_uint
p'
->
p
=
p'
.
Lemma
to_uint_pos_surj
d
:
unorm
d
<>
zero
->
exists
p
,
Pos.to_uint
p
=
unorm
d
.
Lemma
of_uint_norm
d
:
Pos.of_uint
(
unorm
d
)
=
Pos.of_uint
d
.
Lemma
of_inj
d
d'
:
Pos.of_uint
d
=
Pos.of_uint
d'
->
unorm
d
=
unorm
d'
.
Lemma
of_iff
d
d'
:
Pos.of_uint
d
=
Pos.of_uint
d'
<->
unorm
d
=
unorm
d'
.
Lemma
nztail_to_uint
p
:
let
(
h
,
n
) :=
Decimal.nztail
(
Pos.to_uint
p
)
in
Npos
p
=
Pos.of_uint
h
*
10
^(
N.of_nat
n
)
.
End
Unsigned
.
Conversion from/to signed decimal numbers
Module
Signed
.
Lemma
of_to
(
p
:
positive
) :
Pos.of_int
(
Pos.to_int
p
)
=
Some
p
.
Lemma
to_of
(
d
:
int
)(
p
:
positive
) :
Pos.of_int
d
=
Some
p
->
Pos.to_int
p
=
norm
d
.
Lemma
to_int_inj
p
p'
:
Pos.to_int
p
=
Pos.to_int
p'
->
p
=
p'
.
Lemma
to_int_pos_surj
d
:
unorm
d
<>
zero
->
exists
p
,
Pos.to_int
p
=
norm
(
Pos
d
).
Lemma
of_int_norm
d
:
Pos.of_int
(
norm
d
)
=
Pos.of_int
d
.
Lemma
of_inj_pos
d
d'
:
Pos.of_int
(
Pos
d
)
=
Pos.of_int
(
Pos
d'
)
->
unorm
d
=
unorm
d'
.
End
Signed
.