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
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
47
exists 0%R.
48 49 50
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
destruct (Req_dec x 0) as [Hx0|Hx0].
(* *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
74
exists 0%R.
75 76 77
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
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. }
Guillaume Melquiond's avatar
Guillaume Melquiond committed
653
  exists 0%R; exists 0%R; rewrite Zx; split; [|split; [|split]].
654 655 656 657 658 659 660
  { 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.