aboutsummaryrefslogtreecommitdiffstats
path: root/flocq/Prop/Fprop_div_sqrt_error.v
diff options
context:
space:
mode:
authorGuillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-22 15:41:50 +0200
committerGuillaume Melquiond <guillaume.melquiond@inria.fr>2015-09-22 15:41:50 +0200
commit0af966a42eb60e9af43f9a450d924758a83946c6 (patch)
tree2bef73e80a8a80da1c47deee66dc825feac45bdd /flocq/Prop/Fprop_div_sqrt_error.v
parentc212ab7a8adea516db72f17d818393629dbde1b3 (diff)
downloadcompcert-kvx-0af966a42eb60e9af43f9a450d924758a83946c6.tar.gz
compcert-kvx-0af966a42eb60e9af43f9a450d924758a83946c6.zip
Upgrade to Flocq 2.5.0.
Note: this version of Flocq is compatible with both Coq 8.4 and 8.5.
Diffstat (limited to 'flocq/Prop/Fprop_div_sqrt_error.v')
-rw-r--r--flocq/Prop/Fprop_div_sqrt_error.v16
1 files changed, 9 insertions, 7 deletions
diff --git a/flocq/Prop/Fprop_div_sqrt_error.v b/flocq/Prop/Fprop_div_sqrt_error.v
index ec00ca4e..9d29001d 100644
--- a/flocq/Prop/Fprop_div_sqrt_error.v
+++ b/flocq/Prop/Fprop_div_sqrt_error.v
@@ -95,9 +95,6 @@ intros e; apply Zle_refl.
now rewrite F2R_opp, F2R_mult, <- Hr1, <- Hy1.
(* *)
destruct (relative_error_FLX_ex beta prec (prec_gt_0 prec) rnd (x / y)%R) as (eps,(Heps1,Heps2)).
-apply Rmult_integral_contrapositive_currified.
-exact Zx.
-now apply Rinv_neq_0_compat.
rewrite Heps2.
rewrite <- Rabs_Ropp.
replace (-(x + - (x / y * (1 + eps) * y)))%R with (x * eps)%R by now field.
@@ -135,8 +132,11 @@ now apply Rabs_pos_lt.
rewrite Rabs_Ropp.
replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
rewrite <- Hr1.
-apply ulp_error_f...
-unfold ulp; apply f_equal.
+apply error_lt_ulp_round...
+apply Rmult_integral_contrapositive_currified; try apply Rinv_neq_0_compat; assumption.
+rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
now rewrite Hr2, <- Hr1.
replace (prec+(Fexp fr+Fexp fy))%Z with ((prec+Fexp fy)+Fexp fr)%Z by ring.
rewrite bpow_plus.
@@ -246,8 +246,10 @@ apply Rmult_le_compat_r.
apply Rabs_pos.
apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R.
rewrite <- Hr1.
-apply ulp_half_error_f...
-right; unfold ulp; apply f_equal.
+apply error_le_half_ulp_round...
+right; rewrite ulp_neq_0.
+2: now rewrite <- Hr1.
+apply f_equal.
rewrite Hr2, <- Hr1; trivial.
rewrite Rmult_assoc, Rmult_comm.
replace (prec+(Fexp fr+Fexp fr))%Z with (Fexp fr + (prec+Fexp fr))%Z by ring.