Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
CertiCompil
CompCert-KVX
Commits
d4513f41
Unverified
Commit
d4513f41
authored
Dec 28, 2020
by
Guillaume Melquiond
Committed by
GitHub
Dec 28, 2020
Browse files
Update Flocq to 3.4.0 (#383)
parent
548e62be
Changes
30
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
d4513f41
...
...
@@ -57,6 +57,7 @@ GPATH=$(DIRS)
ifeq
($(LIBRARY_FLOCQ),local)
FLOCQ
=
\
SpecFloatCompat.v
\
Raux.v Zaux.v Defs.v Digits.v Float_prop.v FIX.v FLT.v FLX.v FTZ.v
\
Generic_fmt.v Round_pred.v Round_NE.v Ulp.v Core.v
\
Bracket.v Div.v Operations.v Round.v Sqrt.v
\
...
...
flocq/Calc/Bracket.v
View file @
d4513f41
...
...
@@ -19,15 +19,19 @@ COPYING file for more details.
(
**
*
Locations
:
where
a
real
number
is
positioned
with
respect
to
its
rounded
-
down
value
in
an
arbitrary
format
.
*
)
From
Coq
Require
Import
Lia
.
Require
Import
Raux
Defs
Float_prop
.
Require
Import
SpecFloatCompat
.
Notation
location
:=
location
(
only
parsing
).
Notation
loc_Exact
:=
loc_Exact
(
only
parsing
).
Notation
loc_Inexact
:=
loc_Inexact
(
only
parsing
).
Section
Fcalc_bracket
.
Variable
d
u
:
R
.
Hypothesis
Hdu
:
(
d
<
u
)
%
R
.
Inductive
location
:=
loc_Exact
|
loc_Inexact
:
comparison
->
location
.
Variable
x
:
R
.
Definition
inbetween_loc
:=
...
...
@@ -233,7 +237,7 @@ apply Rplus_le_compat_l.
apply
Rmult_le_compat_r
.
now
apply
Rlt_le
.
apply
IZR_le
.
omeg
a
.
li
a
.
(
*
.
*
)
now
rewrite
middle_range
.
Qed
.
...
...
@@ -246,7 +250,7 @@ Theorem inbetween_step_Lo :
Proof
.
intros
x
k
l
Hx
Hk1
Hk2
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
apply
Rcompare_Lt
.
assert
(
Hx
'
:=
inbetween_bounds
_
_
(
ordered_steps
_
)
_
_
Hx
).
apply
Rlt_le_trans
with
(
1
:=
proj2
Hx
'
).
...
...
@@ -255,7 +259,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply
Rcompare_not_Lt
.
rewrite
<-
mult_IZR
.
apply
IZR_le
.
omeg
a
.
li
a
.
exact
Hstep
.
Qed
.
...
...
@@ -267,7 +271,7 @@ Theorem inbetween_step_Hi :
Proof
.
intros
x
k
l
Hx
Hk1
Hk2
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
apply
Rcompare_Gt
.
assert
(
Hx
'
:=
inbetween_bounds
_
_
(
ordered_steps
_
)
_
_
Hx
).
apply
Rlt_le_trans
with
(
2
:=
proj1
Hx
'
).
...
...
@@ -276,7 +280,7 @@ rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply
Rcompare_Lt
.
rewrite
<-
mult_IZR
.
apply
IZR_lt
.
omeg
a
.
li
a
.
exact
Hstep
.
Qed
.
...
...
@@ -331,7 +335,7 @@ Theorem inbetween_step_any_Mi_odd :
Proof
.
intros
x
k
l
Hx
Hk
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
inversion_clear
Hx
as
[
|
l
'
_
Hl
].
now
rewrite
(
middle_odd
_
Hk
)
in
Hl
.
Qed
.
...
...
@@ -344,7 +348,7 @@ Theorem inbetween_step_Lo_Mi_Eq_odd :
Proof
.
intros
x
k
Hx
Hk
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
inversion_clear
Hx
as
[
Hl
|
].
rewrite
Hl
.
rewrite
Rcompare_plus_l
,
Rcompare_mult_r
,
Rcompare_half_r
.
...
...
@@ -365,7 +369,7 @@ Theorem inbetween_step_Hi_Mi_even :
Proof
.
intros
x
k
l
Hx
Hl
Hk
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
apply
Rcompare_Gt
.
assert
(
Hx
'
:=
inbetween_bounds_not_Eq
_
_
_
_
Hx
Hl
).
apply
Rle_lt_trans
with
(
2
:=
proj1
Hx
'
).
...
...
@@ -387,7 +391,7 @@ Theorem inbetween_step_Mi_Mi_even :
Proof
.
intros
x
k
Hx
Hk
.
apply
inbetween_step_not_Eq
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
apply
Rcompare_Eq
.
inversion_clear
Hx
as
[
Hx
'
|
].
rewrite
Hx
'
,
<-
Hk
,
mult_IZR
.
...
...
@@ -433,10 +437,10 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1).
destruct
(
Zcompare_spec
(
2
*
k
)
nb_steps
)
as
[
Hk1
|
Hk1
|
Hk1
].
(
*
.
2
*
k
<
nb_steps
*
)
apply
inbetween_step_Lo
with
(
1
:=
Hx
).
omeg
a
.
li
a
.
destruct
(
Zeven_ex
nb_steps
).
rewrite
He
in
H
.
omeg
a
.
li
a
.
(
*
.
2
*
k
=
nb_steps
*
)
set
(
l
'
:=
match
l
with
loc_Exact
=>
Eq
|
_
=>
Gt
end
).
assert
((
l
=
loc_Exact
/
\
l
'
=
Eq
)
\
/
(
l
<>
loc_Exact
/
\
l
'
=
Gt
)).
...
...
@@ -490,7 +494,7 @@ now apply inbetween_step_Lo_not_Eq with (2 := H1).
destruct
(
Zcompare_spec
(
2
*
k
+
1
)
nb_steps
)
as
[
Hk1
|
Hk1
|
Hk1
].
(
*
.
2
*
k
+
1
<
nb_steps
*
)
apply
inbetween_step_Lo
with
(
1
:=
Hx
)
(
3
:=
Hk1
).
omeg
a
.
li
a
.
(
*
.
2
*
k
+
1
=
nb_steps
*
)
destruct
l
.
apply
inbetween_step_Lo_Mi_Eq_odd
with
(
1
:=
Hx
)
(
2
:=
Hk1
).
...
...
@@ -499,7 +503,7 @@ apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1).
apply
inbetween_step_Hi
with
(
1
:=
Hx
).
destruct
(
Zeven_ex
nb_steps
).
rewrite
Ho
in
H
.
omeg
a
.
li
a
.
apply
Hk
.
Qed
.
...
...
@@ -612,7 +616,7 @@ clear -Hk. intros m.
rewrite
(
F2R_change_exp
beta
e
).
apply
(
f_equal
(
fun
r
=>
F2R
(
Float
beta
(
m
*
Zpower
_
r
)
e
))).
ring
.
omeg
a
.
li
a
.
assert
(
Hp
:
(
Zpower
beta
k
>
0
)
%
Z
).
apply
Z
.
lt_gt
.
apply
Zpower_gt_0
.
...
...
@@ -622,7 +626,7 @@ rewrite 2!Hr.
rewrite
Zmult_plus_distr_l
,
Zmult_1_l
.
unfold
F2R
at
2.
simpl
.
rewrite
plus_IZR
,
Rmult_plus_distr_r
.
apply
new_location_correct
.
apply
new_location_correct
;
unfold
F2R
;
simpl
.
apply
bpow_gt_0
.
now
apply
Zpower_gt_1
.
now
apply
Z_mod_lt
.
...
...
@@ -665,7 +669,7 @@ rewrite <- Hm in H'. clear -H H'.
apply
inbetween_unique
with
(
1
:=
H
)
(
2
:=
H
'
).
destruct
(
inbetween_float_bounds
x
m
e
l
H
)
as
(
H1
,
H2
).
destruct
(
inbetween_float_bounds
x
m
'
e
l
'
H
'
)
as
(
H3
,
H4
).
cut
(
m
<
m
'
+
1
/
\
m
'
<
m
+
1
)
%
Z
.
clear
;
omeg
a
.
cut
(
m
<
m
'
+
1
/
\
m
'
<
m
+
1
)
%
Z
.
clear
;
li
a
.
now
split
;
apply
lt_F2R
with
beta
e
;
apply
Rle_lt_trans
with
x
.
Qed
.
...
...
flocq/Calc/Div.v
View file @
d4513f41
...
...
@@ -19,6 +19,7 @@ COPYING file for more details.
(
**
*
Helper
function
and
theorem
for
computing
the
rounded
quotient
of
two
floating
-
point
numbers
.
*
)
From
Coq
Require
Import
Lia
.
Require
Import
Raux
Defs
Generic_fmt
Float_prop
Digits
Bracket
.
Set
Implicit
Arguments
.
...
...
@@ -80,7 +81,7 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b
destruct
(
Zle_bool
e
(
e1
-
e2
))
eqn
:
He
'
;
injection
Hm
;
intros
;
subst
.
-
split
;
try
easy
.
apply
Zle_bool_imp_le
in
He
'
.
rewrite
mult_IZR
,
IZR_Zpower
by
omeg
a
.
rewrite
mult_IZR
,
IZR_Zpower
by
li
a
.
unfold
Zminus
;
rewrite
2
!
bpow_plus
,
2
!
bpow_opp
.
field
.
repeat
split
;
try
apply
Rgt_not_eq
,
bpow_gt_0
.
...
...
@@ -88,8 +89,8 @@ assert ((F2R (Float beta m1 e1) / F2R (Float beta m2 e2) = IZR m1' / IZR m2' * b
-
apply
Z
.
leb_gt
in
He
'
.
split
;
cycle
1.
{
apply
Z
.
mul_pos_pos
with
(
1
:=
Hm2
).
apply
Zpower_gt_0
;
omeg
a
.
}
rewrite
mult_IZR
,
IZR_Zpower
by
omeg
a
.
apply
Zpower_gt_0
;
li
a
.
}
rewrite
mult_IZR
,
IZR_Zpower
by
li
a
.
unfold
Zminus
;
rewrite
bpow_plus
,
bpow_opp
,
bpow_plus
,
bpow_opp
.
field
.
repeat
split
;
try
apply
Rgt_not_eq
,
bpow_gt_0
.
...
...
@@ -113,7 +114,7 @@ destruct (Z_lt_le_dec 1 m2') as [Hm2''|Hm2''].
now
apply
IZR_neq
,
Zgt_not_eq
.
field
.
now
apply
IZR_neq
,
Zgt_not_eq
.
-
assert
(
r
=
0
/
\
m2
'
=
1
)
%
Z
as
[
->
->
]
by
(
clear
-
Hr
Hm2
''
;
omeg
a
).
-
assert
(
r
=
0
/
\
m2
'
=
1
)
%
Z
as
[
->
->
]
by
(
clear
-
Hr
Hm2
''
;
li
a
).
unfold
Rdiv
.
rewrite
Rmult_1_l
,
Rplus_0_r
,
Rinv_1
,
Rmult_1_r
.
now
constructor
.
...
...
@@ -150,10 +151,10 @@ unfold cexp.
destruct
(
Zle_lt_or_eq
_
_
H1
)
as
[
H
|
H
].
-
replace
(
fexp
(
mag
_
_
))
with
(
fexp
(
e
+
1
)).
apply
Z
.
le_min_r
.
clear
-
H1
H2
H
;
apply
f_equal
;
omeg
a
.
clear
-
H1
H2
H
;
apply
f_equal
;
li
a
.
-
replace
(
fexp
(
mag
_
_
))
with
(
fexp
e
).
apply
Z
.
le_min_l
.
clear
-
H1
H2
H
;
apply
f_equal
;
omeg
a
.
clear
-
H1
H2
H
;
apply
f_equal
;
li
a
.
Qed
.
End
Fcalc_div
.
flocq/Calc/Operations.v
View file @
d4513f41
...
...
@@ -17,7 +17,9 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING
file
for
more
details
.
*
)
(
**
Basic
operations
on
floats
:
alignment
,
addition
,
multiplication
*
)
(
**
*
Basic
operations
on
floats
:
alignment
,
addition
,
multiplication
*
)
From
Coq
Require
Import
Lia
.
Require
Import
Raux
Defs
Float_prop
.
Set
Implicit
Arguments
.
...
...
@@ -50,7 +52,7 @@ case (Zle_bool e1 e2) ; intros He ; split ; trivial.
now
rewrite
<-
F2R_change_exp
.
rewrite
<-
F2R_change_exp
.
apply
refl_equal
.
omeg
a
.
li
a
.
Qed
.
Theorem
Falign_spec_exp
:
...
...
flocq/Calc/Round.v
View file @
d4513f41
...
...
@@ -19,6 +19,7 @@ COPYING file for more details.
(
**
*
Helper
function
for
computing
the
rounded
value
of
a
real
number
.
*
)
From
Coq
Require
Import
Lia
.
Require
Import
Core
Digits
Float_prop
Bracket
.
Section
Fcalc_round
.
...
...
@@ -88,7 +89,7 @@ destruct Px as [Px|Px].
destruct
Bx
as
[
Bx1
Bx2
].
apply
lt_0_F2R
in
Bx1
.
apply
gt_0_F2R
in
Bx2
.
omeg
a
.
li
a
.
Qed
.
(
**
Relates
location
and
rounding
.
*
)
...
...
@@ -585,7 +586,7 @@ apply Zlt_succ.
rewrite
Zle_bool_true
with
(
1
:=
Hm
).
rewrite
Zle_bool_false
.
now
case
Rlt_bool
.
omeg
a
.
li
a
.
Qed
.
Definition
truncate_aux
t
k
:=
...
...
@@ -674,7 +675,7 @@ unfold cexp.
rewrite
mag_F2R_Zdigits
.
2
:
now
apply
Zgt_not_eq
.
unfold
k
in
Hk
.
clear
-
Hk
.
omeg
a
.
li
a
.
rewrite
<-
Hm
'
,
F2R_0
.
apply
generic_format_0
.
Qed
.
...
...
@@ -717,14 +718,14 @@ simpl.
apply
Zfloor_div
.
intros
H
.
generalize
(
Zpower_pos_gt_0
beta
k
)
(
Zle_bool_imp_le
_
_
(
radix_prop
beta
)).
omeg
a
.
li
a
.
rewrite
scaled_mantissa_generic
with
(
1
:=
Fx
).
now
rewrite
Zfloor_IZR
.
(
*
*
)
split
.
apply
refl_equal
.
unfold
k
in
Hk
.
omeg
a
.
li
a
.
Qed
.
Theorem
truncate_correct_partial
'
:
...
...
@@ -744,7 +745,7 @@ destruct Zlt_bool ; intros Hk.
now
apply
inbetween_float_new_location
.
ring
.
-
apply
(
conj
H1
).
omeg
a
.
li
a
.
Qed
.
Theorem
truncate_correct_partial
:
...
...
@@ -790,7 +791,7 @@ intros x m e l [Hx|Hx] H1 H2.
destruct
Zlt_bool
.
intros
H
.
apply
False_ind
.
omeg
a
.
li
a
.
intros
_.
apply
(
conj
H1
).
right
.
...
...
@@ -803,7 +804,7 @@ intros x m e l [Hx|Hx] H1 H2.
rewrite
mag_F2R_Zdigits
with
(
1
:=
Zm
).
now
apply
Zlt_le_weak
.
-
assert
(
Hm
:
m
=
0
%
Z
).
cut
(
m
<=
0
<
m
+
1
)
%
Z
.
omeg
a
.
cut
(
m
<=
0
<
m
+
1
)
%
Z
.
li
a
.
assert
(
F2R
(
Float
beta
m
e
)
<=
x
<
F2R
(
Float
beta
(
m
+
1
)
e
))
%
R
as
Hx
'
.
apply
inbetween_float_bounds
with
(
1
:=
H1
).
rewrite
<-
Hx
in
Hx
'
.
...
...
@@ -1156,7 +1157,7 @@ exact H1.
unfold
k
in
Hk
.
destruct
H2
as
[
H2
|
H2
].
left
.
omeg
a
.
li
a
.
right
.
split
.
exact
H2
.
...
...
@@ -1165,7 +1166,7 @@ inversion_clear H1.
rewrite
H
.
apply
generic_format_F2R
.
unfold
cexp
.
omeg
a
.
li
a
.
Qed
.
End
Fcalc_round
.
flocq/Calc/Sqrt.v
View file @
d4513f41
...
...
@@ -19,6 +19,7 @@ COPYING file for more details.
(
**
*
Helper
functions
and
theorems
for
computing
the
rounded
square
root
of
a
floating
-
point
number
.
*
)
From
Coq
Require
Import
Lia
.
Require
Import
Raux
Defs
Digits
Generic_fmt
Float_prop
Bracket
.
Set
Implicit
Arguments
.
...
...
@@ -86,7 +87,7 @@ assert (sqrt (F2R (Float beta m1 e1)) = sqrt (IZR m') * bpow e)%R as Hf.
{
rewrite
<-
(
sqrt_Rsqr
(
bpow
e
))
by
apply
bpow_ge_0
.
rewrite
<-
sqrt_mult
.
unfold
Rsqr
,
m
'
.
rewrite
mult_IZR
,
IZR_Zpower
by
omeg
a
.
rewrite
mult_IZR
,
IZR_Zpower
by
li
a
.
rewrite
Rmult_assoc
,
<-
2
!
bpow_plus
.
now
replace
(
_
+
_
)
%
Z
with
e1
by
ring
.
now
apply
IZR_le
.
...
...
@@ -106,7 +107,7 @@ fold (Rsqr (IZR q)).
rewrite
sqrt_Rsqr
.
now
constructor
.
apply
IZR_le
.
clear
-
Hr
;
omeg
a
.
clear
-
Hr
;
li
a
.
(
*
..
r
<>
0
*
)
constructor
.
split
.
...
...
@@ -117,14 +118,14 @@ fold (Rsqr (IZR q)).
rewrite
sqrt_Rsqr
.
apply
Rle_refl
.
apply
IZR_le
.
clear
-
Hr
;
omeg
a
.
clear
-
Hr
;
li
a
.
apply
sqrt_lt_1
.
rewrite
mult_IZR
.
apply
Rle_0_sqr
.
rewrite
<-
Hq
.
now
apply
IZR_le
.
apply
IZR_lt
.
omeg
a
.
li
a
.
apply
Rlt_le_trans
with
(
sqrt
(
IZR
((
q
+
1
)
*
(
q
+
1
)))).
apply
sqrt_lt_1
.
rewrite
<-
Hq
.
...
...
@@ -133,13 +134,13 @@ rewrite mult_IZR.
apply
Rle_0_sqr
.
apply
IZR_lt
.
ring_simplify
.
omeg
a
.
li
a
.
rewrite
mult_IZR
.
fold
(
Rsqr
(
IZR
(
q
+
1
))).
rewrite
sqrt_Rsqr
.
apply
Rle_refl
.
apply
IZR_le
.
clear
-
Hr
;
omeg
a
.
clear
-
Hr
;
li
a
.
(
*
...
location
*
)
rewrite
Rcompare_half_r
.
generalize
(
Rcompare_sqr
(
2
*
sqrt
(
IZR
(
q
*
q
+
r
)))
(
IZR
q
+
IZR
(
q
+
1
))).
...
...
@@ -154,14 +155,14 @@ replace ((q + (q + 1)) * (q + (q + 1)))%Z with (4 * (q * q) + 4 * q + 1)%Z by ri
generalize
(
Zle_cases
r
q
).
case
(
Zle_bool
r
q
)
;
intros
Hr
''
.
change
(
4
*
(
q
*
q
+
r
)
<
4
*
(
q
*
q
)
+
4
*
q
+
1
)
%
Z
.
omeg
a
.
li
a
.
change
(
4
*
(
q
*
q
+
r
)
>
4
*
(
q
*
q
)
+
4
*
q
+
1
)
%
Z
.
omeg
a
.
li
a
.
rewrite
<-
Hq
.
now
apply
IZR_le
.
rewrite
<-
plus_IZR
.
apply
IZR_le
.
clear
-
Hr
;
omeg
a
.
clear
-
Hr
;
li
a
.
apply
Rmult_le_pos
.
now
apply
IZR_le
.
apply
sqrt_ge_0
.
...
...
@@ -188,7 +189,7 @@ set (e := Z.min _ _).
assert
(
2
*
e
<=
e1
)
%
Z
as
He
.
{
assert
(
e
<=
Z
.
div2
e1
)
%
Z
by
apply
Z
.
le_min_r
.
rewrite
(
Zdiv2_odd_eqn
e1
).
destruct
Z
.
odd
;
omeg
a
.
}
destruct
Z
.
odd
;
li
a
.
}
generalize
(
Fsqrt_core_correct
m1
e1
e
Hm1
He
).
destruct
Fsqrt_core
as
[
m
l
].
apply
conj
.
...
...
flocq/Core/Defs.v
View file @
d4513f41
...
...
@@ -80,4 +80,8 @@ Definition Rnd_NA_pt (F : R -> Prop) (x f : R) :=
Rnd_N_pt
F
x
f
/
\
forall
f2
:
R
,
Rnd_N_pt
F
x
f2
->
(
Rabs
f2
<=
Rabs
f
)
%
R
.
Definition
Rnd_N0_pt
(
F
:
R
->
Prop
)
(
x
f
:
R
)
:=
Rnd_N_pt
F
x
f
/
\
forall
f2
:
R
,
Rnd_N_pt
F
x
f2
->
(
Rabs
f
<=
Rabs
f2
)
%
R
.
End
RND
.
flocq/Core/Digits.v
View file @
d4513f41
...
...
@@ -17,8 +17,13 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING
file
for
more
details
.
*
)
Require
Import
ZArith
Zquot
.
From
Coq
Require
Import
Lia
ZArith
Zquot
.
Require
Import
Zaux
.
Require
Import
SpecFloatCompat
.
Notation
digits2_pos
:=
digits2_pos
(
only
parsing
).
Notation
Zdigits2
:=
Zdigits2
(
only
parsing
).
(
**
Number
of
bits
(
radix
2
)
of
a
positive
integer
.
...
...
@@ -41,9 +46,9 @@ intros n d. unfold d. clear.
assert
(
Hp
:
forall
m
,
(
Zpower_nat
2
(
S
m
)
=
2
*
Zpower_nat
2
m
)
%
Z
)
by
easy
.
induction
n
;
simpl
digits2_Pnat
.
rewrite
Zpos_xI
,
2
!
Hp
.
omeg
a
.
li
a
.
rewrite
(
Zpos_xO
n
),
2
!
Hp
.
omeg
a
.
li
a
.
now
split
.
Qed
.
...
...
@@ -185,13 +190,13 @@ apply Zgt_not_eq.
now
apply
Zpower_gt_0
.
now
apply
Zle_minus_le_0
.
destruct
(
Zle_or_lt
0
k
)
as
[
H0
|
H0
].
rewrite
(
Zdigit_lt
n
)
by
omeg
a
.
rewrite
(
Zdigit_lt
n
)
by
li
a
.
unfold
Zdigit
.
replace
k
'
with
(
k
'
-
k
+
k
)
%
Z
by
ring
.
rewrite
Zpower_plus
with
(
2
:=
H0
).
rewrite
Zmult_assoc
,
Z_quot_mult
.
replace
(
k
'
-
k
)
%
Z
with
(
k
'
-
k
-
1
+
1
)
%
Z
by
ring
.
rewrite
Zpower_exp
by
omeg
a
.
rewrite
Zpower_exp
by
li
a
.
rewrite
Zmult_assoc
.
change
(
Zpower
beta
1
)
with
(
beta
*
1
)
%
Z
.
rewrite
Zmult_1_r
.
...
...
@@ -203,7 +208,7 @@ now apply Zlt_le_weak.
rewrite
Zdigit_lt
with
(
1
:=
H0
).
apply
sym_eq
.
apply
Zdigit_lt
.
omeg
a
.
li
a
.
Qed
.
Theorem
Zdigit_div_pow
:
...
...
@@ -227,7 +232,7 @@ unfold Zdigit.
rewrite
<-
2
!
ZOdiv_mod_mult
.
apply
(
f_equal
(
fun
x
=>
Z
.
quot
x
(
beta
^
k
))).
replace
k
'
with
(
k
+
1
+
(
k
'
-
(
k
+
1
)))
%
Z
by
ring
.
rewrite
Zpower_exp
by
omeg
a
.
rewrite
Zpower_exp
by
li
a
.
rewrite
Zmult_comm
.
rewrite
Zpower_plus
by
easy
.
change
(
Zpower
beta
1
)
with
(
beta
*
1
)
%
Z
.
...
...
@@ -449,7 +454,7 @@ unfold Zscale.
case
Zle_bool_spec
;
intros
Hk
.
now
apply
Zdigit_mul_pow
.
apply
Zdigit_div_pow
with
(
1
:=
Hk
'
).
omeg
a
.
li
a
.
Qed
.
Theorem
Zscale_0
:
...
...
@@ -492,7 +497,7 @@ now rewrite Zpower_plus.
now
apply
Zplus_le_0_compat
.
case
Zle_bool_spec
;
intros
Hk
''
.
pattern
k
at
1
;
replace
k
with
(
k
+
k
'
+
-
k
'
)
%
Z
by
ring
.
assert
(
0
<=
-
k
'
)
%
Z
by
omeg
a
.
assert
(
0
<=
-
k
'
)
%
Z
by
li
a
.
rewrite
Zpower_plus
by
easy
.
rewrite
Zmult_assoc
,
Z_quot_mult
.
apply
refl_equal
.
...
...
@@ -503,7 +508,7 @@ rewrite Zpower_plus with (2 := Hk).
apply
Zquot_mult_cancel_r
.
apply
Zgt_not_eq
.
now
apply
Zpower_gt_0
.
omeg
a
.
li
a
.
Qed
.
Theorem
Zscale_scale
:
...
...
@@ -532,7 +537,7 @@ rewrite Zdigit_mod_pow by apply Hk.
rewrite
Zdigit_scale
by
apply
Hk
.
unfold
Zminus
.
now
rewrite
Z
.
opp_involutive
,
Zplus_comm
.
omeg
a
.
li
a
.
Qed
.
Theorem
Zdigit_slice_out
:
...
...
@@ -589,16 +594,16 @@ destruct (Zle_or_lt k2' k) as [Hk''|Hk''].
now
apply
Zdigit_slice_out
.
rewrite
Zdigit_slice
by
now
split
.
apply
Zdigit_slice_out
.
zify
;
omeg
a
.
rewrite
Zdigit_slice
by
(
zify
;
omeg
a
).
zify
;
li
a
.
rewrite
Zdigit_slice
by
(
zify
;
li
a
).
rewrite
(
Zdigit_slice
n
(
k1
+
k1
'
))
by
now
split
.
rewrite
Zdigit_slice
.
now
rewrite
Zplus_assoc
.
zify
;
omeg
a
.
zify
;
li
a
.
unfold
Zslice
.
rewrite
Z
.
min_r
.
now
rewrite
Zle_bool_false
.
omeg
a
.
li
a
.
Qed
.
Theorem
Zslice_mul_pow
:
...
...
@@ -624,14 +629,14 @@ case Zle_bool_spec ; intros Hk2.
apply
(
f_equal
(
fun
x
=>
Z
.
rem
x
(
beta
^
k2
))).
unfold
Zscale
.
case
Zle_bool_spec
;
intros
Hk1
'
.
replace
k1
with
Z0
by
omeg
a
.
replace
k1
with
Z0
by
li
a
.
case
Zle_bool_spec
;
intros
Hk
'
.
replace
k
with
Z0
by
omeg
a
.
replace
k
with
Z0
by
li
a
.
simpl
.
now
rewrite
Z
.
quot_1_r
.
rewrite
Z
.
opp_involutive
.
apply
Zmult_1_r
.
rewrite
Zle_bool_false
by
omeg
a
.
rewrite
Zle_bool_false
by
li
a
.
rewrite
2
!
Z
.
opp_involutive
,
Zplus_comm
.
rewrite
Zpower_plus
by
assumption
.
apply
Zquot_Zquot
.
...
...
@@ -646,7 +651,7 @@ unfold Zscale.
case
Zle_bool_spec
;
intros
Hk
.
now
apply
Zslice_mul_pow
.
apply
Zslice_div_pow
with
(
2
:=
Hk1
).
omeg
a
.
li
a
.
Qed
.
Theorem
Zslice_div_pow_scale
:
...
...
@@ -666,7 +671,7 @@ apply Zdigit_slice_out.
now
apply
Zplus_le_compat_l
.
rewrite
Zdigit_slice
by
now
split
.
destruct
(
Zle_or_lt
0
(
k1
+
k
'
))
as
[
Hk1
'
|
Hk1
'
].
rewrite
Zdigit_slice
by
omeg
a
.
rewrite
Zdigit_slice
by
li
a
.
rewrite
Zdigit_div_pow
by
assumption
.
apply
f_equal
.
ring
.
...
...
@@ -685,15 +690,15 @@ rewrite Zdigit_plus.
rewrite
Zdigit_scale
with
(
1
:=
Hk
).
destruct
(
Zle_or_lt
(
l1
+
l2
)
k
)
as
[
Hk2
|
Hk2
].
rewrite
Zdigit_slice_out
with
(
1
:=
Hk2
).
now
rewrite
2
!
Zdigit_slice_out
by
omeg
a
.
now
rewrite
2
!
Zdigit_slice_out
by
li
a
.
rewrite
Zdigit_slice
with
(
1
:=
conj
Hk
Hk2
).
destruct
(
Zle_or_lt
l1
k
)
as
[
Hk1
|
Hk1
].
rewrite
Zdigit_slice_out
with
(
1
:=
Hk1
).
rewrite
Zdigit_slice
by
omeg
a
.
rewrite
Zdigit_slice
by
li
a
.
simpl
;
apply
f_equal
.
ring
.
rewrite
Zdigit_slice
with
(
1
:=
conj
Hk
Hk1
).
rewrite
(
Zdigit_lt
_
(
k
-
l1
))
by
omeg
a
.
rewrite
(
Zdigit_lt
_
(
k
-
l1
))
by
li
a
.
apply
Zplus_0_r
.
rewrite
Zmult_comm
.
apply
Zsame_sign_trans_weak
with
n
.
...
...
@@ -713,7 +718,7 @@ left.
now
apply
Zdigit_slice_out
.
right
.
apply
Zdigit_lt
.
omeg
a
.
li
a
.
Qed
.
Section
digits_aux
.
...
...
@@ -788,7 +793,7 @@ pattern (radix_val beta) at 2 5 ; replace (radix_val beta) with (Zpower beta 1)
rewrite
<-
Zpower_plus
.
rewrite
Zplus_comm
.
apply
IHu
.
clear
-
Hv
;
omeg
a
.
clear
-
Hv
;
li
a
.
split
.
now
ring_simplify
(
1
+
v
-
1
)
%
Z
.
now
rewrite
Zplus_assoc
.
...
...
@@ -928,7 +933,7 @@ intros x y Zx Hxy.
assert
(
Hx
:=
Zdigits_correct
x
).
assert
(
Hy
:=
Zdigits_correct
y
).
apply
(
Zpower_lt_Zpower
beta
).
zify
;
omeg
a
.
zify
;
li
a
.
Qed
.
Theorem
lt_Zdigits
:
...
...
@@ -938,7 +943,7 @@ Theorem lt_Zdigits :
(
x
<
y
)
%
Z
.
Proof
.
intros
x
y
Hy
.
cut
(
y
<=
x
->
Zdigits
y
<=
Zdigits
x
)
%
Z
.
omeg
a
.
cut
(
y
<=
x
->
Zdigits
y
<=
Zdigits
x
)
%
Z
.
li
a
.
now
apply
Zdigits_le
.
Qed
.
...
...
@@ -951,7 +956,7 @@ intros e x Hex.
destruct
(
Zdigits_correct
x
)
as
[
H1
H2
].
apply
Z
.
le_trans
with
(
2
:=
H1
).
apply
Zpower_le
.
clear
-
Hex
;
omeg
a
.
clear
-
Hex
;
li
a
.