...
 
Commits (149)
......@@ -4,6 +4,9 @@ ChangeLog
config.log
config.status
configure
deps.dot
deps.png
deps.map
install-sh
lia.cache
Remakefile
......@@ -11,7 +14,7 @@ Remakefile
remake
remake.exe
html/
src/Flocq_version.v
src/Version.v
*.vo
*.glob
.*.aux
......
Sylvie Boldo <sylvie.boldo@inria.fr> Sylvie Boldo <sboldo@quetsche.inria.fr>
Pierre Roux <pierre@roux01.fr> Pierre Roux <proux@lri.fr>
Sylvie Boldo <sylvie.boldo@inria.fr> <sboldo@quetsche.inria.fr>
Xavier Leroy <xavier.leroy@college-de-france.fr> <xavier.leroy@inria.fr>
Pierre Roux <pierre.roux@onera.fr> <pierre@roux01.fr>
Pierre Roux <pierre.roux@onera.fr> <proux@lri.fr>
Prerequisites
-------------
You will need the Coq proof assistant (>= 8.4) with a Reals theory
compiled in.
The .tar.gz file is distributed with a working set of configure files. They
are not in the git repository though. Consequently, if you are building from
git, you will need autoconf (>= 2.59).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
$ ./configure && ./remake && ./remake install
The environment variable COQC can be passed to the configure script in order
to set the Coq compiler command. The configure script defaults to "coqc".
Similarly, COQDEP can be used to specify the location of "coqdep". The
COQBIN environment variable can be used to set both variables at once.
The option "--libdir=DIR" can be set to the directory where the compiled
library files should be installed by "make install". By default, the
target directory is "`$COQC -where`/user-contrib/Flocq".
The files are compiled at a logical location starting with "Flocq".
Installation instructions
=========================
Prerequisites
-------------
You will need the [Coq proof assistant](https://coq.inria.fr/) (>= 8.7)
with the `Reals` theory compiled in.
The `.tar.gz` file is distributed with a working set of configure files. They
are not in the git repository though. Consequently, if you are building from
git, you will need `autoconf` (>= 2.59).
Configuring, compiling and installing
-------------------------------------
Ideally, you should just have to type:
./configure && ./remake --jobs=2 && ./remake install
The environment variable `COQC` can be passed to the configure script in order
to set the Coq compiler command. The configure script defaults to `coqc`.
Similarly, `COQDEP` can be used to specify the location of `coqdep`. The
`COQBIN` environment variable can be used to set both variables at once.
The option `--libdir=DIR` can be set to the directory where the compiled
library files should be installed by `./remake install`. By default, the
target directory is `` `$COQC -where`/user-contrib/Flocq ``.
The files are compiled at a logical location starting with `Flocq`.
Version 2.5.2:
- ensured compatibility from Coq 8.4 to 8.6
Version 2.5.1:
- ensured compatibility with both Coq 8.4 and 8.5
Version 2.5.0:
- ensured compatibility with both Coq 8.4 and 8.5
(Flocq now provides its own version of iter_pos)
- redefined ulp, so that ulp(0) is meaningful
- renamed, generalized, and added lemmas in Fcore_ulp
- extended predecessor and successor to nonpositive values
(the previous definition of pred has been renamed pred_pos)
- removed some hypotheses on lemmas of Fprop_relative
- added more examples
. Average: proof on Sterbenz's average and correctly-rounded average
. Cody_Waite: Cody & Waite's approximation of exponential
. Compute: effective FP computations with an example of sqrt(sqr(x))
in radix 5 and precision 3
. Division_u16: integer division using floating-point FMA
. Triangle: Kahan's algorithm for the area of a triangle
Version 2.4.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
- added theorems about double rounding being innocuous (Fappli_double_round.v)
- added example about double rounding in odd radix
- improved a bit the efficiency of IEEE-754 arithmetic
Version 2.3.0:
- moved some lemmas from Fcalc_digits to Fcore_digits and made them axiom-free
- used the square root from the standard library instead of a custom one
- added an example about sqrt(sqr(x))
Version 2.2.2:
- fixed install target for case-insensitive filesystems
Version 2.2.1:
- fixed regeneration of Flocq_version.v
Version 2.2.0:
- added theorems about rounding to odd and double rounding
- improved handling of special values of IEEE-754 arithmetic
Version 2.1.0:
- ensured compatibility with both Coq 8.3 and 8.4
- improved support for rounding toward and away from zero
- proved that formats are stable by arbitrary rounding or ulp addition
- generalized usage of ln_beta
Version 2.0.0:
- changed rounding modes from records to R -> Z functions as arguments
to the round function
. rndDN -> Zfloor
. rndUP -> Zceil
. rndZE -> Ztrunc
. rndNE -> ZnearestE
. rndNA -> ZnearestA
- added typeclasses for automatic inference of properties:
. Valid_exp for Z -> Z functions describing formats
. Valid_rnd for R -> Z functions describing rounding modes
. Exp_not_FTZ for Z -> Z functions describing formats with subnormal
. Monotone_exp for Z -> Z functions describing regular formats
. Exists_NE for radix/formats supporting rounding to nearest even
- removed theorems superseded by typeclasses:
. FIX_exp_correct, FLX_exp_correct, FLT_exp_correct, FTZ_exp_correct
. FIX_exp_monotone, FLX_exp_monotone, FLT_monotone
. Rnd_NE_pt_FIX, Rnd_NE_pt_FLX, Rnd_NE_pt_FLT
. round_NE_pt_FLX, round_NE_pt_FLT
. Zrnd_opp_le, Zrnd_Z2R_opp
- removed example file Fappli_sqrt_FLT_ne
- split theorems on equivalence between specific and generic formats
into both directions:
. FIX_format_generic and generic_format_FIX
. FLX_format_generic and generic_format_FLX
. FLT_format_generic and generic_format_FLT
. FTZ_format_generic and generic_format_FTZ
- modified correctness theorems for IEEE-754 operators so that they also
mention finiteness of the results
- added a Flocq_version.Flocq_version Coq variable for Flocq detection
and version testing in configure scripts
- moved parts of some files into other files:
. Fcore_Raux -> Fcore_Zaux
. Fcalc_digits -> Fcore_digits
. Fappli_IEEE -> Fappli_IEEE_bits
- renamed functions:
. canonic_exponent -> canonic_exp
. digits -> Zdigits
. bounded_prec -> canonic_mantissa
. Bsign_FF -> sign_FF
. shl -> shl_align
. shl_fexp -> shl_align_fexp
. binary_round_sign -> binary_round_aux
. binary_round_sign_shl -> binary_round
- renamed theorems more uniformly:
. Rabs_Rminus_pos -> Rabs_minus_le
. exp_increasing_weak -> exp_le
. ln_beta_monotone -> ln_beta_le
. ln_beta_monotone_abs -> ln_beta_le_abs
. abs_F2R -> F2R_Zabs (changed direction)
. opp_F2R -> F2R_Zopp (changed direction)
. scaled_mantissa_bpow -> scaled_mantissa_mult_bpow
. round_monotone -> round_le
. round_monotone_l -> round_ge_generic
. round_monotone_r -> round_le_generic
. round_monotone_abs_l -> abs_round_ge_generic
. round_monotone_abs_r -> abs_round_le_generic
. generic_format_canonic_exponent -> generic_format_F2R (modified hypothesis)
. canonic_exponent_round -> canonic_exp_round_ge
. generic_N_pt -> round_N_pt
. round_pred_pos_imp_rnd -> round_pred_ge_0
. round_pred_rnd_imp_pos -> round_pred_gt_0
. round_pred_neg_imp_rnd -> round_pred_le_0
. round_pred_rnd_imp_neg -> round_pred_lt_0
. ulp_le_pos -> ulp_le_id
. succ_lt_le -> succ_le_lt
. ulp_monotone -> ulp_le
. ulp_DN_pt_eq -> ulp_DN
. format_pred -> generic_format_pred
. pred_ulp -> pred_plus_ulp
. pred_lt -> pred_lt_id
. FLT_generic_format_FLX -> generic_format_FLT_FLX
. FLX_generic_format_FLT -> generic_format_FLX_FLT
. FIX_generic_format_FLT -> generic_format_FIX_FLT
. FLT_generic_format_FIX -> generic_format_FLT_FIX
. FLT_round_FLX -> round_FLT_FLX
. FTZ_round -> round_FTZ_FLX
. FTZ_round_small -> round_FTZ_small
. FLT_canonic_FLX -> canonic_exp_FLT_FLX
. FLT_canonic_FIX -> canonic_exp_FLT_FIX
. canonic_exponent_opp -> canonic_exp_opp
. canonic_exponent_abs -> canonic_exp_abs
. canonic_exponent_fexp -> canonic_exp_fexp
. canonic_exponent_fexp_pos -> canonic_exp_fexp_pos
. canonic_exponent_DN -> canonic_exp_DN
. canonic_exp_ge -> abs_lt_bpow_prec (modified hypotheses)
. Fopp_F2R -> F2R_opp
. Fabs_F2R -> F2R_abs
. plus_F2R -> F2R_plus
. minus_F2R -> F2R_minus
. mult_F2R -> F2R_mult
. digits_abs -> Zdigits_abs
. digits_ge_0 -> Zdigits_ge_0
. digits_gt_0 -> Zdigits_gt_0
. ln_beta_F2R_Zdigits -> ln_beta_F2R_Zdigits
. digits_shift -> Zdigits_mult_Zpower
. digits_Zpower -> Zdigits_Zpower
. digits_le -> Zdigits_le
. lt_digits -> lt_Zdigits
. Zpower_le_digits -> Zpower_le_Zdigits
. digits_le_Zpower -> Zdigits_le_Zpower
. Zpower_gt_digits -> Zpower_gt_Zdigits
. digits_gt_Zpower -> Zdigits_gt_Zpower
. digits_mult_strong -> Zdigits_mult_strong
. digits_mult -> Zdigits_mult
. digits_mult_ge -> Zdigits_mult_ge
. digits_shr -> Zdigits_div_Zpower
. format_add -> generic_format_plus_prec (modified hypothesis)
. format_nx -> ex_Fexp_canonic
. generic_relative_error -> relative_error
. generic_relative_error_ex -> relative_error_ex
. generic_relative_error_F2R -> relative_error_F2R_emin
. generic_relative_error_F2R_ex -> relative_error_F2R_emin_ex
. generic_relative_error_2 -> relative_error_round
. generic_relative_error_F2R_2 -> relative_error_round_F2R_emin
. generic_relative_error_N -> relative_error_N
. generic_relative_error_N_ex -> relative_error_N_ex
. generic_relative_error_N_F2R -> relative_error_N_F2R_emin
. generic_relative_error_N_F2R_ex -> relative_error_N_F2R_emin_ex
. generic_relative_error_N_2 -> relative_error_N_round
. generic_relative_error_N_F2R_2 -> relative_error_N_round_F2R_emin
. relative_error_FLT_F2R -> relative_error_FLT_F2R_emin
. relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex
. relative_error_N_FLT_2 -> relative_error_N_FLT_round
. relative_error_N_FLT_F2R -> relative_error_N_FLT_F2R_emin
. relative_error_N_FLT_F2R_ex -> relative_error_N_FLT_F2R_emin_ex
. relative_error_N_FLT_F2R_2 -> relative_error_N_FLT_round_F2R_emin
. relative_error_FLX_2 -> relative_error_FLX_round
. relative_error_N_FLX_2 -> relative_error_N_FLX_round
. canonic_bounded_prec -> canonic_canonic_mantissa
. B2R_lt_emax -> abs_B2R_lt_emax
. binary_unicity -> B2FF_inj
. finite_binary_unicity -> B2R_inj
. binary_round_sign_correct -> binary_round_aux_correct
. shl_correct -> shl_align_correct
. snd_shl -> snd_shl_align
. shl_fexp_correct -> shl_align_fexp_correct
. binary_round_sign_shl_correct -> binary_round_correct
Version 1.4.0:
- improved efficiency of IEEE-754 addition
- fixed compilation with Coq 8.3
Version 1.3:
- fixed overflow handling in IEEE-754 formats with directed rounding
Version 1.2:
- added IEEE-754 binary32 and 64 formats, including infinities and NaN
Version 1.1:
- simplified effective rounding for negative reals
- proved monotonicity of exponent functions for common formats
Version 1.0:
- initial release
Version 3.2.0
-------------
* added function `Bfma`
* ensured compatibility from Coq 8.7 to 8.10
Version 3.1.0
-------------
* changed matching order in `Bcompare`
* improved behavior of `Binary.v` functions with respect to NaNs
* ensured compatibility from Coq 8.7 to 8.9
* added functions `Bpred` and `Bsucc`
* added theorems on optimal relative error bounds for plus and square root
* made installation also install source files
Version 3.0.0
-------------
* stripped the `F*_` prefix from all the file names, renamed some files:
- `Definitions -> Defs`
- `Appli -> IEEE754`
* renamed `ln_beta` into `mag`
* renamed `canonic_exp` into `cexp`, `canonic` into `canonical`
* renamed all theorems ending with `unicity` by `unique`
* changed `FLX_`, `FIX_`, `FLT_`, `FLXN_`, `FTZ_format` into inductive types
* changed `nan_pl` into a boolean predicate
* replaced `Z2R` with Coq 8.7's `IZR`
* removed `Zeven` and its theorems in favor of `Z.even` of the standard library
* modified statements of `Rcompare_sqr`, `ulp_DN`, `mult_error_FLT`, `mag_div`
* added theorems about the remainder being in the format (in `Div_sqrt_error.v`)
* made `Fdiv_core` and `Fsqrt_core` generic with respect to the format
* renamed theorems more uniformly:
- `bpow_plus1 -> bpow_plus_1`
- `mag_lt_pos -> lt_mag`
- `F2R_le_reg -> le_F2R`
- `F2R_le_compat -> F2R_le`
- `F2R_lt_reg -> lt_F2R`
- `F2R_lt_compat -> F2R_lt`
- `F2R_eq_reg -> eq_F2R`
- `F2R_eq_compat -> F2R_eq`
- `F2R_eq_0_reg -> eq_0_F2R`
- `F2R_ge_0_reg -> ge_0_F2R`
- `F2R_le_0_reg -> le_0_F2R`
- `F2R_gt_0_reg -> gt_0_F2R`
- `F2R_lt_0_reg -> lt_0_F2R`
- `F2R_le_0_compat -> F2R_le_0`
- `F2R_ge_0_compat -> F2R_ge_0`
- `F2R_gt_0_compat -> F2R_gt_0`
- `F2R_lt_0_compat -> F2R_lt_0`
- `F2R_neq_0_compat -> F2R_neq_0`
- `Fnum_ge_0_compat -> Fnum_ge_0`
- `Fnum_le_0_compat -> Fnum_le_0`
- `round_ZR_pos -> round_ZR_DN`
- `round_ZR_neg -> round_ZR_UP`
- `round_AW_pos -> round_ZR_UP`
- `round_AW_neg -> round_ZR_DN`
- `Znearest_N -> Znearest_half`
- `Rnd_DN_UP_pt_N -> Rnd_N_pt_DN_UP`
- `Rnd_DN_pt_N -> Rnd_N_pt_DN`
- `Rnd_UP_pt_N -> Rnd_N_pt_UP`
- `Rnd_DN_UP_pt_sym -> Rnd_UP_pt_opp`
- `Rnd_UP_DN_pt_sym -> Rnd_DN_pt_opp`
- `Rnd_DN_UP_sym -> Rnd_DN_opp`
- `Rnd_N_pt_sym -> Rnd_N_pt_opp_inv`
- `Rnd_N_pt_pos -> Rnd_N_pt_ge_0`
- `Rnd_N_pt_neg -> Rnd_N_pt_le_0`
- `Rnd_NG_pt_sym -> Rnd_NG_pt_opp_inv`
- `Rnd_NA_N_pt -> Rnd_NA_pt_N`
- `Rnd_odd_pt_sym -> Rnd_odd_pt_opp_inv`
- `le_pred_lt -> pred_ge_gt`
- `lt_succ_le -> succ_gt_ge`
- `le_round_DN_lt_UP -> round_DN_ge_UP_gt`
- `round_UP_le_gt_DN -> round_UP_le_DN_lt`
- `round_DN_eq_betw -> round_DN_eq`
- `round_UP_eq_betw -> round_UP_eq`
- `round_plus_eq_zero -> round_plus_neq_0` (and modified statement)
- `round_odd_prop -> round_N_odd`
- `double_round_*_beta_ge_* -> round_round_*_radix_ge_*`
- `double_round_* -> round_round_*`
Version 2.6.1
-------------
* ensured compatibility from Coq 8.4 to 8.8
Version 2.6.0
-------------
* ensured compatibility from Coq 8.4 to 8.7
* removed some hypotheses on some lemmas of `Fcore_ulp`
* added lemmas to `Fprop_plus_error`
* improved examples
Version 2.5.2
-------------
* ensured compatibility from Coq 8.4 to 8.6
Version 2.5.1
-------------
* ensured compatibility with both Coq 8.4 and 8.5
Version 2.5.0
-------------
* ensured compatibility with both Coq 8.4 and 8.5
(Flocq now provides its own version of `iter_pos`)
* redefined `ulp`, so that `ulp 0` is meaningful
* renamed, generalized, and added lemmas in `Fcore_ulp`
* extended predecessor and successor to nonpositive values
(the previous definition of `pred` has been renamed `pred_pos`)
* removed some hypotheses on lemmas of `Fprop_relative.v`
* added more examples
- `Average`: proof on Sterbenz's average and correctly-rounded average
- `Cody_Waite`: Cody & Waite's approximation of exponential
- `Compute`: effective FP computations with an example of `sqrt(sqr(x))`
in radix 5 and precision 3
- `Division_u16`: integer division using floating-point FMA
- `Triangle`: Kahan's algorithm for the area of a triangle
Version 2.4.0
-------------
* moved some lemmas from `Fcalc_digits.v` to `Fcore_digits.v` and made them axiom-free
* added theorems about double rounding being innocuous (`Fappli_double_round.v`)
* added example about double rounding in odd radix
* improved a bit the efficiency of IEEE-754 arithmetic
Version 2.3.0
-------------
* moved some lemmas from `Fcalc_digits.v` to `Fcore_digits.v` and made them axiom-free
* used the square root from the standard library instead of a custom one
* added an example about `sqrt(sqr(x))`
Version 2.2.2
-------------
* fixed `install` target for case-insensitive filesystems
Version 2.2.1
-------------
* fixed regeneration of `Flocq_version.v`
Version 2.2.0
-------------
* added theorems about rounding to odd and double rounding
* improved handling of special values of IEEE-754 arithmetic
Version 2.1.0
-------------
* ensured compatibility with both Coq 8.3 and 8.4
* improved support for rounding toward and away from zero
* proved that formats are stable by arbitrary rounding or ulp addition
* generalized usage of `ln_beta`
Version 2.0.0
-------------
* changed rounding modes from records to `R -> Z` functions as arguments
to the `round` function
- `rndDN -> Zfloor`
- `rndUP -> Zceil`
- `rndZE -> Ztrunc`
- `rndNE -> ZnearestE`
- `rndNA -> ZnearestA`
* added typeclasses for automatic inference of properties:
- `Valid_exp` for `Z -> Z` functions describing formats
- `Valid_rnd` for `R -> Z` functions describing rounding modes
- `Exp_not_FTZ` for `Z -> Z` functions describing formats with subnormal
- `Monotone_exp` for `Z -> Z` functions describing regular formats
- `Exists_NE` for radix/formats supporting rounding to nearest even
* removed theorems superseded by typeclasses:
- `FIX_exp_correct`, `FLX_exp_correct`, `FLT_exp_correct`, `FTZ_exp_correct`
- `FIX_exp_monotone`, `FLX_exp_monotone`, `FLT_monotone`
- `Rnd_NE_pt_FIX`, `Rnd_NE_pt_FLX`, `Rnd_NE_pt_FLT`
- `round_NE_pt_FLX`, `round_NE_pt_FLT`
- `Zrnd_opp_le`, `Zrnd_Z2R_opp`
* removed example file `Fappli_sqrt_FLT_ne.v`
* split theorems on equivalence between specific and generic formats
into both directions:
- `FIX_format_generic` and `generic_format_FIX`
- `FLX_format_generic` and `generic_format_FLX`
- `FLT_format_generic` and `generic_format_FLT`
- `FTZ_format_generic` and `generic_format_FTZ`
* modified correctness theorems for IEEE-754 operators so that they also
mention finiteness of the results
* added a `Flocq_version.Flocq_version` Coq variable for Flocq detection
and version testing in configure scripts
* moved parts of some files into other files:
- `Fcore_Raux -> Fcore_Zaux`
- `Fcalc_digits -> Fcore_digits`
- `Fappli_IEEE -> Fappli_IEEE_bits`
* renamed functions:
- `canonic_exponent -> canonic_exp`
- `digits -> Zdigits`
- `bounded_prec -> canonic_mantissa`
- `Bsign_FF -> sign_FF`
- `shl -> shl_align`
- `shl_fexp -> shl_align_fexp`
- `binary_round_sign -> binary_round_aux`
- `binary_round_sign_shl -> binary_round`
* renamed theorems more uniformly:
- `Rabs_Rminus_pos -> Rabs_minus_le`
- `exp_increasing_weak -> exp_le`
- `ln_beta_monotone -> ln_beta_le`
- `ln_beta_monotone_abs -> ln_beta_le_abs`
- `abs_F2R -> F2R_Zabs` (changed direction)
- `opp_F2R -> F2R_Zopp` (changed direction)
- `scaled_mantissa_bpow -> scaled_mantissa_mult_bpow`
- `round_monotone -> round_le`
- `round_monotone_l -> round_ge_generic`
- `round_monotone_r -> round_le_generic`
- `round_monotone_abs_l -> abs_round_ge_generic`
- `round_monotone_abs_r -> abs_round_le_generic`
- `generic_format_canonic_exponent -> generic_format_F2R` (modified hypothesis)
- `canonic_exponent_round -> canonic_exp_round_ge`
- `generic_N_pt -> round_N_pt`
- `round_pred_pos_imp_rnd -> round_pred_ge_0`
- `round_pred_rnd_imp_pos -> round_pred_gt_0`
- `round_pred_neg_imp_rnd -> round_pred_le_0`
- `round_pred_rnd_imp_neg -> round_pred_lt_0`
- `ulp_le_pos -> ulp_le_id`
- `succ_lt_le -> succ_le_lt`
- `ulp_monotone -> ulp_le`
- `ulp_DN_pt_eq -> ulp_DN`
- `format_pred -> generic_format_pred`
- `pred_ulp -> pred_plus_ulp`
- `pred_lt -> pred_lt_id`
- `FLT_generic_format_FLX -> generic_format_FLT_FLX`
- `FLX_generic_format_FLT -> generic_format_FLX_FLT`
- `FIX_generic_format_FLT -> generic_format_FIX_FLT`
- `FLT_generic_format_FIX -> generic_format_FLT_FIX`
- `FLT_round_FLX -> round_FLT_FLX`
- `FTZ_round -> round_FTZ_FLX`
- `FTZ_round_small -> round_FTZ_small`
- `FLT_canonic_FLX -> canonic_exp_FLT_FLX`
- `FLT_canonic_FIX -> canonic_exp_FLT_FIX`
- `canonic_exponent_opp -> canonic_exp_opp`
- `canonic_exponent_abs -> canonic_exp_abs`
- `canonic_exponent_fexp -> canonic_exp_fexp`
- `canonic_exponent_fexp_pos -> canonic_exp_fexp_pos`
- `canonic_exponent_DN -> canonic_exp_DN`
- `canonic_exp_ge -> abs_lt_bpow_prec` (modified hypotheses)
- `Fopp_F2R -> F2R_opp`
- `Fabs_F2R -> F2R_abs`
- `plus_F2R -> F2R_plus`
- `minus_F2R -> F2R_minus`
- `mult_F2R -> F2R_mult`
- `digits_abs -> Zdigits_abs`
- `digits_ge_0 -> Zdigits_ge_0`
- `digits_gt_0 -> Zdigits_gt_0`
- `ln_beta_F2R_Zdigits -> ln_beta_F2R_Zdigits`
- `digits_shift -> Zdigits_mult_Zpower`
- `digits_Zpower -> Zdigits_Zpower`
- `digits_le -> Zdigits_le`
- `lt_digits -> lt_Zdigits`
- `Zpower_le_digits -> Zpower_le_Zdigits`
- `digits_le_Zpower -> Zdigits_le_Zpower`
- `Zpower_gt_digits -> Zpower_gt_Zdigits`
- `digits_gt_Zpower -> Zdigits_gt_Zpower`
- `digits_mult_strong -> Zdigits_mult_strong`
- `digits_mult -> Zdigits_mult`
- `digits_mult_ge -> Zdigits_mult_ge`
- `digits_shr -> Zdigits_div_Zpower`
- `format_add -> generic_format_plus_prec` (modified hypothesis)
- `format_nx -> ex_Fexp_canonic`
- `generic_relative_error -> relative_error`
- `generic_relative_error_ex -> relative_error_ex`
- `generic_relative_error_F2R -> relative_error_F2R_emin`
- `generic_relative_error_F2R_ex -> relative_error_F2R_emin_ex`
- `generic_relative_error_2 -> relative_error_round`
- `generic_relative_error_F2R_2 -> relative_error_round_F2R_emin`
- `generic_relative_error_N -> relative_error_N`
- `generic_relative_error_N_ex -> relative_error_N_ex`
- `generic_relative_error_N_F2R -> relative_error_N_F2R_emin`
- `generic_relative_error_N_F2R_ex -> relative_error_N_F2R_emin_ex`
- `generic_relative_error_N_2 -> relative_error_N_round`
- `generic_relative_error_N_F2R_2 -> relative_error_N_round_F2R_emin`
- `relative_error_FLT_F2R -> relative_error_FLT_F2R_emin`
- `relative_error_FLT_F2R_ex -> relative_error_FLT_F2R_emin_ex`
- `relative_error_N_FLT_2 -> relative_error_N_FLT_round`
- `relative_error_N_FLT_F2R -> relative_error_N_FLT_F2R_emin`
- `relative_error_N_FLT_F2R_ex -> relative_error_N_FLT_F2R_emin_ex`
- `relative_error_N_FLT_F2R_2 -> relative_error_N_FLT_round_F2R_emin`
- `relative_error_FLX_2 -> relative_error_FLX_round`
- `relative_error_N_FLX_2 -> relative_error_N_FLX_round`
- `canonic_bounded_prec -> canonic_canonic_mantissa`
- `B2R_lt_emax -> abs_B2R_lt_emax`
- `binary_unicity -> B2FF_inj`
- `finite_binary_unicity -> B2R_inj`
- `binary_round_sign_correct -> binary_round_aux_correct`
- `shl_correct -> shl_align_correct`
- `snd_shl -> snd_shl_align`
- `shl_fexp_correct -> shl_align_fexp_correct`
- `binary_round_sign_shl_correct -> binary_round_correct`
Version 1.4.0
-------------
* improved efficiency of IEEE-754 addition
* fixed compilation with Coq 8.3
Version 1.3
-----------
* fixed overflow handling in IEEE-754 formats with directed rounding
Version 1.2
-----------
* added IEEE-754 binary32 and 64 formats, including infinities and NaN
Version 1.1
-----------
* simplified effective rounding for negative reals
* proved monotonicity of exponent functions for common formats
Version 1.0
-----------
* initial release
The Flocq library provides vernacular files formalizing multi-radix
multi-precision fixed- and floating-point arithmetic for the Coq proof
assistant.
This package is free software; you can redistribute it and/or modify it
under the terms of GNU Lesser General Public License (see the COPYING
file). Authors are Sylvie Boldo <sylvie.boldo@inria.fr> and Guillaume
Melquiond <guillaume.melquiond@inria.fr>.
FLOCQ
=====
The Flocq library provides vernacular files formalizing multi-radix
multi-precision fixed- and floating-point arithmetic for the
[Coq proof assistant](https://coq.inria.fr/).
PROJECT HOME
------------
Homepage: http://flocq.gforge.inria.fr/
Repository: https://gitlab.inria.fr/flocq/flocq
Bug tracker: https://gitlab.inria.fr/flocq/flocq/issues
COPYRIGHT
---------
This package is free software; you can redistribute it and/or modify it
under the terms of GNU Lesser General Public License (see the
[COPYING](COPYING) file). Authors are Sylvie Boldo <sylvie.boldo@inria.fr>
and Guillaume Melquiond <guillaume.melquiond@inria.fr>.
INSTALLATION
------------
See the file [INSTALL.md](INSTALL.md).
FILES = \
Flocq_version.v \
Core/Fcore_Raux.v \
Core/Fcore_Zaux.v \
Core/Fcore_defs.v \
Core/Fcore_digits.v \
Core/Fcore_float_prop.v \
Core/Fcore_FIX.v \
Core/Fcore_FLT.v \
Core/Fcore_FLX.v \
Core/Fcore_FTZ.v \
Core/Fcore_generic_fmt.v \
Core/Fcore_rnd.v \
Core/Fcore_rnd_ne.v \
Core/Fcore_ulp.v \
Core/Fcore.v \
Calc/Fcalc_bracket.v \
Calc/Fcalc_digits.v \
Calc/Fcalc_div.v \
Calc/Fcalc_ops.v \
Calc/Fcalc_round.v \
Calc/Fcalc_sqrt.v \
Prop/Fprop_div_sqrt_error.v \
Prop/Fprop_mult_error.v \
Prop/Fprop_plus_error.v \
Prop/Fprop_relative.v \
Prop/Fprop_Sterbenz.v \
Appli/Fappli_rnd_odd.v \
Appli/Fappli_IEEE.v \
Appli/Fappli_IEEE_bits.v \
Appli/Fappli_double_round.v
Version.v \
Core/Raux.v \
Core/Zaux.v \
Core/Defs.v \
Core/Digits.v \
Core/Float_prop.v \
Core/FIX.v \
Core/FLT.v \
Core/FLX.v \
Core/FTZ.v \
Core/Generic_fmt.v \
Core/Round_pred.v \
Core/Round_NE.v \
Core/Ulp.v \
Core/Core.v \
Calc/Bracket.v \
Calc/Div.v \
Calc/Operations.v \
Calc/Round.v \
Calc/Sqrt.v \
Prop/Div_sqrt_error.v \
Prop/Mult_error.v \
Prop/Plus_error.v \
Prop/Relative.v \
Prop/Sterbenz.v \
Prop/Round_odd.v \
Prop/Double_rounding.v \
IEEE754/Binary.v \
IEEE754/Bits.v \
Pff/Pff.v \
Pff/Pff2FlocqAux.v \
Pff/Pff2Flocq.v
OBJS = $(addprefix src/,$(addsuffix o,$(FILES)))
EXAMPLES = \
Average.v \
Compute.v \
Double_round_beta_odd.v \
Double_rounding_odd_radix.v \
Homogen.v
MORE_EXAMPLES = \
......@@ -58,8 +60,8 @@ check-more: $(MOBJS)
Remakefile: Remakefile.in config.status
./config.status Remakefile
src/Flocq_version.v: src/Flocq_version.v.in config.status
./config.status src/Flocq_version.v
src/Version.v: src/Version.v.in config.status
./config.status src/Version.v
configure config.status: configure.in
autoconf
......@@ -69,9 +71,13 @@ configure config.status: configure.in
@COQDEP@ -R src Flocq $< | @REMAKE@ -r $@
@COQC@ -R src Flocq $<
examples/%.vo: examples/%.v
@COQDEP@ -R src Flocq -R examples FlocqEx $< | @REMAKE@ -r $@
@COQC@ -R src Flocq -R examples FlocqEx $<
clean:
rm -f $(OBJS) $(EOBJS) $(MOBJS) src/*.glob examples/*.glob
for d in src src/Core src/Calc src/Prop src/Appli examples; do \
for d in src src/Core src/Calc src/Prop src/Pff src/IEEE754 examples; do \
rm -f $d/.coq-native/*.o $d/.coq-native/*.cm*; done
find . -type d -name ".coq-native" -empty -prune -exec rmdir "{}" \;
......@@ -79,8 +85,39 @@ html/index.html: $(OBJS)
rm -rf html
mkdir -p html
@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
--coqlib http://coq.inria.fr/distrib/current/stdlib/ \
--coqlib http://coq.inria.fr/distrib/current/stdlib \
$(addprefix src/,$(FILES))
for f in html/*.html; do
sed -e 's;<a href="index.html">Index</a>;Go back to the <a href="../index.html">Main page</a> or <a href="index.html">Index</a>.;' -i $f
done
deps.dot: $(addprefix src/,$(FILES)) Remakefile.in
(echo "digraph flocq_deps { pack=true; rank=max;"
echo "node [shape=ellipse, style=filled, URL=\"html/Flocq.\N.html\", color=black];"
echo '{ rank=same; "Core.Zaux"; "Core.Raux"; }'
echo '{ rank=same; "Core.FLX"; "Core.FIX"; "Core.Round_NE"; "Calc.Operations"; }'
echo '{ rank=same; "Core.FLT"; "Core.FTZ"; }'
echo '{ rank=same; "Core.Generic_fmt"; "Core.Ulp"; }'
echo '{ rank=same; "IEEE754.Binary"; "IEEE754.Bits"; }'
echo '{ rank=same; "Pff.Pff2FlocqAux"; "Pff.Pff2Flocq"; }'
(cd src ; @COQDEP@ -R . Flocq $(FILES)) |
sed -n -e 's,/,.,g;s/[.]vo.*: [^ ]*[.]v//p' |
while read src dst; do
color=$$(echo "$src" | sed -e 's,Core.*,turquoise,;s,Calc.*,plum,;s,Prop.*,lightcoral,;s,Pff.*,yellow,;s,IEEE754.*,cornflowerblue,;s,Version.*,white,')
echo "\"$src\" [fillcolor=$color];"
for d in $dst; do
echo "\"$src\" -> \"${d%.vo}\" ;"
done
done;
echo "}") | tred > $@
deps.png: deps.dot
dot -T png deps.dot > deps.png
deps.map: deps.dot
dot -T cmap deps.dot | sed -e 's,>$,/>,' > deps.map
doc: html/index.html
......@@ -88,16 +125,15 @@ install:
prefix=@prefix@
exec_prefix=@exec_prefix@
mkdir -p @libdir@
for d in Core Calc Prop Appli; do mkdir -p @libdir@/$d; done
for d in Core Calc Prop IEEE754 Pff; do mkdir -p @libdir@/$d; done
for f in $(OBJS); do cp $f @libdir@/${f#src/}; done
for f in $(FILES); do cp src/$f @libdir@/$f; done
( cd src && find . -type d -name ".coq-native" -exec cp -RT "{}" "@libdir@/{}" \; )
EXTRA_DIST = \
configure
REMOVE_FROM_DIST = \
src/Appli/Fappli_Axpy.v \
src/Translate/
REMOVE_FROM_DIST =
dist: $(EXTRA_DIST)
PACK=@PACKAGE_TARNAME@-@PACKAGE_VERSION@
......
-R src Flocq
AC_INIT([Flocq], [2.5.2],
AC_INIT([Flocq], [3.2.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......@@ -51,7 +51,7 @@ fi
AC_MSG_RESULT([$COQDOC])
if test "$libdir" = '${exec_prefix}/lib'; then
libdir="`$COQC -where`/user-contrib/Flocq"
libdir="`$COQC -where | tr -d '\r' | tr '\\\\' '/'`/user-contrib/Flocq"
fi
AC_MSG_NOTICE([building remake...])
......@@ -68,5 +68,5 @@ MINGW*)
;;
esac
AC_CONFIG_FILES([Remakefile src/Flocq_version.v])
AC_CONFIG_FILES([Remakefile src/Version.v])
AC_OUTPUT
Require Import Reals Fourier Psatz.
Require Import Fcore.
Require Import Fprop_plus_error.
(**
This example is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2014-2018 Sylvie Boldo
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)
Require Import Reals Psatz.
From Flocq Require Import Core Plus_error.
Open Scope R_scope.
......@@ -42,9 +58,9 @@ Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Notation format := (generic_format radix2 (FLT_exp emin prec)).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation round_flt :=(round radix2 (FLT_exp emin prec) ZnearestE).
Notation ulp_flt :=(ulp radix2 (FLT_exp emin prec)).
Notation cexp := (canonic_exp radix2 (FLT_exp emin prec)).
Notation cexp := (cexp radix2 (FLT_exp emin prec)).
Notation pred_flt := (pred radix2 (FLT_exp emin prec)).
Lemma FLT_format_double: forall u, format u -> format (2*u).
......@@ -52,35 +68,32 @@ Proof with auto with typeclass_instances.
intros u Fu.
apply generic_format_FLT.
apply FLT_format_generic in Fu...
destruct Fu as (uf, (H1,(H2,H3))).
destruct Fu as [uf H1 H2 H3].
exists (Float radix2 (Fnum uf) (Fexp uf+1)).
split.
rewrite H1; unfold F2R; simpl.
rewrite bpow_plus, bpow_1.
simpl;ring.
split.
now simpl.
simpl; apply Zle_trans with (1:=H3).
omega.
easy.
apply Z.le_trans with (1:=H3).
apply Zle_succ.
Qed.
Lemma FLT_format_half: forall u,
Lemma FLT_format_half: forall u,
format u -> bpow (prec+emin) <= Rabs u -> format (u/2).
Proof with auto with typeclass_instances.
intros u Fu H.
apply FLT_format_generic in Fu...
destruct Fu as ((n,e),(H1,(H2,H3))).
destruct Fu as [[n e] H1 H2 H3].
simpl in H1, H2, H3.
apply generic_format_FLT.
exists (Float radix2 n (e-1)).
split; simpl.
rewrite H1; unfold F2R; simpl.
unfold Zminus; rewrite bpow_plus.
change (bpow (-(1))) with (/2).
unfold Rdiv; ring.
split;[assumption|idtac].
assert (prec + emin < prec +e)%Z;[idtac|omega].
easy.
cut (prec + emin < prec +e)%Z.
simpl ; omega.
apply lt_bpow with radix2.
apply Rle_lt_trans with (1:=H).
rewrite H1; unfold F2R; simpl.
......@@ -89,14 +102,13 @@ rewrite Rabs_mult; rewrite (Rabs_right (bpow e)).
rewrite bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
rewrite <- Z2R_abs.
rewrite <- Z2R_Zpower.
now apply Z2R_lt.
unfold Prec_gt_0 in prec_gt_0_; omega.
rewrite <- abs_IZR.
rewrite <- IZR_Zpower.
now apply IZR_lt.
now apply Zlt_le_weak.
Qed.
Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z ->
Lemma FLT_round_half: forall z, bpow (prec+emin) <= Rabs z ->
round_flt (z/2)= round_flt z /2.
Proof with auto with typeclass_instances.
intros z Hz.
......@@ -109,18 +121,17 @@ intros K; contradict Hz.
rewrite K, Rabs_R0; apply Rlt_not_le.
apply bpow_gt_0.
assert (cexp (z/2) = cexp z -1)%Z.
assert (prec+emin < ln_beta radix2 z)%Z.
assert (prec+emin < mag radix2 z)%Z.
apply lt_bpow with radix2.
destruct ln_beta as (e,He); simpl.
destruct mag as (e,He); simpl.
apply Rle_lt_trans with (1:=Hz).
now apply He.
unfold canonic_exp, FLT_exp.
replace ((ln_beta radix2 (z/2))-prec)%Z with ((ln_beta radix2 z -1) -prec)%Z.
rewrite Z.max_l; try omega.
rewrite Z.max_l; try omega.
unfold cexp, FLT_exp.
replace ((mag radix2 (z/2))-prec)%Z with ((mag radix2 z -1) -prec)%Z.
rewrite Z.max_l; lia.
apply Zplus_eq_compat; try reflexivity.
apply sym_eq, ln_beta_unique.
destruct (ln_beta radix2 z) as (e,He); simpl.
apply sym_eq, mag_unique.
destruct (mag radix2 z) as (e,He); simpl.
unfold Rdiv; rewrite Rabs_mult.
rewrite (Rabs_right (/2)).
split.
......@@ -155,17 +166,15 @@ change (bpow (-(1))) with (/2).
field.
Qed.
Lemma FLT_ulp_le_id: forall u, bpow emin <= u -> ulp_flt u <= u.
Proof with auto with typeclass_instances.
intros u H.
rewrite ulp_neq_0.
2: apply Rgt_not_eq, Rlt_le_trans with (2:=H), bpow_gt_0.
case (Rle_or_lt (bpow (emin+prec-1)) u); intros Hu.
unfold ulp; rewrite canonic_exp_FLT_FLX.
unfold canonic_exp, FLX_exp.
destruct (ln_beta radix2 u) as (e,He); simpl.
unfold ulp; rewrite cexp_FLT_FLX.
unfold cexp, FLX_exp.
destruct (mag radix2 u) as (e,He); simpl.
apply Rle_trans with (bpow (e-1)).
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -178,7 +187,7 @@ apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0.
rewrite Rabs_right.
assumption.
apply Rle_ge, Rle_trans with (2:=Hu), bpow_ge_0.
unfold ulp; rewrite canonic_exp_FLT_FIX.
unfold ulp; rewrite cexp_FLT_FIX.
apply H.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_le_trans with (2:=H).
......@@ -207,11 +216,11 @@ rewrite <- bpow_plus.
apply bpow_le.
case (Rle_or_lt (bpow (emin+prec-1)) (Rabs u)); intros Hu.
(* *)
rewrite canonic_exp_FLT_FLX.
rewrite canonic_exp_FLT_FLX; trivial.
unfold canonic_exp, FLX_exp.
rewrite cexp_FLT_FLX.
rewrite cexp_FLT_FLX; trivial.
unfold cexp, FLX_exp.
change 2 with (bpow 1).
rewrite Rmult_comm, ln_beta_mult_bpow.
rewrite Rmult_comm, mag_mult_bpow.
omega.
intros H; contradict Hu.
apply Rlt_not_le; rewrite H, Rabs_R0.
......@@ -221,19 +230,18 @@ rewrite Rabs_mult.
pattern (Rabs u) at 1; rewrite <- (Rmult_1_l (Rabs u)).
apply Rmult_le_compat_r.
apply Rabs_pos.
change 2 with (Z2R 2).
rewrite <- (Z2R_abs 2).
now apply (Z2R_le 1 2).
rewrite <- (abs_IZR 2).
now apply IZR_le.
(* *)
rewrite canonic_exp_FLT_FIX.
rewrite canonic_exp_FLT_FIX; trivial.
unfold FIX_exp, canonic_exp; omega.
rewrite cexp_FLT_FIX.
rewrite cexp_FLT_FIX; trivial.
unfold FIX_exp, cexp; omega.
apply Rlt_le_trans with (1:=Hu).
apply bpow_le; omega.
lra.
rewrite Rabs_mult.
rewrite Rabs_pos_eq.
2: now apply (Z2R_le 0 2).
2: now apply IZR_le.
apply Rlt_le_trans with (2*bpow (emin + prec - 1)).
apply Rmult_lt_compat_l with (1 := Rlt_0_2).
assumption.
......@@ -243,7 +251,7 @@ apply bpow_le; omega.
Qed.
Lemma round_plus_small_id_aux: forall f h, format f -> (bpow (prec+emin) <= f) -> 0 < f
Lemma round_plus_small_id_aux: forall f h, format f -> (bpow (prec+emin) <= f) -> 0 < f
-> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
Proof with auto with typeclass_instances.
intros f h Ff H1 H2 Hh.
......@@ -262,7 +270,7 @@ rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
fourier.
lra.
rewrite <- (round_UP_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=h); try assumption.
apply round_UP_pt...
now left.
......@@ -271,7 +279,7 @@ apply Rle_trans with (1:=Hh).
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
apply Rplus_lt_reg_l with (-f); ring_simplify.
apply Rlt_le_trans with (/2*ulp_flt f).
2: right; field.
......@@ -279,7 +287,7 @@ apply Rle_lt_trans with (1:=Hh).
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
fourier.
lra.
(* h = 0 *)
rewrite <- H, Rplus_0_r.
apply round_generic...
......@@ -289,55 +297,55 @@ rewrite Rabs_left in Hh; try assumption.
assert (0 < pred_flt f).
apply Rlt_le_trans with (bpow emin).
apply bpow_gt_0.
apply le_pred_lt...
apply pred_ge_gt...
apply FLT_format_bpow...
omega.
apply Rlt_le_trans with (2:=H1).
apply bpow_lt.
unfold Prec_gt_0 in prec_gt_0_; omega.
assert (M:(prec + emin +1 <= ln_beta radix2 f)%Z).
apply ln_beta_ge_bpow.
assert (M:(prec + emin +1 <= mag radix2 f)%Z).
apply mag_ge_bpow.
replace (prec+emin+1-1)%Z with (prec+emin)%Z by ring.
rewrite Rabs_right; try assumption.
apply Rle_ge; now left.
assert (T1:(ulp_flt (pred_flt f) = ulp_flt f)
\/ ( ulp_flt (pred_flt f) = /2* ulp_flt f
/\ f = bpow (ln_beta radix2 f -1))).
assert (T1:(ulp_flt (pred_flt f) = ulp_flt f)
\/ ( ulp_flt (pred_flt f) = /2* ulp_flt f
/\ f = bpow (mag radix2 f -1))).
generalize H; rewrite pred_eq_pos; [idtac|now left].
unfold pred_pos; case Req_bool_spec; intros K HH.
(**)
right; split; try assumption.
rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
apply trans_eq with (bpow (ln_beta radix2 f- prec -1)).
apply trans_eq with (bpow (mag radix2 f- prec -1)).
apply f_equal.
unfold canonic_exp.
apply trans_eq with (FLT_exp emin prec (ln_beta radix2 f -1)%Z).
unfold cexp.
apply trans_eq with (FLT_exp emin prec (mag radix2 f -1)%Z).
apply f_equal.
unfold FLT_exp.
rewrite Z.max_l.
2: omega.
apply ln_beta_unique.
apply mag_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f -1-prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f -1-prec)).
ring_simplify.
apply Rle_trans with (bpow (ln_beta radix2 f - 1 - 1) + bpow (ln_beta radix2 f - 1 - 1)).
apply Rle_trans with (bpow (mag radix2 f - 1 - 1) + bpow (mag radix2 f - 1 - 1)).
apply Rplus_le_compat_r.
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
apply Rle_trans with (bpow 1*bpow (ln_beta radix2 f - 1 - 1)).
apply Rle_trans with (bpow 1*bpow (mag radix2 f - 1 - 1)).
change (bpow 1) with 2.
right; ring.
rewrite <- bpow_plus.
apply Rle_trans with (bpow (ln_beta radix2 f -1)).
apply Rle_trans with (bpow (mag radix2 f -1)).
apply bpow_le; omega.
rewrite <- K; now right.
rewrite <- K.
apply Rplus_lt_reg_l with (-f+bpow (ln_beta radix2 f-1-prec)); ring_simplify.
apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f-1-prec)); ring_simplify.
apply bpow_gt_0.
apply Rle_ge.
rewrite K at 1.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f - 1 - prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f - 1 - prec)).
ring_simplify.
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -347,12 +355,12 @@ replace (/2) with (bpow (-1)) by reflexivity.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
rewrite <- bpow_plus.
apply f_equal.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite Z.max_l;[ring|omega].
(**)
left.
assert (bpow (ln_beta radix2 f -1) < f).
destruct (ln_beta radix2 f); simpl in *.
assert (bpow (mag radix2 f -1) < f).
destruct (mag radix2 f); simpl in *.
destruct a.
now apply Rgt_not_eq.
rewrite Rabs_right in H0.
......@@ -360,7 +368,7 @@ destruct H0; try assumption.
contradict H0.
now apply sym_not_eq.
apply Rle_ge; now left.
assert (bpow (ln_beta radix2 f -1) + ulp_flt (bpow (ln_beta radix2 f-1)) <= f).
assert (bpow (mag radix2 f -1) + ulp_flt (bpow (mag radix2 f-1)) <= f).
rewrite <- succ_eq_pos;[idtac|apply bpow_ge_0].
apply succ_le_lt...
apply FLT_format_bpow...
......@@ -369,39 +377,39 @@ rewrite ulp_bpow in H4.
unfold FLT_exp in H4.
rewrite Z.max_l in H4.
2: omega.
replace (ln_beta radix2 f - 1 + 1 - prec)%Z with (ln_beta radix2 f - prec)%Z in H4 by ring.
replace (mag radix2 f - 1 + 1 - prec)%Z with (mag radix2 f - prec)%Z in H4 by ring.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
rewrite ulp_neq_0 at 2; try now apply Rgt_not_eq.
unfold canonic_exp.
unfold cexp.
apply f_equal; apply f_equal.
replace (ulp_flt f) with (bpow (ln_beta radix2 f -prec)).
apply ln_beta_unique.
replace (ulp_flt f) with (bpow (mag radix2 f -prec)).
apply mag_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f -prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f -prec)).
ring_simplify.
apply Rle_trans with (2:=H4); right; ring.
apply Rlt_trans with f.
apply Rplus_lt_reg_l with (-f+bpow (ln_beta radix2 f - prec)).
apply Rplus_lt_reg_l with (-f+bpow (mag radix2 f - prec)).
ring_simplify.
apply bpow_gt_0.
apply Rle_lt_trans with (1:=RRle_abs _).
apply bpow_ln_beta_gt.
apply bpow_mag_gt.
apply Rle_ge.
apply Rplus_le_reg_l with (bpow (ln_beta radix2 f - prec)).
apply Rplus_le_reg_l with (bpow (mag radix2 f - prec)).
ring_simplify.
left; apply Rle_lt_trans with (2:=H0).
apply bpow_le.
unfold Prec_gt_0 in prec_gt_0_;omega.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
unfold canonic_exp, FLT_exp.
unfold cexp, FLT_exp.
rewrite Z.max_l.
reflexivity.
omega.
assert (T: (ulp_flt (pred_flt f) = ulp_flt f \/
assert (T: (ulp_flt (pred_flt f) = ulp_flt f \/
(ulp_flt (pred_flt f) = / 2 * ulp_flt f /\ - h < / 4 * ulp_flt f))
\/ (ulp_flt (pred_flt f) = / 2 * ulp_flt f /\
f = bpow (ln_beta radix2 f - 1) /\
f = bpow (mag radix2 f - 1) /\
- h = / 4 * ulp_flt f) ).
destruct T1.
left; now left.
......@@ -424,13 +432,13 @@ apply Rle_trans with (1:=Hh).
apply Rle_trans with (/2*ulp_flt f).
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
case H0.
intros Y; rewrite Y.
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
intros Y; rewrite (proj1 Y); now right.
replace (f+h) with (pred_flt f + (f-pred_flt f+h)) by ring.
pattern f at 4; rewrite <- (round_UP_pred_plus_eps_pos radix2 (FLT_exp emin prec) f) with (eps:=(f - pred_flt f + h)); try assumption.
......@@ -444,12 +452,12 @@ rewrite Y.
rewrite <- (Rmult_1_l (ulp_flt f)) at 2.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0;[apply bpow_gt_0|now apply Rgt_not_eq].
fourier.
lra.
apply Rlt_le_trans with (1:=Y2).
rewrite Y1.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
apply Rplus_le_reg_l with (-ulp_flt (pred_flt f)); ring_simplify.
now left.
rewrite pred_eq_pos; try now left.
......@@ -470,13 +478,13 @@ apply Rle_lt_trans with (1:=Hh).
rewrite Y.
apply Rmult_lt_compat_r.
rewrite ulp_neq_0; try apply bpow_gt_0; now apply Rgt_not_eq.
fourier.
lra.
apply Rlt_le_trans with (1:=Y2).
rewrite Y1.
right; field.
(* complex case: even choosing *)
elim H0; intros T1 (T2,T3); clear H0.
assert (pred_flt f = bpow (ln_beta radix2 f - 1) - bpow (ln_beta radix2 f - 1 -prec)).
assert (pred_flt f = bpow (mag radix2 f - 1) - bpow (mag radix2 f - 1 -prec)).
rewrite pred_eq_pos; try now left.
unfold pred_pos; case Req_bool_spec.
intros _; rewrite <- T2.
......@@ -494,22 +502,22 @@ auto with real.
rewrite T3, T1.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
assert (round radix2 (FLT_exp emin prec) Zceil (f+h) = f).
replace (f+h) with (pred_flt f + /2*ulp_flt (pred_flt f)).
apply round_UP_pred_plus_eps_pos...
split.
apply Rmult_lt_0_compat.
fourier.
lra.
rewrite ulp_neq_0; try now apply Rgt_not_eq.
apply bpow_gt_0.
rewrite <- (Rmult_1_l (ulp_flt (pred_flt f))) at 2.
apply Rmult_le_compat_r.
apply ulp_ge_0.
fourier.
lra.
rewrite T1, H0, <- T2.
replace h with (--h) by ring; rewrite T3.
replace (bpow (ln_beta radix2 f - 1 - prec)) with (/2*ulp_flt f).
replace (bpow (mag radix2 f - 1 - prec)) with (/2*ulp_flt f).
field.
replace (/2) with (bpow (-1)) by reflexivity.
rewrite T2 at 1.
......@@ -518,15 +526,15 @@ apply f_equal; unfold FLT_exp.
rewrite Z.max_l.
ring.
omega.
assert ((Zeven (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))) = false).
assert ((Z.even (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))) = false).
replace (Zfloor (scaled_mantissa radix2 (FLT_exp emin prec) (f + h)))
with (Zpower radix2 prec -1)%Z.
unfold Zminus; rewrite Zeven_plus.
rewrite Zeven_opp.
rewrite Zeven_Zpower.
unfold Zminus; rewrite Z.even_add.
rewrite Z.even_opp.
rewrite Z.even_pow.
reflexivity.
unfold Prec_gt_0 in prec_gt_0_; omega.
apply eq_Z2R.
apply eq_IZR.
rewrite <- scaled_mantissa_DN...
2: rewrite H4; assumption.
rewrite H4.
......@@ -535,11 +543,11 @@ rewrite bpow_opp.
rewrite <- ulp_neq_0; try now apply Rgt_not_eq.
rewrite T1.
rewrite Rinv_mult_distr.
2: apply Rgt_not_eq; fourier.
2: apply Rgt_not_eq; lra.
2: apply Rgt_not_eq; rewrite ulp_neq_0; try apply bpow_gt_0.
2: now apply Rgt_not_eq.
rewrite Rinv_involutive.
2: apply Rgt_not_eq; fourier.
2: apply Rgt_not_eq; lra.
rewrite T2 at 2.
rewrite ulp_bpow.
rewrite <- bpow_opp.
......@@ -550,9 +558,9 @@ replace 2 with (bpow 1) by reflexivity.
rewrite <- bpow_plus.
rewrite H0.
rewrite Rmult_minus_distr_r, <- 2!bpow_plus.
rewrite Z2R_minus.
rewrite minus_IZR.
apply f_equal2.
rewrite Z2R_Zpower.
rewrite IZR_Zpower.
apply f_equal.
ring.
unfold Prec_gt_0 in prec_gt_0_; omega.
......@@ -574,7 +582,7 @@ rewrite T3.
field.
Qed.
Lemma round_plus_small_id: forall f h, format f -> (bpow (prec+emin) <= Rabs f)
Lemma round_plus_small_id: forall f h, format f -> (bpow (prec+emin) <= Rabs f)
-> Rabs h <= /4* ulp_flt f -> round_flt (f+h) = f.
intros f h Ff H1 H2.
case (Rle_or_lt 0 f); intros V.
......@@ -598,21 +606,21 @@ Qed.
Definition average1 (x y : R) :=round_flt(round_flt(x+y)/2).
Definition avg_naive (x y : R) :=round_flt(round_flt(x+y)/2).
Variables x y:R.
Hypothesis Fx: format x.
Hypothesis Fy: format y.
Let a:=(x+y)/2.
Let av:=average1 x y.
Let av:=avg_naive x y.
Lemma average1_correct: av = round_flt a.
Lemma avg_naive_correct: av = round_flt a.
Proof with auto with typeclass_instances.
case (Rle_or_lt (bpow (prec + emin)) (Rabs (x+y))).
(* normal case: division by 2 is exact *)
intros H.
unfold av,a,average1.
unfold av,a,avg_naive.
rewrite round_generic...
now apply sym_eq, FLT_round_half.
apply FLT_format_half.
......@@ -622,7 +630,7 @@ apply FLT_format_bpow...
unfold Prec_gt_0 in prec_gt_0_; omega.
(* subnormal case: addition is exact, but division by 2 is not *)
intros H.
unfold av, average1.
unfold av, avg_naive.
replace (round_flt (x + y)) with (x+y).
reflexivity.
apply sym_eq, round_generic...
......@@ -632,40 +640,40 @@ Qed.
Lemma average1_symmetry: forall u v, average1 u v = average1 v u.
Lemma avg_naive_symmetry: forall u v, avg_naive u v = avg_naive v u.
Proof.
intros u v; unfold average1.
intros u v; unfold avg_naive.
rewrite Rplus_comm; reflexivity.
Qed.
Lemma average1_symmetry_Ropp: forall u v, average1 (-u) (-v) = - average1 u v.
Lemma avg_naive_symmetry_Ropp: forall u v, avg_naive (-u) (-v) = - avg_naive u v.
Proof.
intros u v; unfold average1.
intros u v; unfold avg_naive.
replace (-u+-v) with (-(u+v)) by ring.
rewrite round_NE_opp.
replace (- round_flt (u + v) / 2) with (- (round_flt (u + v) / 2)) by (unfold Rdiv; ring).
now rewrite round_NE_opp.
Qed.
Lemma average1_same_sign_1: 0 <= a -> 0 <= av.
Lemma avg_naive_same_sign_1: 0 <= a -> 0 <= av.
Proof with auto with typeclass_instances.
intros H.
rewrite average1_correct.
rewrite avg_naive_correct.
apply round_ge_generic...
apply generic_format_0.
Qed.
Lemma average1_same_sign_2: a <= 0-> av <= 0.
Lemma avg_naive_same_sign_2: a <= 0-> av <= 0.
Proof with auto with typeclass_instances.
intros H.
rewrite average1_correct.
rewrite avg_naive_correct.
apply round_le_generic...
apply generic_format_0.
Qed.
Lemma average1_between: Rmin x y <= av <= Rmax x y.
Lemma avg_naive_between: Rmin x y <= av <= Rmax x y.
Proof with auto with typeclass_instances.
rewrite average1_correct.
rewrite avg_naive_correct.
split.
apply round_ge_generic...
now apply P_Rmin.
......@@ -687,15 +695,15 @@ apply Rmax_r.
Qed.
Lemma average1_zero: a = 0 -> av = 0.
Lemma avg_naive_zero: a = 0 -> av = 0.
Proof with auto with typeclass_instances.
intros H1; rewrite average1_correct, H1.
intros H1; rewrite avg_naive_correct, H1.
rewrite round_0...
Qed.
Lemma average1_no_underflow: (bpow emin) <= Rabs a -> av <> 0.
Lemma avg_naive_no_underflow: (bpow emin) <= Rabs a -> av <> 0.
Proof with auto with typeclass_instances.
intros H.
(* *)
......@@ -706,22 +714,22 @@ contradict H1.
apply Rlt_not_le.
apply bpow_gt_0.
(* *)
rewrite average1_correct.
rewrite avg_naive_correct.
apply abs_round_ge_generic...
apply FLT_format_bpow...
omega.
Qed.
Lemma average1_correct_weak1: Rabs (av -a) <= /2*ulp_flt a.
Lemma avg_naive_correct_weak1: Rabs (av -a) <= /2*ulp_flt a.
Proof with auto with typeclass_instances.
rewrite average1_correct.
rewrite avg_naive_correct.
apply error_le_half_ulp...
Qed.
Lemma average1_correct_weak2: Rabs (av -a) <= 3/2*ulp_flt a.
Lemma avg_naive_correct_weak2: Rabs (av -a) <= 3/2*ulp_flt a.
Proof with auto with typeclass_instances.
apply Rle_trans with (1:=average1_correct_weak1).
apply Rle_trans with (1:=avg_naive_correct_weak1).
apply Rmult_le_compat_r.
unfold ulp; apply ulp_ge_0.
lra.
......@@ -736,17 +744,17 @@ Qed.
Definition average2 (x y : R) :=round_flt(round_flt(x/2) + round_flt(y/2)).