Library Coq.Numbers.DecimalN
DecimalN
Proofs that conversions between decimal numbers and
N
are bijections
Require
Import
Decimal
DecimalFacts
DecimalPos
PArith
NArith
.
Module
Unsigned
.
Lemma
of_to
(
n
:
N
) :
N.of_uint
(
N.to_uint
n
)
=
n
.
Lemma
to_of
(
d
:
uint
) :
N.to_uint
(
N.of_uint
d
)
=
unorm
d
.
Lemma
to_uint_inj
n
n'
:
N.to_uint
n
=
N.to_uint
n'
->
n
=
n'
.
Lemma
to_uint_surj
d
:
exists
p
,
N.to_uint
p
=
unorm
d
.
Lemma
of_uint_norm
d
:
N.of_uint
(
unorm
d
)
=
N.of_uint
d
.
Lemma
of_inj
d
d'
:
N.of_uint
d
=
N.of_uint
d'
->
unorm
d
=
unorm
d'
.
Lemma
of_iff
d
d'
:
N.of_uint
d
=
N.of_uint
d'
<->
unorm
d
=
unorm
d'
.
End
Unsigned
.
Conversion from/to signed decimal numbers
Module
Signed
.
Lemma
of_to
(
n
:
N
) :
N.of_int
(
N.to_int
n
)
=
Some
n
.
Lemma
to_of
(
d
:
int
)(
n
:
N
) :
N.of_int
d
=
Some
n
->
N.to_int
n
=
norm
d
.
Lemma
to_int_inj
n
n'
:
N.to_int
n
=
N.to_int
n'
->
n
=
n'
.
Lemma
to_int_pos_surj
d
:
exists
n
,
N.to_int
n
=
norm
(
Pos
d
).
Lemma
of_int_norm
d
:
N.of_int
(
norm
d
)
=
N.of_int
d
.
Lemma
of_inj_pos
d
d'
:
N.of_int
(
Pos
d
)
=
N.of_int
(
Pos
d'
)
->
unorm
d
=
unorm
d'
.
End
Signed
.