Version 3.0.0: - stripped prefix from all the file names, renamed some files . Definitions -> Defs . Appli -> IEEE754 - 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) - renamed theorem 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.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