Commit 6aad9951 by Guillaume Melquiond

Merge branch 'renaming'

parents e46760a7 117ae867
......@@ -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
......
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.4)
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.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
- 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
This diff is collapsed. Click to expand it.
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://flocg.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 "{}" \;
......@@ -81,6 +87,37 @@ html/index.html: $(OBJS)
@COQDOC@ -toc -interpolate -utf8 -html -g -R src Flocq -d html \
--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 > deps.map
doc: html/index.html
......@@ -88,16 +125,14 @@ 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
( 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@
......
AC_INIT([Flocq], [2.6.1],
AC_INIT([Flocq], [3.0.0],
[Sylvie Boldo <sylvie.boldo@inria.fr>, Guillaume Melquiond <guillaume.melquiond@inria.fr>],
[flocq])
......@@ -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 Flocq.Core.Fcore.
(**
This example is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2014-2018 Guillaume Melquiond
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 Flocq.Core.Core.
Require Import Gappa.Gappa_tactic Interval.Interval_tactic.
Open Scope R_scope.
......@@ -74,7 +91,7 @@ Lemma method_error :
Rabs ((f - exp t) / exp t) <= 23 * pow2 (-62).
Proof.
intros t t2 p q f Ht.
unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ; simpl ;
unfold f, q, p, t2, p0, p1, p2, q0, q1, q2 ;
interval with (i_bisect_taylor t 9, i_prec 70).
Qed.
......@@ -103,11 +120,11 @@ assert (Rabs x <= 5/16 \/ 5/16 <= Rabs x <= 746) as [Bx'|Bx'] by gappa.
rewrite 2!round_generic with (2 := Fx)...
gappa.
- assert (Hl: - 1 * pow2 (-102) <= Log2l - (ln 2 - Log2h) <= 0).
unfold Log2l, Log2h ; simpl bpow ;
unfold Log2l, Log2h ;
interval with (i_prec 110).
assert (Ax: x = x * InvLog2 * (1 / InvLog2)).
field.
unfold InvLog2 ; simpl ; interval.
unfold InvLog2 ; interval.
unfold te.
replace (x - k * ln 2) with (x - k * Log2h - k * (ln 2 - Log2h)) by ring.
revert Hl Ax.
......@@ -132,8 +149,8 @@ generalize (method_error t Bt).
intros Ef.
rewrite bpow_plus, Rmult_assoc.
assert (exp x = pow2 (Zfloor k) * exp (x - k * ln 2)) as ->.
assert (exists k', k = Z2R k') as [k' ->] by (eexists ; apply Rmult_1_r).
rewrite Zfloor_Z2R, bpow_exp, <- exp_plus.
assert (exists k', k = IZR k') as [k' ->] by (eexists ; apply Rmult_1_r).
rewrite Zfloor_IZR, bpow_exp, <- exp_plus.
apply f_equal.
simpl ; ring.
rewrite <- Rmult_minus_distr_l.
......@@ -152,9 +169,9 @@ assert (Rabs ((exp t - exp x) / exp x) <= 33 * pow2 (-60)).
rewrite <- exp_Ropp, <- exp_plus.
revert Ex.
unfold Rminus ; generalize (t + - x) ; clear.
simpl ; intros r Hr ; interval with (i_prec 60).
intros r Hr ; interval with (i_prec 60).
apply rel_helper. apply Rgt_not_eq, exp_pos.
apply rel_helper in H. 2: apply Rgt_not_eq, exp_pos.
apply rel_helper in Ef. 2: apply Rgt_not_eq, exp_pos.
unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; simpl bpow in * ; gappa.
unfold t2, add, mul, sub, div, p0, p1, p2, q0, q1, q2 in * ; gappa.
Qed.
Require Import Flocq.Core.Fcore.
Require Import Flocq.Calc.Fcalc_bracket Flocq.Calc.Fcalc_round Flocq.Calc.Fcalc_ops Flocq.Calc.Fcalc_div Flocq.Calc.Fcalc_sqrt.
(**
This example is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2015-2018 Sylvie Boldo
#<br />#
Copyright (C) 2015-2018 Guillaume Melquiond
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.
*)
From Flocq Require Import Core Bracket Round Operations Div Sqrt.
Section Compute.
......@@ -29,13 +47,13 @@ Proof.
intros m e.
case Zlt_bool_spec ; intros H.
apply Rlt_bool_true.
now apply F2R_lt_0_compat.
now apply F2R_lt_0.
apply Rlt_bool_false.
now apply F2R_ge_0_compat.
now apply F2R_ge_0.
Qed.
Definition plus (x y : float beta) :=
let (m, e) := Fplus beta x y in
let (m, e) := Fplus x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -47,7 +65,7 @@ Proof.
intros x y.
unfold plus.
rewrite <- F2R_plus.
destruct (Fplus beta x y) as [m e].
destruct (Fplus x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
......@@ -58,7 +76,7 @@ apply sym_eq, F2R_Zabs.
Qed.
Definition mult (x y : float beta) :=
let (m, e) := Fmult beta x y in
let (m, e) := Fmult x y in
let s := Zlt_bool m 0 in
let '(m', e', l) := truncate beta fexp (Zabs m, e, loc_Exact) in
Float beta (cond_Zopp s (choice s m' l)) e'.
......@@ -70,7 +88,7 @@ Proof.
intros x y.
unfold mult.
rewrite <- F2R_mult.
destruct (Fmult beta x y) as [m e].
destruct (Fmult x y) as [m e].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ (Zabs m) e loc_Exact).
3: now right.
destruct truncate as [[m' e'] l'].
......@@ -81,9 +99,8 @@ apply sym_eq, F2R_Zabs.
Qed.
Definition sqrt (x : float beta) :=
let (m, e) := x in
if Zlt_bool 0 m then
let '(m', e', l) := truncate beta fexp (Fsqrt_core beta prec m e) in
if Zlt_bool 0 (Fnum x) then
let '(m', e', l) := truncate beta fexp (Fsqrt fexp x) in
Float beta (choice false m' l) e'
else Float beta 0 0.
......@@ -91,20 +108,18 @@ Theorem sqrt_correct :
forall x : float beta,
round beta fexp rnd (R_sqrt.sqrt (F2R x)) = F2R (sqrt x).
Proof.
intros [m e].
intros x.
unfold sqrt.
case Zlt_bool_spec ; intros Hm.
generalize (Fsqrt_core_correct beta prec m e Hm).
destruct Fsqrt_core as [[m' e'] l].
generalize (Fsqrt_correct fexp x (F2R_gt_0 _ _ Hm)).
destruct Fsqrt as [[m' e'] l].
intros [Hs1 Hs2].
rewrite (round_trunc_sign_any_correct beta fexp rnd choice rnd_choice _ m' e' l).
rewrite (round_trunc_sign_any_correct' beta fexp rnd choice rnd_choice _ m' e' l).
destruct truncate as [[m'' e''] l'].
now rewrite Rlt_bool_false by apply sqrt_ge_0.
now rewrite Rabs_pos_eq by apply sqrt_ge_0.
left.
apply Zle_trans with (2 := fexp_prec _).
clear -Hs1 ; omega.
destruct (Req_dec (F2R (Float beta m e)) 0) as [Hz|Hz].
now left.
destruct (Req_dec (F2R x) 0) as [Hz|Hz].
rewrite Hz, sqrt_0, F2R_0.
now apply round_0.
unfold R_sqrt.sqrt.
......@@ -113,13 +128,13 @@ rewrite F2R_0.
now apply round_0.
destruct H as [H|H].
elim Rgt_not_le with (1 := H).
now apply F2R_le_0_compat.
now apply F2R_le_0.
now elim Hz.
Qed.
Lemma Rsgn_div :
forall x y : R,
x <> R0 -> y <> R0 ->
x <> 0%R -> y <> 0%R ->
Rlt_bool (x / y) 0 = xorb (Rlt_bool x 0) (Rlt_bool y 0).
Proof.
intros x y Hx0 Hy0.
......@@ -162,51 +177,54 @@ now elim Hy0.
Qed.
Definition div (x y : float beta) :=
let (mx, ex) := x in
let (my, ey) := y in
if Zeq_bool mx 0 then Float beta 0 0
if Zeq_bool (Fnum x) 0 then Float beta 0 0
else
let '(m, e, l) := truncate beta fexp (Fdiv_core beta prec (Zabs mx) ex (Zabs my) ey) in
let s := xorb (Zlt_bool mx 0) (Zlt_bool my 0) in
let '(m, e, l) := truncate beta fexp (Fdiv fexp (Fabs x) (Fabs y)) in
let s := xorb (Zlt_bool (Fnum x) 0) (Zlt_bool (Fnum y) 0) in
Float beta (cond_Zopp s (choice s m l)) e.
Theorem div_correct :
forall x y : float beta,
F2R y <> R0 ->
F2R y <> 0%R ->
round beta fexp rnd (F2R x / F2R y) = F2R (div x y).
Proof.
intros [mx ex] [my ey] Hy.
intros x y Hy.
unfold div.
case Zeq_bool_spec ; intros Hm.
rewrite Hm, 2!F2R_0.
unfold Rdiv.
rewrite Rmult_0_l.
now apply round_0.
assert (Hx: (0 < Zabs mx)%Z) by now apply Z.abs_pos.
assert (Hy': (0 < Zabs my)%Z).
apply Z.abs_pos.
destruct x as [mx ex].
simpl in Hm.
rewrite Hm, 2!F2R_0.
unfold Rdiv.
rewrite Rmult_0_l.
now apply round_0.
assert (0 < F2R (Fabs x))%R as Hx.
destruct x as [mx ex].
now apply F2R_gt_0, Z.abs_pos.
assert (0 < F2R (Fabs y))%R as Hy'.
destruct y as [my ey].
apply F2R_gt_0, Z.abs_pos.