Library Coq.Numbers.DecimalFacts
DecimalFacts : some facts about Decimal numbers
Require
Import
Decimal
.
Lemma
uint_dec
(
d
d'
:
uint
) :
{
d
=
d'
}
+
{
d
<>
d'
}
.
Lemma
rev_revapp
d
d'
:
rev
(
revapp
d
d'
)
=
revapp
d'
d
.
Lemma
rev_rev
d
:
rev
(
rev
d
)
=
d
.
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
)
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_nztail_rev
d
:
rev
(
nztail
(
rev
d
))
=
nzhead
d
.
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
nzhead_invol
d
:
nzhead
(
nzhead
d
)
=
nzhead
d
.
Lemma
unorm_invol
d
:
unorm
(
unorm
d
)
=
unorm
d
.
Lemma
norm_invol
d
:
norm
(
norm
d
)
=
norm
d
.