Library Coq.Numbers.DecimalFacts
DecimalFacts : some facts about Decimal numbers
Require
Import
Decimal
Arith
.
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
.
Lemma
revapp_rev_nil
d
:
revapp
(
rev
d
)
Nil
=
d
.
Lemma
app_nil_r
d
:
app
d
Nil
=
d
.
Lemma
app_int_nil_r
d
:
app_int
d
Nil
=
d
.
Lemma
revapp_revapp_1
d
d'
d''
:
nb_digits
d
<=
1
->
revapp
(
revapp
d
d'
)
d''
=
revapp
d'
(
revapp
d
d''
).
Lemma
nb_digits_pos
d
:
d
<>
Nil
->
0
<
nb_digits
d
.
Lemma
nb_digits_revapp
d
d'
:
nb_digits
(
revapp
d
d'
)
=
nb_digits
d
+
nb_digits
d'
.
Lemma
nb_digits_rev
u
:
nb_digits
(
rev
u
)
=
nb_digits
u
.
Lemma
nb_digits_nzhead
u
:
nb_digits
(
nzhead
u
)
<=
nb_digits
u
.
Lemma
del_head_nb_digits
(
u
:
uint
) :
del_head
(
nb_digits
u
)
u
=
Nil
.
Lemma
nb_digits_del_head
n
u
:
n
<=
nb_digits
u
->
nb_digits
(
del_head
n
u
)
=
nb_digits
u
-
n
.
Lemma
nb_digits_iter_D0
n
d
:
nb_digits
(
Nat.iter
n
D0
d
)
=
n
+
nb_digits
d
.
Fixpoint
nth
n
u
:=
match
n
with
|
O
=>
match
u
with
|
Nil
=>
Nil
|
D0
d
=>
D0
Nil
|
D1
d
=>
D1
Nil
|
D2
d
=>
D2
Nil
|
D3
d
=>
D3
Nil
|
D4
d
=>
D4
Nil
|
D5
d
=>
D5
Nil
|
D6
d
=>
D6
Nil
|
D7
d
=>
D7
Nil
|
D8
d
=>
D8
Nil
|
D9
d
=>
D9
Nil
end
|
S
n
=>
match
u
with
|
Nil
=>
Nil
|
D0
d
|
D1
d
|
D2
d
|
D3
d
|
D4
d
|
D5
d
|
D6
d
|
D7
d
|
D8
d
|
D9
d
=>
nth
n
d
end
end
.
Lemma
nb_digits_nth
n
u
:
nb_digits
(
nth
n
u
)
<=
1.
Lemma
del_head_nth
n
u
:
n
<
nb_digits
u
->
del_head
n
u
=
revapp
(
nth
n
u
) (
del_head
(
S
n
)
u
).
Lemma
nth_revapp_r
n
d
d'
:
nb_digits
d
<=
n
->
nth
n
(
revapp
d
d'
)
=
nth
(
n
-
nb_digits
d
)
d'
.
Lemma
nth_revapp_l
n
d
d'
:
n
<
nb_digits
d
->
nth
n
(
revapp
d
d'
)
=
nth
(
nb_digits
d
-
n
-
1)
d
.
Lemma
app_del_tail_head
(
u
:
uint
)
n
:
n
<=
nb_digits
u
->
app
(
del_tail
n
u
) (
del_head
(
nb_digits
u
-
n
)
u
)
=
u
.
Lemma
app_int_del_tail_head
n
(
d
:
int
) :
let
ad
:=
match
d
with
Pos
d
|
Neg
d
=>
d
end
in
n
<=
nb_digits
ad
->
app_int
(
del_tail_int
n
d
) (
del_head
(
nb_digits
ad
-
n
)
ad
)
=
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
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_D0
u
:
unorm
(
D0
u
)
=
unorm
u
.
Lemma
unorm_iter_D0
n
u
:
unorm
(
Nat.iter
n
D0
u
)
=
unorm
u
.
Lemma
nb_digits_unorm
u
:
u
<>
Nil
->
nb_digits
(
unorm
u
)
<=
nb_digits
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_invol
d
:
nzhead
(
nzhead
d
)
=
nzhead
d
.
Lemma
nztail_invol
d
:
nztail
(
nztail
d
)
=
nztail
d
.
Lemma
unorm_invol
d
:
unorm
(
unorm
d
)
=
unorm
d
.
Lemma
norm_invol
d
:
norm
(
norm
d
)
=
norm
d
.
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'
).