Fprop_relative.v 20.6 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1
(**
2 3 4
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

5
Copyright (C) 2010-2013 Sylvie Boldo
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
#<br />#
7
Copyright (C) 2010-2013 Guillaume Melquiond
8 9 10 11 12 13 14 15 16 17 18 19

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.
*)

BOLDO Sylvie's avatar
BOLDO Sylvie committed
20
(** * Relative error of the roundings *)
21 22 23 24 25 26 27 28 29 30
Require Import Fcore.

Section Fprop_relative.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Section Fprop_relative_generic.

Variable fexp : Z -> Z.
31
Context { prop_exp : Valid_exp fexp }.
32

33 34 35 36 37
Section relative_error_conversion.

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
38
Lemma relative_error_lt_conversion :
39
  forall x b, (0 < b)%R ->
40
  (x <> 0 -> Rabs (round beta fexp rnd x - x) < b * Rabs x)%R ->
41
  exists eps,
42
  (Rabs eps < b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
43 44
Proof with auto with typeclass_instances.
intros x b Hb0 Hxb.
45 46 47 48 49 50
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
exists R0.
split.
now rewrite Rabs_R0.
rewrite Hx0, Rmult_0_l.
51
apply round_0...
52
(* *)
53
specialize (Hxb Hx0).
54
exists ((round beta fexp rnd x - x) / x)%R.
55 56 57 58 59 60 61 62 63 64
split. 2: now field.
unfold Rdiv.
rewrite Rabs_mult.
apply Rmult_lt_reg_r with (Rabs x).
now apply Rabs_pos_lt.
rewrite Rmult_assoc, <- Rabs_mult.
rewrite Rinv_l with (1 := Hx0).
now rewrite Rabs_R1, Rmult_1_r.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
65
Lemma relative_error_le_conversion :
66
  forall x b, (0 <= b)%R ->
67
  (Rabs (round beta fexp rnd x - x) <= b * Rabs x)%R ->
68
  exists eps,
69
  (Rabs eps <= b)%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
70 71
Proof with auto with typeclass_instances.
intros x b Hb0 Hxb.
72 73 74 75 76 77
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
exists R0.
split.
now rewrite Rabs_R0.
rewrite Hx0, Rmult_0_l.
78
apply round_0...
79
(* *)
80
exists ((round beta fexp rnd x - x) / x)%R.
81 82 83 84 85 86 87 88 89 90
split. 2: now field.
unfold Rdiv.
rewrite Rabs_mult.
apply Rmult_le_reg_r with (Rabs x).
now apply Rabs_pos_lt.
rewrite Rmult_assoc, <- Rabs_mult.
rewrite Rinv_l with (1 := Hx0).
now rewrite Rabs_R1, Rmult_1_r.
Qed.

91
End relative_error_conversion.
92

93 94 95
Variable emin p : Z.
Hypothesis Hmin : forall k, (emin < k)%Z -> (p <= k - fexp k)%Z.

96 97 98
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
99
Theorem relative_error :
100 101
  forall x,
  (bpow emin <= Rabs x)%R ->
102
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R.
103
Proof with auto with typeclass_instances.
104
intros x Hx.
105
assert (Hx': (x <> 0)%R).
106 107 108
intros T; contradict Hx; rewrite T, Rabs_R0.
apply Rlt_not_le, bpow_gt_0.
apply Rlt_le_trans with (ulp beta fexp x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
109
now apply error_lt_ulp...
110 111
rewrite ulp_neq_0; trivial.
unfold canonic_exp.
112 113
destruct (ln_beta beta x) as (ex, He).
simpl.
114
specialize (He Hx').
115
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
116
rewrite <- bpow_plus.
117
apply bpow_le.
118
assert (emin < ex)%Z.
119
apply (lt_bpow beta).
120
apply Rle_lt_trans with (2 := proj2 He).
121 122 123 124 125 126 127 128
exact Hx.
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
apply bpow_ge_0.
apply He.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
129
(** 1+#&epsilon;# property in any rounding *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
130
Theorem relative_error_ex :
131 132 133
  forall x,
  (bpow emin <= Rabs x)%R ->
  exists eps,
134
  (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
135
Proof with auto with typeclass_instances.
136
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
137
apply relative_error_lt_conversion...
138
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
139
intros _.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
140
now apply relative_error.
141 142
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
143
Theorem relative_error_F2R_emin :
144 145
  forall m, let x := F2R (Float beta m emin) in
  (x <> 0)%R ->
146
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs x)%R.
147
Proof.
148
intros m x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
149
apply relative_error.
150
unfold x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
151
rewrite <- F2R_Zabs.
152 153
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
154
rewrite F2R_0, F2R_Zabs.
155
now apply Rabs_pos_lt.
156 157
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
158
Theorem relative_error_F2R_emin_ex :
159 160
  forall m, let x := F2R (Float beta m emin) in
  exists eps,
161
  (Rabs eps < bpow (-p + 1))%R /\ round beta fexp rnd x = (x * (1 + eps))%R.
162
Proof with auto with typeclass_instances.
163
intros m x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
164
apply relative_error_lt_conversion...
165
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
166
now apply relative_error_F2R_emin.
167 168
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
169
Theorem relative_error_round :
170
  (0 < p)%Z ->
171 172
  forall x,
  (bpow emin <= Rabs x)%R ->
173
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R.
174
Proof with auto with typeclass_instances.
175
intros Hp x Hx.
176 177 178
assert (Hx': (x <> 0)%R).
intros T; contradict Hx; rewrite T, Rabs_R0.
apply Rlt_not_le, bpow_gt_0.
179
apply Rlt_le_trans with (ulp beta fexp x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
180
now apply error_lt_ulp.
181 182
rewrite ulp_neq_0; trivial.
unfold canonic_exp.
183 184 185 186
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He Hx').
assert (He': (emin < ex)%Z).
187
apply (lt_bpow beta).
188 189 190
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
191
rewrite <- bpow_plus.
192
apply bpow_le.
193 194 195 196
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
apply bpow_ge_0.
197
generalize He.
198 199
apply round_abs_abs...
clear rnd valid_rnd x Hx Hx' He.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
200
intros rnd valid_rnd x _ Hx.
201
rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
202
now apply round_le.
203 204 205 206 207 208
apply generic_format_bpow.
ring_simplify (ex - 1 + 1)%Z.
generalize (Hmin ex).
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
209
Theorem relative_error_round_F2R_emin :
210
  (0 < p)%Z ->
211 212
  forall m, let x := F2R (Float beta m emin) in
  (x <> 0)%R ->
213
  (Rabs (round beta fexp rnd x - x) < bpow (-p + 1) * Rabs (round beta fexp rnd x))%R.
214
Proof.
215
intros Hp m x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
216
apply relative_error_round.
217
exact Hp.
218
unfold x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
219
rewrite <- F2R_Zabs.
220 221
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
222
rewrite F2R_0, F2R_Zabs.
223
now apply Rabs_pos_lt.
224 225
Qed.

226
Variable choice : Z -> bool.
227

BOLDO Sylvie's avatar
BOLDO Sylvie committed
228
Theorem relative_error_N :
229 230
  forall x,
  (bpow emin <= Rabs x)%R ->
231
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R.
232
Proof.
233
intros x Hx.
234
apply Rle_trans with (/2 * ulp beta fexp x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
235
now apply error_le_half_ulp.
236 237 238 239 240 241 242 243 244 245
rewrite Rmult_assoc.
apply Rmult_le_compat_l.
apply Rlt_le.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
assert (Hx': (x <> 0)%R).
intros H.
apply Rlt_not_le with (2 := Hx).
rewrite H, Rabs_R0.
apply bpow_gt_0.
246 247
rewrite ulp_neq_0; trivial.
unfold canonic_exp.
248 249 250 251
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He Hx').
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
252
rewrite <- bpow_plus.
253
apply bpow_le.
254
assert (emin < ex)%Z.
255
apply (lt_bpow beta).
256 257 258 259 260 261 262 263 264
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
apply bpow_ge_0.
apply He.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
265
(** 1+#&epsilon;# property in rounding to nearest *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
266
Theorem relative_error_N_ex :
267 268 269
  forall x,
  (bpow emin <= Rabs x)%R ->
  exists eps,
270 271
  (Rabs eps <= /2 * bpow (-p + 1))%R /\ round beta fexp (Znearest choice) x = (x * (1 + eps))%R.
Proof with auto with typeclass_instances.
272
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
273
apply relative_error_le_conversion...
274 275 276 277 278
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
279
now apply relative_error_N.
280 281
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
282
Theorem relative_error_N_F2R_emin :
283
  forall m, let x := F2R (Float beta m emin) in
284 285
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs x)%R.
Proof with auto with typeclass_instances.
286
intros m x.
287 288
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
289
rewrite Hx, round_0...
290 291 292 293 294
unfold Rminus.
rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0.
rewrite Rmult_0_r.
apply Rle_refl.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
295
apply relative_error_N.
296
unfold x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
297
rewrite <- F2R_Zabs.
298 299
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
300
rewrite F2R_0, F2R_Zabs.
301 302 303
now apply Rabs_pos_lt.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
304
Theorem relative_error_N_F2R_emin_ex :
305 306
  forall m, let x := F2R (Float beta m emin) in
  exists eps,
307 308
  (Rabs eps <= /2 * bpow (-p + 1))%R /\ round beta fexp (Znearest choice) x = (x * (1 + eps))%R.
Proof with auto with typeclass_instances.
309
intros m x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
310
apply relative_error_le_conversion...
311 312 313 314 315
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
316
now apply relative_error_N_F2R_emin.
317 318
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
319
Theorem relative_error_N_round :
320
  (0 < p)%Z ->
321 322
  forall x,
  (bpow emin <= Rabs x)%R ->
323 324
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs (round beta fexp (Znearest choice) x))%R.
Proof with auto with typeclass_instances.
325
intros Hp x Hx.
326
apply Rle_trans with (/2 * ulp beta fexp x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
327
now apply error_le_half_ulp.
328 329 330 331 332
rewrite Rmult_assoc.
apply Rmult_le_compat_l.
apply Rlt_le.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
333 334 335 336 337
assert (Hx': (x <> 0)%R).
intros H.
apply Rlt_not_le with (2 := Hx).
rewrite H, Rabs_R0.
apply bpow_gt_0.
338 339
rewrite ulp_neq_0; trivial.
unfold canonic_exp.
340 341 342 343
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He Hx').
assert (He': (emin < ex)%Z).
344
apply (lt_bpow beta).
345 346
apply Rle_lt_trans with (2 := proj2 He).
exact Hx.
347
apply Rle_trans with (bpow (-p + 1) * bpow (ex - 1))%R.
348
rewrite <- bpow_plus.
349
apply bpow_le.
350 351 352 353 354
generalize (Hmin ex).
omega.
apply Rmult_le_compat_l.
apply bpow_ge_0.
generalize He.
355 356
apply round_abs_abs...
clear rnd valid_rnd x Hx Hx' He.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
357
intros rnd valid_rnd x _ Hx.
358
rewrite <- (round_generic beta fexp rnd (bpow (ex - 1))).
359
now apply round_le.
360 361 362 363 364 365
apply generic_format_bpow.
ring_simplify (ex - 1 + 1)%Z.
generalize (Hmin ex).
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
366
Theorem relative_error_N_round_F2R_emin :
367
  (0 < p)%Z ->
368
  forall m, let x := F2R (Float beta m emin) in
369 370
  (Rabs (round beta fexp (Znearest choice) x - x) <= /2 * bpow (-p + 1) * Rabs (round beta fexp (Znearest choice) x))%R.
Proof with auto with typeclass_instances.
371
intros Hp m x.
372 373
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
374
rewrite Hx, round_0...
375 376 377 378 379
unfold Rminus.
rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0.
rewrite Rmult_0_r.
apply Rle_refl.
(* . *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
380
apply relative_error_N_round with (1 := Hp).
381
unfold x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
382
rewrite <- F2R_Zabs.
383 384
apply bpow_le_F2R.
apply F2R_lt_reg with beta emin.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
385
rewrite F2R_0, F2R_Zabs.
386 387 388 389 390 391 392 393 394 395
now apply Rabs_pos_lt.
Qed.

End Fprop_relative_generic.

Section Fprop_relative_FLT.

Variable emin prec : Z.
Variable Hp : Zlt 0 prec.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
396 397 398 399 400 401 402 403 404
Lemma relative_error_FLT_aux :
  forall k, (emin + prec - 1 < k)%Z -> (prec <= k - FLT_exp emin prec k)%Z.
Proof.
intros k Hk.
unfold FLT_exp.
generalize (Zmax_spec (k - prec) emin).
omega.
Qed.

405 406
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
407

408
Theorem relative_error_FLT :
409 410
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
411
  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
412
Proof with auto with typeclass_instances.
413
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
414
apply relative_error with (emin + prec - 1)%Z...
Guillaume Melquiond's avatar
Guillaume Melquiond committed
415
apply relative_error_FLT_aux.
416 417
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
418
Theorem relative_error_FLT_F2R_emin :
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440
  forall m, let x := F2R (Float beta m emin) in
  (x <> 0)%R ->
  (Rabs (round beta (FLT_exp emin prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
Proof with auto with typeclass_instances.
intros m x Zx.
destruct (Rlt_or_le (Rabs x) (bpow (emin + prec - 1))) as [Hx|Hx].
rewrite round_generic...
unfold Rminus.
rewrite Rplus_opp_r, Rabs_R0.
apply Rmult_lt_0_compat.
apply bpow_gt_0.
now apply Rabs_pos_lt.
apply generic_format_FLT_FIX...
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx).
apply bpow_le.
apply Zle_pred.
apply generic_format_FIX.
now exists (Float beta m emin).
now apply relative_error_FLT.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
441
Theorem relative_error_FLT_F2R_emin_ex :
442
  forall m, let x := F2R (Float beta m emin) in
443
  exists eps,
444
  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
445
Proof with auto with typeclass_instances.
446
intros m x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
447
apply relative_error_lt_conversion...
448 449
apply bpow_gt_0.
now apply relative_error_FLT_F2R_emin.
450 451
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
452
(** 1+#&epsilon;# property in any rounding in FLT *)
453 454 455 456
Theorem relative_error_FLT_ex :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  exists eps,
457
  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) rnd x = (x * (1 + eps))%R.
458
Proof with auto with typeclass_instances.
459
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
460
apply relative_error_lt_conversion...
461
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
462
intros _; now apply relative_error_FLT.
463 464
Qed.

465
Variable choice : Z -> bool.
466

467 468 469
Theorem relative_error_N_FLT :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
470 471
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
Proof with auto with typeclass_instances.
472
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
473
apply relative_error_N with (emin + prec - 1)%Z...
Guillaume Melquiond's avatar
Guillaume Melquiond committed
474
apply relative_error_FLT_aux.
475 476
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
477
(** 1+#&epsilon;# property in rounding to nearest in FLT *)
478 479 480 481
Theorem relative_error_N_FLT_ex :
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  exists eps,
482 483
  (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
Proof with auto with typeclass_instances.
484
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
485
apply relative_error_le_conversion...
486 487 488 489 490 491 492 493
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply relative_error_N_FLT.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
494
Theorem relative_error_N_FLT_round :
495 496
  forall x,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
497 498
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
Proof with auto with typeclass_instances.
499
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
500
apply relative_error_N_round with (emin + prec - 1)%Z...
Guillaume Melquiond's avatar
Guillaume Melquiond committed
501
apply relative_error_FLT_aux.
502 503
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
504
Theorem relative_error_N_FLT_F2R_emin :
505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528
  forall m, let x := F2R (Float beta m emin) in
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
Proof with auto with typeclass_instances.
intros m x.
destruct (Rlt_or_le (Rabs x) (bpow (emin + prec - 1))) as [Hx|Hx].
rewrite round_generic...
unfold Rminus.
rewrite Rplus_opp_r, Rabs_R0.
apply Rmult_le_pos.
apply Rmult_le_pos.
apply Rlt_le.
apply (RinvN_pos 1).
apply bpow_ge_0.
apply Rabs_pos.
apply generic_format_FLT_FIX...
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx).
apply bpow_le.
apply Zle_pred.
apply generic_format_FIX.
now exists (Float beta m emin).
now apply relative_error_N_FLT.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
529
Theorem relative_error_N_FLT_F2R_emin_ex :
530 531 532 533 534 535 536 537 538 539
  forall m, let x := F2R (Float beta m emin) in
  exists eps,
  (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps))%R.
Proof with auto with typeclass_instances.
intros m x.
apply relative_error_le_conversion...
apply Rmult_le_pos.
apply Rlt_le.
apply (RinvN_pos 1).
apply bpow_ge_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
540
now apply relative_error_N_FLT_F2R_emin.
541 542
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
543 544

Theorem relative_error_N_FLT_round_F2R_emin :
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569
  forall m, let x := F2R (Float beta m emin) in
  (Rabs (round beta (FLT_exp emin prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLT_exp emin prec) (Znearest choice) x))%R.
Proof with auto with typeclass_instances.
intros m x.
destruct (Rlt_or_le (Rabs x) (bpow (emin + prec - 1))) as [Hx|Hx].
rewrite round_generic...
unfold Rminus.
rewrite Rplus_opp_r, Rabs_R0.
apply Rmult_le_pos.
apply Rmult_le_pos.
apply Rlt_le.
apply (RinvN_pos 1).
apply bpow_ge_0.
apply Rabs_pos.
apply generic_format_FLT_FIX...
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx).
apply bpow_le.
apply Zle_pred.
apply generic_format_FIX.
now exists (Float beta m emin).
apply relative_error_N_round with (emin := (emin + prec - 1)%Z)...
apply relative_error_FLT_aux.
Qed.

570
Lemma error_N_FLT_aux :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
571
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
572
  (0 < x)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
573
  exists eps, exists  eta,
574 575
  (Rabs eps <= /2 * bpow (-prec + 1))%R /\
  (Rabs eta <= /2 * bpow (emin))%R      /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
576
  (eps*eta=0)%R /\
577
  round beta (FLT_exp emin prec) (Znearest choice) x = (x * (1 + eps) + eta)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
578
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
579 580 581
intros x Hx2.
case (Rle_or_lt (bpow (emin+prec)) x); intros Hx.
(* *)
582
destruct relative_error_N_ex with (FLT_exp emin prec) (emin+prec)%Z prec choice x
BOLDO Sylvie's avatar
BOLDO Sylvie committed
583
  as (eps,(Heps1,Heps2)).
584
now apply FLT_exp_valid.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
585 586 587 588 589 590 591 592 593 594 595
intros; unfold FLT_exp.
rewrite Zmax_left; omega.
rewrite Rabs_right;[assumption|apply Rle_ge; now left].
exists eps; exists 0%R.
split;[assumption|split].
rewrite Rabs_R0; apply Rmult_le_pos.
auto with real.
apply bpow_ge_0.
split;[apply Rmult_0_r|idtac].
now rewrite Rplus_0_r.
(* *)
596
exists 0%R; exists (round beta (FLT_exp emin prec) (Znearest choice) x - x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
597 598 599 600 601 602
split.
rewrite Rabs_R0; apply Rmult_le_pos.
auto with real.
apply bpow_ge_0.
split.
apply Rle_trans with (/2*ulp beta (FLT_exp emin prec) x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
603
apply error_le_half_ulp.
604
now apply FLT_exp_valid.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
605
apply Rmult_le_compat_l; auto with real.
606 607
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
608
apply bpow_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
609
unfold FLT_exp, canonic_exp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
610 611 612 613
rewrite Zmax_right.
omega.
destruct (ln_beta beta x) as (e,He); simpl.
assert (e-1 < emin+prec)%Z.
614
apply (lt_bpow beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
615 616 617 618 619 620 621 622
apply Rle_lt_trans with (2:=Hx).
rewrite <- (Rabs_right x).
apply He; auto with real.
apply Rle_ge; now left.
omega.
split;ring.
Qed.

623 624
End Fprop_relative_FLT.

625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660
Lemma error_N_FLT :
  forall (emin prec : Z), (0 < prec)%Z ->
  forall (choice : Z -> bool),
  forall (x : R),
  exists eps eta : R,
  (Rabs eps <= /2 * bpow (-prec + 1))%R /\
  (Rabs eta <= /2 * bpow emin)%R /\
  (eps * eta = 0)%R /\
  (round beta (FLT_exp emin prec) (Znearest choice) x
   = x * (1 + eps) + eta)%R.
Proof.
intros emin prec Pprec choice x.
destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
{ assert (Pmx : (0 < - x)%R).
  { now rewrite <- Ropp_0; apply Ropp_lt_contravar. }
  destruct (error_N_FLT_aux emin prec Pprec
                            (fun t : Z => negb (choice (- (t + 1))%Z))
                            (- x)%R Pmx)
    as (d,(e,(Hd,(He,(Hde,Hr))))).
  exists d; exists (- e)%R; split; [exact Hd|split; [|split]].
  { now rewrite Rabs_Ropp. }
  { now rewrite Ropp_mult_distr_r_reverse, <- Ropp_0; apply f_equal. }
  rewrite <- (Ropp_involutive x), round_N_opp.
  now rewrite Ropp_mult_distr_l_reverse, <- Ropp_plus_distr; apply f_equal. }
{ assert (Ph2 : (0 <= / 2)%R).
  { apply (Rmult_le_reg_l 2 _ _ Rlt_0_2).
    rewrite Rmult_0_r, Rinv_r; [exact Rle_0_1|].
    apply Rgt_not_eq, Rlt_gt, Rlt_0_2. }
  exists R0; exists R0; rewrite Zx; split; [|split; [|split]].
  { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
  { now rewrite Rabs_R0; apply Rmult_le_pos; [|apply bpow_ge_0]. }
  { now rewrite Rmult_0_l. }
  now rewrite Rmult_0_l, Rplus_0_l, round_0; [|apply valid_rnd_N]. }
now apply error_N_FLT_aux.
Qed.

661 662 663 664 665
Section Fprop_relative_FLX.

Variable prec : Z.
Variable Hp : Zlt 0 prec.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
666 667 668 669 670 671 672 673
Lemma relative_error_FLX_aux :
  forall k, (prec <= k - FLX_exp prec k)%Z.
Proof.
intros k.
unfold FLX_exp.
omega.
Qed.

674 675
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
676

677
Theorem relative_error_FLX :
678 679
  forall x,
  (x <> 0)%R ->
680
  (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs x)%R.
681
Proof with auto with typeclass_instances.
682
intros x Hx.
683 684
destruct (ln_beta beta x) as (ex, He).
specialize (He Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
685
apply relative_error with (ex - 1)%Z...
686
intros k _.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
687
apply relative_error_FLX_aux.
688 689 690
apply He.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
691
(** 1+#&epsilon;# property in any rounding in FLX *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
692
Theorem relative_error_FLX_ex :
693 694
  forall x,
  exists eps,
695
  (Rabs eps < bpow (-prec + 1))%R /\ round beta (FLX_exp prec) rnd x = (x * (1 + eps))%R.
696
Proof with auto with typeclass_instances.
697
intros x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
698
apply relative_error_lt_conversion...
699 700 701 702
apply bpow_gt_0.
now apply relative_error_FLX.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
703
Theorem relative_error_FLX_round :
704 705
  forall x,
  (x <> 0)%R ->
706
  (Rabs (round beta (FLX_exp prec) rnd x - x) < bpow (-prec + 1) * Rabs (round beta (FLX_exp prec) rnd x))%R.
707
Proof with auto with typeclass_instances.
708
intros x Hx.
709 710
destruct (ln_beta beta x) as (ex, He).
specialize (He Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
711
apply relative_error_round with (ex - 1)%Z...
712
intros k _.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
713
apply relative_error_FLX_aux.
714 715 716
apply He.
Qed.

717
Variable choice : Z -> bool.
718

719
Theorem relative_error_N_FLX :
720
  forall x,
721 722
  (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs x)%R.
Proof with auto with typeclass_instances.
723 724 725
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
726
rewrite Hx, round_0...
727 728 729 730 731
unfold Rminus.
rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0.
rewrite Rmult_0_r.
apply Rle_refl.
(* . *)
732 733
destruct (ln_beta beta x) as (ex, He).
specialize (He Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
734
apply relative_error_N with (ex - 1)%Z...
735
intros k _.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
736
apply relative_error_FLX_aux.
737 738 739
apply He.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
740
(** 1+#&epsilon;# property in rounding to nearest in FLX *)
741 742 743
Theorem relative_error_N_FLX_ex :
  forall x,
  exists eps,
744 745
  (Rabs eps <= /2 * bpow (-prec + 1))%R /\ round beta (FLX_exp prec) (Znearest choice) x = (x * (1 + eps))%R.
Proof with auto with typeclass_instances.
746
intros x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
747
apply relative_error_le_conversion...
748 749 750 751 752 753 754 755
apply Rlt_le.
apply Rmult_lt_0_compat.
apply Rinv_0_lt_compat.
now apply (Z2R_lt 0 2).
apply bpow_gt_0.
now apply relative_error_N_FLX.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
756
Theorem relative_error_N_FLX_round :
757
  forall x,
758 759
  (Rabs (round beta (FLX_exp prec) (Znearest choice) x - x) <= /2 * bpow (-prec + 1) * Rabs (round beta (FLX_exp prec) (Znearest choice) x))%R.
Proof with auto with typeclass_instances.
760 761 762
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
763
rewrite Hx, round_0...
764 765 766 767 768
unfold Rminus.
rewrite Rplus_0_l, Rabs_Ropp, Rabs_R0.
rewrite Rmult_0_r.
apply Rle_refl.
(* . *)
769 770
destruct (ln_beta beta x) as (ex, He).
specialize (He Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
771
apply relative_error_N_round with (ex - 1)%Z.
772
now apply FLX_exp_valid.
773
intros k _.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
774
apply relative_error_FLX_aux.
775
exact Hp.
776 777 778 779 780 781
apply He.
Qed.

End Fprop_relative_FLX.

End Fprop_relative.