Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
F
flocq
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
1
Merge Requests
1
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
Flocq
flocq
Commits
60631b5d
Commit
60631b5d
authored
Mar 02, 2014
by
Guillaume Melquiond
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Make it compile with both Coq 8.4 and trunk.
parent
218bcb9b
Changes
10
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
141 additions
and
105 deletions
+141
-105
.gitignore
.gitignore
+4
-0
src/Appli/Fappli_IEEE.v
src/Appli/Fappli_IEEE.v
+4
-2
src/Appli/Fappli_IEEE_bits.v
src/Appli/Fappli_IEEE_bits.v
+12
-2
src/Calc/Fcalc_bracket.v
src/Calc/Fcalc_bracket.v
+1
-1
src/Calc/Fcalc_ops.v
src/Calc/Fcalc_ops.v
+13
-11
src/Core/Fcore_Raux.v
src/Core/Fcore_Raux.v
+18
-0
src/Core/Fcore_Zaux.v
src/Core/Fcore_Zaux.v
+29
-29
src/Core/Fcore_digits.v
src/Core/Fcore_digits.v
+52
-52
src/Core/Fcore_generic_fmt.v
src/Core/Fcore_generic_fmt.v
+7
-7
src/Core/Fcore_ulp.v
src/Core/Fcore_ulp.v
+1
-1
No files found.
.gitignore
View file @
60631b5d
...
...
@@ -13,3 +13,7 @@ html
src/Flocq_version.v
*.vo
*.glob
.*.aux
N*.cm*
N*.native
N*.o
src/Appli/Fappli_IEEE.v
View file @
60631b5d
...
...
@@ -46,6 +46,8 @@ End AnyRadix.
Section
Binary
.
Implicit
Arguments
exist
[[
A
]
[
P
]].
(
**
prec
is
the
number
of
bits
of
the
mantissa
including
the
implicit
one
emax
is
the
exponent
of
the
infinities
Typically
p
=
24
and
emax
=
128
in
single
precision
*
)
...
...
@@ -89,7 +91,7 @@ Definition FF2B x :=
|
F754_finite
s
m
e
=>
B754_finite
s
m
e
|
F754_infinity
s
=>
fun
_
=>
B754_infinity
s
|
F754_zero
s
=>
fun
_
=>
B754_zero
s
|
F754_nan
b
pl
=>
fun
H
=>
B754_nan
b
(
exist
_
pl
H
)
|
F754_nan
b
pl
=>
fun
H
=>
B754_nan
b
(
exist
pl
H
)
end
.
Definition
B2FF
x
:=
...
...
@@ -601,7 +603,7 @@ induction (nat_of_P n).
simpl
.
rewrite
Zplus_0_r
.
now
destruct
l
as
[
|
[
|
|
]].
simpl
iter_na
t
.
simpl
nat_rec
t
.
rewrite
inj_S
.
unfold
Zsucc
.
rewrite
Zplus_assoc
.
...
...
src/Appli/Fappli_IEEE_bits.v
View file @
60631b5d
...
...
@@ -25,6 +25,12 @@ Require Import Fappli_IEEE.
Section
Binary_Bits
.
Implicit
Arguments
exist
[[
A
]
[
P
]].
Implicit
Arguments
B754_zero
[[
prec
]
[
emax
]].
Implicit
Arguments
B754_infinity
[[
prec
]
[
emax
]].
Implicit
Arguments
B754_nan
[[
prec
]
[
emax
]].
Implicit
Arguments
B754_finite
[[
prec
]
[
emax
]].
(
**
Number
of
bits
for
the
fraction
and
exponent
*
)
Variable
mw
ew
:
Z
.
Hypothesis
Hmw
:
(
0
<
mw
)
%
Z
.
...
...
@@ -516,6 +522,8 @@ End Binary_Bits.
(
**
Specialization
for
IEEE
single
precision
operations
*
)
Section
B32_Bits
.
Implicit
Arguments
B754_nan
[[
prec
]
[
emax
]].
Definition
binary32
:=
binary_float
24
128.
Let
Hprec
:
(
0
<
24
)
%
Z
.
...
...
@@ -527,7 +535,7 @@ apply refl_equal.
Qed
.
Definition
default_nan_pl32
:
bool
*
nan_pl
24
:=
(
false
,
exist
_
(
nat_iter
22
xO
xH
)
(
refl_equal
true
)).
(
false
,
exist
_
(
iter_nat
22
_
xO
xH
)
(
refl_equal
true
)).
Definition
unop_nan_pl32
(
f
:
binary32
)
:
bool
*
nan_pl
24
:=
match
f
with
...
...
@@ -557,6 +565,8 @@ End B32_Bits.
(
**
Specialization
for
IEEE
double
precision
operations
*
)
Section
B64_Bits
.
Implicit
Arguments
B754_nan
[[
prec
]
[
emax
]].
Definition
binary64
:=
binary_float
53
1024.
Let
Hprec
:
(
0
<
53
)
%
Z
.
...
...
@@ -568,7 +578,7 @@ apply refl_equal.
Qed
.
Definition
default_nan_pl64
:
bool
*
nan_pl
53
:=
(
false
,
exist
_
(
nat_iter
51
xO
xH
)
(
refl_equal
true
)).
(
false
,
exist
_
(
iter_nat
51
_
xO
xH
)
(
refl_equal
true
)).
Definition
unop_nan_pl64
(
f
:
binary64
)
:
bool
*
nan_pl
53
:=
match
f
with
...
...
src/Calc/Fcalc_bracket.v
View file @
60631b5d
...
...
@@ -168,7 +168,7 @@ apply Rplus_lt_reg_r with (d * (v - 1))%R.
ring_simplify
.
rewrite
Rmult_comm
.
now
apply
Rmult_lt_compat_l
.
apply
Rplus_lt_reg_
r
with
(
-
u
*
v
)
%
R
.
apply
Rplus_lt_reg_
l
with
(
-
u
*
v
)
%
R
.
replace
(
-
u
*
v
+
(
d
+
v
*
(
u
-
d
)))
%
R
with
(
d
*
(
1
-
v
))
%
R
by
ring
.
replace
(
-
u
*
v
+
u
)
%
R
with
(
u
*
(
1
-
v
))
%
R
by
ring
.
apply
Rmult_lt_compat_r
.
...
...
src/Calc/Fcalc_ops.v
View file @
60631b5d
...
...
@@ -28,6 +28,8 @@ Variable beta : radix.
Notation
bpow
e
:=
(
bpow
beta
e
).
Implicit
Arguments
Float
[[
beta
]].
Definition
Falign
(
f1
f2
:
float
beta
)
:=
let
'
(
Float
m1
e1
)
:=
f1
in
let
'
(
Float
m2
e2
)
:=
f2
in
...
...
@@ -38,7 +40,7 @@ Definition Falign (f1 f2 : float beta) :=
Theorem
Falign_spec
:
forall
f1
f2
:
float
beta
,
let
'
(
m1
,
m2
,
e
)
:=
Falign
f1
f2
in
F2R
f1
=
F2R
(
Float
beta
m1
e
)
/
\
F2R
f2
=
F2R
(
Float
beta
m2
e
).
F2R
f1
=
@
F2R
beta
(
Float
m1
e
)
/
\
F2R
f2
=
@
F2R
beta
(
Float
m2
e
).
Proof
.
unfold
Falign
.
intros
(
m1
,
e1
)
(
m2
,
e2
).
...
...
@@ -61,9 +63,9 @@ case (Zmin_spec e1 e2); intros (H1,H2); easy.
case
(
Zmin_spec
e1
e2
);
intros
(
H1
,
H2
);
easy
.
Qed
.
Definition
Fopp
(
f1
:
float
beta
)
:=
Definition
Fopp
(
f1
:
float
beta
)
:
float
beta
:=
let
'
(
Float
m1
e1
)
:=
f1
in
Float
beta
(
-
m1
)
%
Z
e1
.
Float
(
-
m1
)
%
Z
e1
.
Theorem
F2R_opp
:
forall
f1
:
float
beta
,
...
...
@@ -72,9 +74,9 @@ intros (m1,e1).
apply
F2R_Zopp
.
Qed
.
Definition
Fabs
(
f1
:
float
beta
)
:=
Definition
Fabs
(
f1
:
float
beta
)
:
float
beta
:=
let
'
(
Float
m1
e1
)
:=
f1
in
Float
beta
(
Zabs
m1
)
%
Z
e1
.
Float
(
Zabs
m1
)
%
Z
e1
.
Theorem
F2R_abs
:
forall
f1
:
float
beta
,
...
...
@@ -83,9 +85,9 @@ intros (m1,e1).
apply
F2R_Zabs
.
Qed
.
Definition
Fplus
(
f1
f2
:
float
beta
)
:=
Definition
Fplus
(
f1
f2
:
float
beta
)
:
float
beta
:
=
let
'
(
m1
,
m2
,
e
)
:=
Falign
f1
f2
in
Float
beta
(
m1
+
m2
)
e
.
Float
(
m1
+
m2
)
e
.
Theorem
F2R_plus
:
forall
f1
f2
:
float
beta
,
...
...
@@ -104,7 +106,7 @@ Qed.
Theorem
Fplus_same_exp
:
forall
m1
m2
e
,
Fplus
(
Float
beta
m1
e
)
(
Float
beta
m2
e
)
=
Float
beta
(
m1
+
m2
)
e
.
Fplus
(
Float
m1
e
)
(
Float
m2
e
)
=
Float
(
m1
+
m2
)
e
.
Proof
.
intros
m1
m2
e
.
unfold
Fplus
.
...
...
@@ -136,17 +138,17 @@ Qed.
Theorem
Fminus_same_exp
:
forall
m1
m2
e
,
Fminus
(
Float
beta
m1
e
)
(
Float
beta
m2
e
)
=
Float
beta
(
m1
-
m2
)
e
.
Fminus
(
Float
m1
e
)
(
Float
m2
e
)
=
Float
(
m1
-
m2
)
e
.
Proof
.
intros
m1
m2
e
.
unfold
Fminus
.
apply
Fplus_same_exp
.
Qed
.
Definition
Fmult
(
f1
f2
:
float
beta
)
:=
Definition
Fmult
(
f1
f2
:
float
beta
)
:
float
beta
:
=
let
'
(
Float
m1
e1
)
:=
f1
in
let
'
(
Float
m2
e2
)
:=
f2
in
Float
beta
(
m1
*
m2
)
(
e1
+
e2
).
Float
(
m1
*
m2
)
(
e1
+
e2
).
Theorem
F2R_mult
:
forall
f1
f2
:
float
beta
,
...
...
src/Core/Fcore_Raux.v
View file @
60631b5d
...
...
@@ -73,6 +73,24 @@ apply Rplus_eq_reg_l with r.
now
rewrite
2
!
(
Rplus_comm
r
).
Qed
.
Theorem
Rplus_lt_reg_l
:
forall
r
r1
r2
:
R
,
(
r
+
r1
<
r
+
r2
)
%
R
->
(
r1
<
r2
)
%
R
.
Proof
.
intros
.
solve
[
apply
Rplus_lt_reg_l
with
(
1
:=
H
)
|
apply
Rplus_lt_reg_r
with
(
1
:=
H
)
].
Qed
.
Theorem
Rplus_lt_reg_r
:
forall
r
r1
r2
:
R
,
(
r1
+
r
<
r2
+
r
)
%
R
->
(
r1
<
r2
)
%
R
.
Proof
.
intros
.
apply
Rplus_lt_reg_l
with
r
.
now
rewrite
2
!
(
Rplus_comm
r
).
Qed
.
Theorem
Rplus_le_reg_r
:
forall
r
r1
r2
:
R
,
(
r1
+
r
<=
r2
+
r
)
%
R
->
(
r1
<=
r2
)
%
R
.
...
...
src/Core/Fcore_Zaux.v
View file @
60631b5d
...
...
@@ -18,7 +18,7 @@ COPYING file for more details.
*
)
Require
Import
ZArith
.
Require
Import
Z
Odiv
.
Require
Import
Z
quot
.
Section
Zmissing
.
...
...
@@ -385,26 +385,26 @@ Qed.
Theorem
ZOmod_eq
:
forall
a
b
,
Z
Omod
a
b
=
(
a
-
ZOdiv
a
b
*
b
)
%
Z
.
Z
.
rem
a
b
=
(
a
-
Z
.
quot
a
b
*
b
)
%
Z
.
Proof
.
intros
a
b
.
rewrite
(
Z
O_div_mod_eq
a
b
)
at
2.
rewrite
(
Z
.
quot_rem
'
a
b
)
at
2.
ring
.
Qed
.
Theorem
ZOmod_mod_mult
:
forall
n
a
b
,
Z
Omod
(
ZOmod
n
(
a
*
b
))
b
=
ZOmod
n
b
.
Z
.
rem
(
Z
.
rem
n
(
a
*
b
))
b
=
Z
.
rem
n
b
.
Proof
.
intros
n
a
b
.
assert
(
Z
Omod
n
(
a
*
b
)
=
n
+
-
(
ZOdiv
n
(
a
*
b
)
*
a
)
*
b
)
%
Z
.
assert
(
Z
.
rem
n
(
a
*
b
)
=
n
+
-
(
Z
.
quot
n
(
a
*
b
)
*
a
)
*
b
)
%
Z
.
rewrite
<-
Zopp_mult_distr_l
.
rewrite
<-
Zmult_assoc
.
apply
ZOmod_eq
.
rewrite
H
.
apply
Z
O_mod
_plus
.
apply
Z
_rem
_plus
.
rewrite
<-
H
.
apply
Z
Omod
_sgn2
.
apply
Z
rem
_sgn2
.
Qed
.
Theorem
Zdiv_mod_mult
:
...
...
@@ -434,73 +434,73 @@ Qed.
Theorem
ZOdiv_mod_mult
:
forall
n
a
b
,
(
Z
Odiv
(
ZOmod
n
(
a
*
b
))
a
)
=
ZOmod
(
ZOdiv
n
a
)
b
.
(
Z
.
quot
(
Z
.
rem
n
(
a
*
b
))
a
)
=
Z
.
rem
(
Z
.
quot
n
a
)
b
.
Proof
.
intros
n
a
b
.
destruct
(
Z_eq_dec
a
0
)
as
[
Za
|
Za
].
rewrite
Za
.
now
rewrite
2
!
Z
Odiv_0_r
,
ZOmod
_0_l
.
assert
(
Z
Omod
n
(
a
*
b
)
=
n
+
-
(
ZOdiv
(
ZOdiv
n
a
)
b
*
b
)
*
a
)
%
Z
.
now
rewrite
2
!
Z
quot_0_r
,
Zrem
_0_l
.
assert
(
Z
.
rem
n
(
a
*
b
)
=
n
+
-
(
Z
.
quot
(
Z
.
quot
n
a
)
b
*
b
)
*
a
)
%
Z
.
rewrite
(
ZOmod_eq
n
(
a
*
b
))
at
1.
rewrite
Z
Odiv_ZOdiv
.
rewrite
Z
quot_Zquot
.
ring
.
rewrite
H
.
rewrite
Z
O_div
_plus
with
(
2
:=
Za
).
rewrite
Z
_quot
_plus
with
(
2
:=
Za
).
apply
sym_eq
.
apply
ZOmod_eq
.
rewrite
<-
H
.
apply
Z
Omod
_sgn2
.
apply
Z
rem
_sgn2
.
Qed
.
Theorem
ZOdiv_small_abs
:
forall
a
b
,
(
Zabs
a
<
b
)
%
Z
->
Z
Odiv
a
b
=
Z0
.
(
Zabs
a
<
b
)
%
Z
->
Z
.
quot
a
b
=
Z0
.
Proof
.
intros
a
b
Ha
.
destruct
(
Zle_or_lt
0
a
)
as
[
H
|
H
].
apply
Z
Odiv
_small
.
apply
Z
quot
_small
.
split
.
exact
H
.
now
rewrite
Zabs_eq
in
Ha
.
apply
Zopp_inj
.
rewrite
<-
Z
Odiv
_opp_l
,
Zopp_0
.
apply
Z
Odiv
_small
.
rewrite
<-
Z
quot
_opp_l
,
Zopp_0
.
apply
Z
quot
_small
.
generalize
(
Zabs_non_eq
a
).
omega
.
Qed
.
Theorem
ZOmod_small_abs
:
forall
a
b
,
(
Zabs
a
<
b
)
%
Z
->
Z
Omod
a
b
=
a
.
(
Zabs
a
<
b
)
%
Z
->
Z
.
rem
a
b
=
a
.
Proof
.
intros
a
b
Ha
.
destruct
(
Zle_or_lt
0
a
)
as
[
H
|
H
].
apply
Z
Omod
_small
.
apply
Z
rem
_small
.
split
.
exact
H
.
now
rewrite
Zabs_eq
in
Ha
.
apply
Zopp_inj
.
rewrite
<-
Z
Omod
_opp_l
.
apply
Z
Omod
_small
.
rewrite
<-
Z
rem
_opp_l
.
apply
Z
rem
_small
.
generalize
(
Zabs_non_eq
a
).
omega
.
Qed
.
Theorem
ZOdiv_plus
:
forall
a
b
c
,
(
0
<=
a
*
b
)
%
Z
->
(
Z
Odiv
(
a
+
b
)
c
=
ZOdiv
a
c
+
ZOdiv
b
c
+
ZOdiv
(
ZOmod
a
c
+
ZOmod
b
c
)
c
)
%
Z
.
(
Z
.
quot
(
a
+
b
)
c
=
Z
.
quot
a
c
+
Z
.
quot
b
c
+
Z
.
quot
(
Z
.
rem
a
c
+
Z
.
rem
b
c
)
c
)
%
Z
.
Proof
.
intros
a
b
c
Hab
.
destruct
(
Z_eq_dec
c
0
)
as
[
Zc
|
Zc
].
now
rewrite
Zc
,
4
!
Z
Odiv
_0_r
.
now
rewrite
Zc
,
4
!
Z
quot
_0_r
.
apply
Zmult_reg_r
with
(
1
:=
Zc
).
rewrite
2
!
Zmult_plus_distr_l
.
assert
(
forall
d
,
Z
Odiv
d
c
*
c
=
d
-
ZOmod
d
c
)
%
Z
.
assert
(
forall
d
,
Z
.
quot
d
c
*
c
=
d
-
Z
.
rem
d
c
)
%
Z
.
intros
d
.
rewrite
ZOmod_eq
.
ring
.
rewrite
4
!
H
.
rewrite
<-
Z
Oplus_mod
with
(
1
:=
Hab
).
rewrite
<-
Z
plus_rem
with
(
1
:=
Hab
).
ring
.
Qed
.
...
...
@@ -543,14 +543,14 @@ Qed.
Theorem
Zsame_sign_odiv
:
forall
u
v
,
(
0
<=
v
)
%
Z
->
(
0
<=
u
*
Z
Odiv
u
v
)
%
Z
.
(
0
<=
u
*
Z
.
quot
u
v
)
%
Z
.
Proof
.
intros
u
v
Hv
.
apply
Zsame_sign_imp
;
intros
Hu
.
apply
Z
O_div
_pos
with
(
2
:=
Hv
).
apply
Z
_quot
_pos
with
(
2
:=
Hv
).
now
apply
Zlt_le_weak
.
rewrite
<-
Z
Odiv
_opp_l
.
apply
Z
O_div
_pos
with
(
2
:=
Hv
).
rewrite
<-
Z
quot
_opp_l
.
apply
Z
_quot
_pos
with
(
2
:=
Hv
).
now
apply
Zlt_le_weak
.
Qed
.
...
...
src/Core/Fcore_digits.v
View file @
60631b5d
...
...
@@ -18,8 +18,8 @@ COPYING file for more details.
*
)
Require
Import
ZArith
.
Require
Import
Zquot
.
Require
Import
Fcore_Zaux
.
Require
Import
ZOdiv
.
(
**
Computes
the
number
of
bits
(
radix
2
)
of
a
positive
integer
.
...
...
@@ -40,7 +40,7 @@ Theorem digits2_Pnat_correct :
Proof
.
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
.
induction
n
;
simpl
digits2_Pnat
.
rewrite
Zpos_xI
,
2
!
Hp
.
omega
.
rewrite
(
Zpos_xO
n
),
2
!
Hp
.
...
...
@@ -52,7 +52,7 @@ Section Fcore_digits.
Variable
beta
:
radix
.
Definition
Zdigit
n
k
:=
Z
Omod
(
ZOdiv
n
(
Zpower
beta
k
))
beta
.
Definition
Zdigit
n
k
:=
Z
.
rem
(
Z
.
quot
n
(
Zpower
beta
k
))
beta
.
Theorem
Zdigit_lt
:
forall
n
k
,
...
...
@@ -68,8 +68,8 @@ Theorem Zdigit_0 :
Proof
.
intros
k
.
unfold
Zdigit
.
rewrite
Z
Odiv
_0_l
.
apply
Z
Omod
_0_l
.
rewrite
Z
quot
_0_l
.
apply
Z
rem
_0_l
.
Qed
.
Theorem
Zdigit_opp
:
...
...
@@ -78,8 +78,8 @@ Theorem Zdigit_opp :
Proof
.
intros
n
k
.
unfold
Zdigit
.
rewrite
Z
Odiv
_opp_l
.
apply
Z
Omod
_opp_l
.
rewrite
Z
quot
_opp_l
.
apply
Z
rem
_opp_l
.
Qed
.
Theorem
Zdigit_ge_Zpower_pos
:
...
...
@@ -89,8 +89,8 @@ Theorem Zdigit_ge_Zpower_pos :
Proof
.
intros
e
n
Hn
k
Hk
.
unfold
Zdigit
.
rewrite
Z
Odiv
_small
.
apply
Z
Omod
_0_l
.
rewrite
Z
quot
_small
.
apply
Z
rem
_0_l
.
split
.
apply
Hn
.
apply
Zlt_le_trans
with
(
1
:=
proj2
Hn
).
...
...
@@ -134,12 +134,12 @@ Proof.
intros
e
n
He
(
Hn1
,
Hn2
).
unfold
Zdigit
.
rewrite
<-
ZOdiv_mod_mult
.
rewrite
Z
Omod
_small
.
rewrite
Z
rem
_small
.
intros
H
.
apply
Zle_not_lt
with
(
1
:=
Hn1
).
rewrite
(
Z
O_div_mod_eq
n
(
beta
^
e
)).
rewrite
(
Z
.
quot_rem
'
n
(
beta
^
e
)).
rewrite
H
,
Zmult_0_r
,
Zplus_0_l
.
apply
Z
Omod
_lt_pos_pos
.
apply
Z
rem
_lt_pos_pos
.
apply
Zle_trans
with
(
2
:=
Hn1
).
apply
Zpower_ge_0
.
now
apply
Zpower_gt_0
.
...
...
@@ -178,10 +178,10 @@ pattern k' ; apply Zlt_0_ind with (2 := Hk').
clear
k
'
Hk
'
.
intros
k
'
IHk
'
Hk
'
k
H
.
unfold
Zdigit
.
apply
(
f_equal
(
fun
x
=>
Z
Omod
x
beta
)).
apply
(
f_equal
(
fun
x
=>
Z
.
rem
x
beta
)).
pattern
k
at
1
;
replace
k
with
(
k
-
k
'
+
k
'
)
%
Z
by
ring
.
rewrite
Zpower_plus
with
(
2
:=
Hk
'
).
apply
Z
Odiv
_mult_cancel_r
.
apply
Z
quot
_mult_cancel_r
.
apply
Zgt_not_eq
.
now
apply
Zpower_gt_0
.
now
apply
Zle_minus_le_0
.
...
...
@@ -190,13 +190,13 @@ rewrite (Zdigit_lt n) by omega.
unfold
Zdigit
.
replace
k
'
with
(
k
'
-
k
+
k
)
%
Z
by
ring
.
rewrite
Zpower_plus
with
(
2
:=
H0
).
rewrite
Zmult_assoc
,
Z
O_div
_mult
.
rewrite
Zmult_assoc
,
Z
_quot
_mult
.
replace
(
k
'
-
k
)
%
Z
with
(
k
'
-
k
-
1
+
1
)
%
Z
by
ring
.
rewrite
Zpower_exp
by
omega
.
rewrite
Zmult_assoc
.
change
(
Zpower
beta
1
)
with
(
beta
*
1
)
%
Z
.
rewrite
Zmult_1_r
.
apply
Z
O_mod
_mult
.
apply
Z
_rem
_mult
.
apply
Zgt_not_eq
.
now
apply
Zpower_gt_0
.
apply
Zle_minus_le_0
.
...
...
@@ -209,24 +209,24 @@ Qed.
Theorem
Zdigit_div_pow
:
forall
n
k
k
'
,
(
0
<=
k
)
%
Z
->
(
0
<=
k
'
)
%
Z
->
Zdigit
(
Z
Odiv
n
(
Zpower
beta
k
'
))
k
=
Zdigit
n
(
k
+
k
'
).
Zdigit
(
Z
.
quot
n
(
Zpower
beta
k
'
))
k
=
Zdigit
n
(
k
+
k
'
).
Proof
.
intros
n
k
k
'
Hk
Hk
'
.
unfold
Zdigit
.
rewrite
Z
Odiv_ZOdiv
.
rewrite
Z
quot_Zquot
.
rewrite
Zplus_comm
.
now
rewrite
Zpower_plus
.
Qed
.
Theorem
Zdigit_mod_pow
:
forall
n
k
k
'
,
(
k
<
k
'
)
%
Z
->
Zdigit
(
Z
Omod
n
(
Zpower
beta
k
'
))
k
=
Zdigit
n
k
.
Zdigit
(
Z
.
rem
n
(
Zpower
beta
k
'
))
k
=
Zdigit
n
k
.
Proof
.
intros
n
k
k
'
Hk
.
destruct
(
Zle_or_lt
0
k
)
as
[
H
|
H
].
unfold
Zdigit
.
rewrite
<-
2
!
ZOdiv_mod_mult
.
apply
(
f_equal
(
fun
x
=>
Z
Odiv
x
(
beta
^
k
))).
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
omega
.
rewrite
Zmult_comm
.
...
...
@@ -239,15 +239,15 @@ Qed.
Theorem
Zdigit_mod_pow_out
:
forall
n
k
k
'
,
(
0
<=
k
'
<=
k
)
%
Z
->
Zdigit
(
Z
Omod
n
(
Zpower
beta
k
'
))
k
=
Z0
.
Zdigit
(
Z
.
rem
n
(
Zpower
beta
k
'
))
k
=
Z0
.
Proof
.
intros
n
k
k
'
Hk
.
unfold
Zdigit
.
rewrite
ZOdiv_small_abs
.
apply
Z
Omod
_0_l
.
apply
Z
rem
_0_l
.
apply
Zlt_le_trans
with
(
Zpower
beta
k
'
).
rewrite
<-
(
Zabs_eq
(
beta
^
k
'
))
at
2
by
apply
Zpower_ge_0
.
apply
Z
Omod
_lt
.
apply
Z
rem
_lt
.
apply
Zgt_not_eq
.
now
apply
Zpower_gt_0
.
now
apply
Zpower_le
.
...
...
@@ -261,12 +261,12 @@ Fixpoint Zsum_digit f k :=
Theorem
Zsum_digit_digit
:
forall
n
k
,
Zsum_digit
(
Zdigit
n
)
k
=
Z
Omod
n
(
Zpower
beta
(
Z_of_nat
k
)).
Zsum_digit
(
Zdigit
n
)
k
=
Z
.
rem
n
(
Zpower
beta
(
Z_of_nat
k
)).
Proof
.
intros
n
.
induction
k
.
apply
sym_eq
.
apply
Z
Omod
_1_r
.
apply
Z
rem
_1_r
.
simpl
Zsum_digit
.
rewrite
IHk
.
unfold
Zdigit
.
...
...
@@ -276,7 +276,7 @@ rewrite Zmult_comm.
replace
(
beta
^
Z_of_nat
k
*
beta
)
%
Z
with
(
Zpower
beta
(
Z_of_nat
(
S
k
))).
rewrite
Zplus_comm
,
Zmult_comm
.
apply
sym_eq
.
apply
Z
O_div_mod_eq
.
apply
Z
.
quot_rem
'
.
rewrite
inj_S
.
rewrite
<-
(
Zmult_1_r
beta
)
at
3.
apply
Zpower_plus
.
...
...
@@ -348,17 +348,17 @@ Qed.
Theorem
ZOmod_plus_pow_digit
:
forall
u
v
n
,
(
0
<=
u
*
v
)
%
Z
->
(
forall
k
,
(
0
<=
k
<
n
)
%
Z
->
Zdigit
u
k
=
Z0
\
/
Zdigit
v
k
=
Z0
)
->
Z
Omod
(
u
+
v
)
(
Zpower
beta
n
)
=
(
ZOmod
u
(
Zpower
beta
n
)
+
ZOmod
v
(
Zpower
beta
n
))
%
Z
.
Z
.
rem
(
u
+
v
)
(
Zpower
beta
n
)
=
(
Z
.
rem
u
(
Zpower
beta
n
)
+
Z
.
rem
v
(
Zpower
beta
n
))
%
Z
.
Proof
.
intros
u
v
n
Huv
Hd
.
destruct
(
Zle_or_lt
0
n
)
as
[
Hn
|
Hn
].
rewrite
Z
Oplus_mod
with
(
1
:=
Huv
).
rewrite
Z
plus_rem
with
(
1
:=
Huv
).
apply
ZOmod_small_abs
.
generalize
(
Zle_refl
n
).
pattern
n
at
-
2
;
rewrite
<-
Zabs_eq
with
(
1
:=
Hn
).
rewrite
<-
(
inj_Zabs_nat
n
).
induction
(
Zabs_nat
n
)
as
[
|
p
IHp
].
now
rewrite
2
!
Z
Omod
_1_r
.
now
rewrite
2
!
Z
rem
_1_r
.
rewrite
<-
2
!
Zsum_digit_digit
.
simpl
Zsum_digit
.
rewrite
inj_S
.
...
...
@@ -385,7 +385,7 @@ apply refl_equal.
apply
Zle_bool_imp_le
.
apply
beta
.
replace
(
Zsucc
(
beta
-
1
))
with
(
Zabs
beta
).
apply
Z
Omod
_lt
.
apply
Z
rem
_lt
.
now
apply
Zgt_not_eq
.
rewrite
Zabs_eq
.
apply
Zsucc_pred
.
...
...
@@ -407,29 +407,29 @@ now rewrite Zmult_1_r.
apply
Zle_0_nat
.
easy
.
destruct
n
as
[
|
n
|
n
]
;
try
easy
.
now
rewrite
3
!
Z
Omod
_0_r
.
now
rewrite
3
!
Z
rem
_0_r
.
Qed
.
Theorem
ZOdiv_plus_pow_digit
:
forall
u
v
n
,
(
0
<=
u
*
v
)
%
Z
->
(
forall
k
,
(
0
<=
k
<
n
)
%
Z
->
Zdigit
u
k
=
Z0
\
/
Zdigit
v
k
=
Z0
)
->
Z
Odiv
(
u
+
v
)
(
Zpower
beta
n
)
=
(
ZOdiv
u
(
Zpower
beta
n
)
+
ZOdiv
v
(
Zpower
beta
n
))
%
Z
.
Z
.
quot
(
u
+
v
)
(
Zpower
beta
n
)
=
(
Z
.
quot
u
(
Zpower
beta
n
)
+
Z
.
quot
v
(
Zpower
beta
n
))
%
Z
.
Proof
.
intros
u
v
n
Huv
Hd
.
rewrite
<-
(
Zplus_0_r
(
Z
Odiv
u
(
Zpower
beta
n
)
+
ZOdiv
v
(
Zpower
beta
n
))).
rewrite
<-
(
Zplus_0_r
(
Z
.
quot
u
(
Zpower
beta
n
)
+
Z
.
quot
v
(
Zpower
beta
n
))).
rewrite
ZOdiv_plus
with
(
1
:=
Huv
).
rewrite
<-
ZOmod_plus_pow_digit
by
assumption
.
apply
f_equal
.
destruct
(
Zle_or_lt
0
n
)
as
[
Hn
|
Hn
].
apply
ZOdiv_small_abs
.
rewrite
<-
Zabs_eq
.
apply
Z
Omod
_lt
.
apply
Z
rem
_lt
.
apply
Zgt_not_eq
.
now
apply
Zpower_gt_0
.
apply
Zpower_ge_0
.
clear
-
Hn
.
destruct
n
as
[
|
n
|
n
]
;
try
easy
.
apply
Z
Odiv
_0_r
.
apply
Z
quot
_0_r
.
Qed
.
Theorem
Zdigit_plus
:
...
...
@@ -447,11 +447,11 @@ change (beta * 1)%Z with (beta ^1)%Z.
apply
ZOmod_plus_pow_digit
.
apply
Zsame_sign_trans_weak
with
v
.
intros
Zv
;
rewrite
Zv
.
apply
Z
Odiv
_0_l
.
apply
Z
quot
_0_l
.
rewrite
Zmult_comm
.
apply
Zsame_sign_trans_weak
with
u
.
intros
Zu
;
rewrite
Zu
.
apply
Z
Odiv
_0_l
.
apply
Z
quot
_0_l
.
now
rewrite
Zmult_comm
.
apply
Zsame_sign_odiv
.
apply
Zpower_ge_0
.
...
...
@@ -467,7 +467,7 @@ now rewrite 3!Zdigit_lt.
Qed
.
Definition
Zscale
n
k
:=
if
Zle_bool
0
k
then
(
n
*
Zpower
beta
k
)
%
Z
else
Z
Odiv
n
(
Zpower
beta
(
-
k
)).
if
Zle_bool
0
k
then
(
n
*
Zpower
beta
k
)
%
Z
else
Z
.
quot
n
(
Zpower
beta
(
-
k
)).
Theorem
Zdigit_scale
:
forall
n
k
k
'
,
(
0
<=
k
'
)
%
Z
->
...
...
@@ -489,7 +489,7 @@ intros k.
unfold
Zscale
.
case
Zle_bool
.
apply
Zmult_0_l
.
apply
Z
Odiv
_0_l
.
apply
Z
quot
_0_l
.
Qed
.
Theorem
Zsame_sign_scale
:
...
...
@@ -523,13 +523,13 @@ case Zle_bool_spec ; intros Hk''.
pattern
k
at
1
;
replace
k
with
(
k
+
k
'
+
-
k
'
)
%
Z
by
ring
.