Fprop_plus_error.v 16.1 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.
*)

20 21 22 23 24 25
(** * Error of the rounded-to-nearest addition is representable. *)

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_generic_fmt.
26 27 28
Require Import Fcore_FIX.
Require Import Fcore_FLX.
Require Import Fcore_FLT.
29
Require Import Fcore_ulp.
30 31
Require Import Fcalc_ops.

32

33 34 35 36 37 38
Section Fprop_plus_error.

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

Variable fexp : Z -> Z.
39
Context { valid_exp : Valid_exp fexp }.
40

41 42 43 44 45
Section round_repr_same_exp.

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

46
Theorem round_repr_same_exp :
47
  forall m e,
48
  exists m',
49
  round beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e).
50 51
Proof with auto with typeclass_instances.
intros m e.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
52
set (e' := canonic_exp beta fexp (F2R (Float beta m e))).
53
unfold round, scaled_mantissa. fold e'.
54 55 56
destruct (Zle_or_lt e' e) as [He|He].
exists m.
unfold F2R at 2. simpl.
57
rewrite Rmult_assoc, <- bpow_plus.
58
rewrite <- Z2R_Zpower. 2: omega.
59
rewrite <- Z2R_mult, Zrnd_Z2R...
60
unfold F2R. simpl.
61
rewrite Z2R_mult.
62 63
rewrite Rmult_assoc.
rewrite Z2R_Zpower. 2: omega.
64
rewrite <- bpow_plus.
65 66
apply (f_equal (fun v => Z2R m * bpow v)%R).
ring.
67
exists ((rnd (Z2R m * bpow (e - e'))) * Zpower beta (e' - e))%Z.
68
unfold F2R. simpl.
69
rewrite Z2R_mult.
70 71
rewrite Z2R_Zpower. 2: omega.
rewrite 2!Rmult_assoc.
72
rewrite <- 2!bpow_plus.
73 74 75 76
apply (f_equal (fun v => _ * bpow v)%R).
ring.
Qed.

77 78
End round_repr_same_exp.

79
Context { monotone_exp : Monotone_exp fexp }.
80 81
Notation format := (generic_format beta fexp).

82
Variable choice : Z -> bool.
83

84
Lemma plus_error_aux :
85
  forall x y,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
86
  (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
87
  format x -> format y ->
88
  format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
89 90
Proof.
intros x y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
91 92
set (ex := canonic_exp beta fexp x).
set (ey := canonic_exp beta fexp y).
93
intros He Hx Hy.
94
destruct (Req_dec (round beta fexp (Znearest choice) (x + y) - (x + y)) R0) as [H0|H0].
95 96 97 98 99
rewrite H0.
apply generic_format_0.
set (mx := Ztrunc (scaled_mantissa beta fexp x)).
set (my := Ztrunc (scaled_mantissa beta fexp y)).
(* *)
100
assert (Hxy: (x + y)%R = F2R (Float beta (mx + my * beta ^ (ey - ex)) ex)).
101 102
rewrite Hx, Hy.
fold mx my ex ey.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
103
rewrite <- F2R_plus.
104 105 106 107
unfold Fplus. simpl.
now rewrite Zle_imp_le_bool with (1 := He).
(* *)
rewrite Hxy.
108
destruct (round_repr_same_exp (Znearest choice) (mx + my * beta ^ (ey - ex)) ex) as (mxy, Hxy').
109
rewrite Hxy'.
110 111
assert (H: (F2R (Float beta mxy ex) - F2R (Float beta (mx + my * beta ^ (ey - ex)) ex))%R =
  F2R (Float beta (mxy - (mx + my * beta ^ (ey - ex))) ex)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
112
now rewrite <- F2R_minus, Fminus_same_exp.
113
rewrite H.
114 115
apply generic_format_F2R.
intros _.
116 117
apply monotone_exp.
rewrite <- H, <- Hxy', <- Hxy.
118
apply ln_beta_le_abs.
119 120 121
exact H0.
pattern x at 3 ; replace x with (-(y - (x + y)))%R by ring.
rewrite Rabs_Ropp.
122
now apply (round_N_pt beta _ choice (x + y)).
123 124
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
125
(** Error of the addition *)
126 127 128
Theorem plus_error :
  forall x y,
  format x -> format y ->
129
  format (round beta fexp (Znearest choice) (x + y) - (x + y))%R.
130 131
Proof.
intros x y Hx Hy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
132
destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)).
133 134 135 136 137 138
now apply plus_error_aux.
rewrite Rplus_comm.
apply plus_error_aux ; try easy.
now apply Zlt_le_weak.
Qed.

139 140 141 142 143 144 145 146
End Fprop_plus_error.

Section Fprop_plus_zero.

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

Variable fexp : Z -> Z.
147
Context { valid_exp : Valid_exp fexp }.
148
Context { exp_not_FTZ : Exp_not_FTZ fexp }.
149 150
Notation format := (generic_format beta fexp).

151 152 153 154 155
Section round_plus_eq_zero_aux.

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

156
Lemma round_plus_eq_zero_aux :
157
  forall x y,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
158
  (canonic_exp beta fexp x <= canonic_exp beta fexp y)%Z ->
159 160
  format x -> format y ->
  (0 <= x + y)%R ->
161
  round beta fexp rnd (x + y) = R0 ->
162
  (x + y = 0)%R.
163 164
Proof with auto with typeclass_instances.
intros x y He Hx Hy Hp Hxy.
165 166 167 168 169 170 171 172
destruct (Req_dec (x + y) 0) as [H0|H0].
exact H0.
destruct (ln_beta beta (x + y)) as (exy, Hexy).
simpl.
specialize (Hexy H0).
destruct (Zle_or_lt exy (fexp exy)) as [He'|He'].
(* . *)
assert (H: (x + y)%R = F2R (Float beta (Ztrunc (x * bpow (- fexp exy)) +
173
  Ztrunc (y * bpow (- fexp exy))) (fexp exy))).
174 175
rewrite (subnormal_exponent beta fexp exy x He' Hx) at 1.
rewrite (subnormal_exponent beta fexp exy y He' Hy) at 1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
176
now rewrite <- F2R_plus, Fplus_same_exp.
177
rewrite H in Hxy.
178
rewrite round_generic in Hxy...
179
now rewrite <- H in Hxy.
180 181
apply generic_format_F2R.
intros _.
182
rewrite <- H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
183
unfold canonic_exp.
184 185 186
rewrite ln_beta_unique with (1 := Hexy).
apply Zle_refl.
(* . *)
187
elim Rle_not_lt with (1 := round_le beta _ rnd _ _ (proj1 Hexy)).
188 189
rewrite (Rabs_pos_eq _ Hp).
rewrite Hxy.
190
rewrite round_generic...
191 192
apply bpow_gt_0.
apply generic_format_bpow.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
193 194
apply Zlt_succ_le.
now rewrite (Zsucc_pred exy) in He'.
195 196
Qed.

197 198 199 200 201
End round_plus_eq_zero_aux.

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

BOLDO Sylvie's avatar
BOLDO Sylvie committed
202
(** rnd(x+y)=0 -> x+y = 0 provided this is not a FTZ format *)
203
Theorem round_plus_eq_zero :
204
  forall x y,
205
  format x -> format y ->
206
  round beta fexp rnd (x + y) = R0 ->
207
  (x + y = 0)%R.
208 209
Proof with auto with typeclass_instances.
intros x y Hx Hy.
210 211 212
destruct (Rle_or_lt R0 (x + y)) as [H1|H1].
(* . *)
revert H1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
213
destruct (Zle_or_lt (canonic_exp beta fexp x) (canonic_exp beta fexp y)) as [H2|H2].
214
now apply round_plus_eq_zero_aux.
215
rewrite Rplus_comm.
216
apply round_plus_eq_zero_aux ; try easy.
217 218 219 220 221
now apply Zlt_le_weak.
(* . *)
revert H1.
rewrite <- (Ropp_involutive (x + y)), Ropp_plus_distr, <- Ropp_0.
intros H1.
222
rewrite round_opp.
223 224
intros Hxy.
apply f_equal.
225
cut (round beta fexp (Zrnd_opp rnd) (- x + - y) = 0)%R.
226
cut (0 <= -x + -y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
227
destruct (Zle_or_lt (canonic_exp beta fexp (-x)) (canonic_exp beta fexp (-y))) as [H2|H2].
228
apply round_plus_eq_zero_aux ; try apply generic_format_opp...
229
rewrite Rplus_comm.
230
apply round_plus_eq_zero_aux ; try apply generic_format_opp...
231 232 233
now apply Zlt_le_weak.
apply Rlt_le.
now apply Ropp_lt_cancel.
234
rewrite <- (Ropp_involutive (round _ _ _ _)).
235 236 237 238 239
rewrite Hxy.
apply Ropp_involutive.
Qed.

End Fprop_plus_zero.
240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270

Section Fprop_plus_FLT.
Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.

Theorem FLT_format_plus_small: forall x y,
  generic_format beta (FLT_exp emin prec) x ->
  generic_format beta (FLT_exp emin prec) y ->
   (Rabs (x+y) <= bpow (prec+emin))%R ->
    generic_format beta (FLT_exp emin prec) (x+y).
Proof with auto with typeclass_instances.
intros x y Fx Fy H.
apply generic_format_FLT_FIX...
rewrite Zplus_comm; assumption.
apply generic_format_FIX_FLT, FIX_format_generic in Fx.
apply generic_format_FIX_FLT, FIX_format_generic in Fy.
destruct Fx as (nx,(H1x,H2x)).
destruct Fy as (ny,(H1y,H2y)).
apply generic_format_FIX.
exists (Float beta (Fnum nx+Fnum ny)%Z emin).
split;[idtac|reflexivity].
rewrite H1x,H1y; unfold F2R; simpl.
rewrite H2x, H2y.
rewrite Z2R_plus; ring.
Qed.

End Fprop_plus_FLT.
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286

Section Fprop_plus_multi.

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

Variable fexp : Z -> Z.
Context { valid_exp : Valid_exp fexp }.
Context { monotone_exp : Monotone_exp fexp }.
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.


Notation format := (generic_format beta fexp).
Notation cexp := (canonic_exp beta fexp).

287
Lemma ex_shift: forall x e, format x -> (e <= cexp x)%Z ->
288 289 290 291 292 293 294 295 296 297 298 299
  exists m, (x = Z2R m*bpow e)%R.
Proof with auto with typeclass_instances.
intros x e Fx He.
exists (Ztrunc (scaled_mantissa beta fexp x)*Zpower beta (cexp x -e))%Z.
rewrite Fx at 1; unfold F2R; simpl.
rewrite Z2R_mult, Rmult_assoc.
f_equal.
rewrite Z2R_Zpower.
2: omega.
rewrite <- bpow_plus; f_equal; ring.
Qed.

300 301
Lemma ln_beta_minus1: 
   forall z, (z<>0)%R -> (ln_beta beta z -1 = ln_beta beta (z / Z2R beta))%Z.
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
Proof with auto with typeclass_instances.
intros z Hz; apply sym_eq, ln_beta_unique.
destruct (ln_beta beta z) as (e,He); simpl.
replace (z / Z2R beta)%R with (z*bpow (-1))%R.
rewrite Rabs_mult, (Rabs_right (bpow _)); try split.
apply Rmult_le_reg_r with (bpow 1).
apply bpow_gt_0.
rewrite Rmult_assoc, <- 2!bpow_plus.
rewrite Rmult_1_r.
apply Rle_trans with (2:=proj1 (He Hz)).
apply bpow_le; omega.
apply Rmult_lt_reg_r with (bpow 1).
apply bpow_gt_0.
rewrite Rmult_assoc, <- 2!bpow_plus.
rewrite Rmult_1_r.
apply Rlt_le_trans with (1:=proj2 (He Hz)).
apply bpow_le; omega.
apply Rle_ge, bpow_ge_0.
simpl; unfold Rdiv; f_equal; f_equal; f_equal.
unfold Z.pow_pos; simpl; ring.
322 323 324 325 326 327 328 329
Qed.

Lemma rnd_plus_mutiple:
   forall x y, format x -> format y -> (x <> 0)%R ->
    exists m,
     (round beta fexp rnd (x+y) = Z2R m * ulp beta fexp (x/Z2R beta))%R.
Proof with auto with typeclass_instances.
intros x y Fx Fy Zx.
330 331
case (Zle_or_lt (ln_beta beta (x/Z2R beta)) (ln_beta beta y)); intros H1.
pose (e:=cexp (x / Z2R beta)).
332
destruct (ex_shift x e) as (nx, Hnx); try exact Fx.
333
apply monotone_exp.
334 335
rewrite <- (ln_beta_minus1 x Zx); omega.
destruct (ex_shift y e) as (ny, Hny); try assumption.
336 337 338 339 340 341 342 343 344 345 346 347 348
apply monotone_exp...
destruct (round_repr_same_exp beta fexp rnd (nx+ny) e) as (n,Hn).
exists n.
apply trans_eq with (F2R (Float beta n e)).
rewrite <- Hn; f_equal.
rewrite Hnx, Hny; unfold F2R; simpl; rewrite Z2R_plus; ring.
unfold F2R; simpl.
rewrite ulp_neq_0; try easy.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
(* *)
349
destruct (ex_shift (round beta fexp rnd (x + y)) (cexp (x/Z2R beta))) as (n,Hn).
350 351 352
apply generic_format_round...
apply Zle_trans with (cexp (x+y)).
apply monotone_exp.
353
rewrite <- ln_beta_minus1; try assumption.
354
rewrite <- (ln_beta_abs beta (x+y)).
355
(* . *)
356
assert (U:(Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R).
357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399
assert (V: forall x y, (Rabs y <= Rabs x)%R -> 
   (Rabs (x+y) = Rabs x + Rabs y)%R \/ (y <> 0 /\ Rabs (x+y)=Rabs x - Rabs y)%R).
clear; intros x y.
case (Rle_or_lt 0 y); intros Hy.
case Hy; intros Hy'.
case (Rle_or_lt 0 x); intros Hx.
intros _; rewrite (Rabs_right y); [idtac|now apply Rle_ge].
rewrite (Rabs_right x); [idtac|now apply Rle_ge].
left; apply Rabs_right.
apply Rle_ge; apply Rplus_le_le_0_compat; assumption.
rewrite (Rabs_right y); [idtac|now apply Rle_ge].
rewrite (Rabs_left x); [idtac|assumption].
intros H; right; split.
now apply Rgt_not_eq.
rewrite Rabs_left1.
ring.
apply Rplus_le_reg_l with (-x)%R; ring_simplify; assumption.
intros _; left.
now rewrite <- Hy', Rabs_R0, 2!Rplus_0_r.
case (Rle_or_lt 0 x); intros Hx.
rewrite (Rabs_left y); [idtac|assumption].
rewrite (Rabs_right x); [idtac|now apply Rle_ge].
intros H; right; split.
apply sym_not_eq; now apply Rgt_not_eq.
rewrite Rabs_right.
ring.
apply Rle_ge; apply Rplus_le_reg_l with (-y)%R; ring_simplify; assumption.
intros _; left.
rewrite (Rabs_left y); [idtac|assumption].
rewrite (Rabs_left x); [idtac|assumption].
rewrite Rabs_left1.
ring.
rewrite <- (Ropp_involutive (x+y)), <- Ropp_0.
apply Ropp_le_contravar; rewrite Ropp_plus_distr.
apply Rplus_le_le_0_compat.
rewrite <- Ropp_0; apply Ropp_le_contravar; now left.
rewrite <- Ropp_0; apply Ropp_le_contravar; now left.
apply V; left.
apply ln_beta_lt_pos with beta.
now apply Rabs_pos_lt.
rewrite <- ln_beta_minus1 in H1; try assumption.
rewrite 2!ln_beta_abs; omega.
(* . *)
400 401 402 403 404 405 406 407 408 409 410 411 412 413
destruct U as [U|U].
rewrite U; apply Zle_trans with (ln_beta beta x);[omega|idtac].
rewrite <- ln_beta_abs.
apply ln_beta_le.
now apply Rabs_pos_lt.
apply Rplus_le_reg_l with (-Rabs x)%R; ring_simplify.
apply Rabs_pos.
destruct U as (U',U); rewrite U.
rewrite <- ln_beta_abs.
apply ln_beta_minus_lb.
now apply Rabs_pos_lt.
now apply Rabs_pos_lt.
rewrite 2!ln_beta_abs.
assert (ln_beta beta y < ln_beta beta x -1)%Z;[idtac|omega].
414
now rewrite (ln_beta_minus1 x Zx).
415 416 417 418 419
apply canonic_exp_round_ge...
intros K.
absurd (x+y=0)%R.
intros K'.
contradict H1; apply Zle_not_lt.
420
rewrite <- (ln_beta_minus1 x Zx).
421 422 423 424 425 426 427 428 429 430 431
replace y with (-x)%R.
rewrite ln_beta_opp; omega.
apply Rplus_eq_reg_l with x; rewrite K'; ring.
apply round_plus_eq_zero with (6:=K)...
exists n.
rewrite ulp_neq_0.
assumption.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485
Qed.

Lemma rnd_0_or_ge: Exp_not_FTZ fexp -> forall x y, format x -> format y -> 
   (round beta fexp rnd (x+y) = 0)%R \/ 
     (ulp beta fexp (x/Z2R beta) <= Rabs (round beta fexp rnd (x+y)))%R.
Proof with auto with typeclass_instances.
intros exp_not_FTZ x y Fx Fy.
case (Req_dec x 0); intros Zx.
(* *)
rewrite Zx, Rplus_0_l.
rewrite round_generic...
unfold Rdiv; rewrite Rmult_0_l.
rewrite Fy at 2.
unfold F2R; simpl; rewrite Rabs_mult.
rewrite (Rabs_right (bpow _)).
2: apply Rle_ge, bpow_ge_0.
case (Z.eq_dec (Ztrunc (scaled_mantissa beta fexp y)) 0); intros Hm.
left.
rewrite Fy, Hm; unfold F2R; simpl; ring.
right.
apply Rle_trans with (1*bpow (cexp y))%R.
rewrite Rmult_1_l.
rewrite <- ulp_neq_0.
apply ulp_ge_ulp_0...
intros K; apply Hm.
rewrite K, scaled_mantissa_0.
replace 0%R with (Z2R 0) by reflexivity.
apply Ztrunc_Z2R.
apply Rmult_le_compat_r.
apply bpow_ge_0.
rewrite <- Z2R_abs.
replace 1%R with (Z2R 1) by reflexivity.
apply Z2R_le.
assert (0 < Z.abs (Ztrunc (scaled_mantissa beta fexp y)))%Z;[|omega].
now apply Z.abs_pos.
(* *)
destruct (rnd_plus_mutiple x y Fx Fy Zx) as (m,Hm).
case (Z.eq_dec m 0); intros Zm.
left.
rewrite Hm, Zm; simpl; ring.
right.
rewrite Hm, Rabs_mult.
rewrite (Rabs_right (ulp _ _ _)).
2: apply Rle_ge, ulp_ge_0.
apply Rle_trans with (1*ulp beta fexp (x/Z2R beta))%R.
right; ring.
apply Rmult_le_compat_r.
apply ulp_ge_0.
rewrite <- Z2R_abs.
replace 1%R with (Z2R 1) by reflexivity.
apply Z2R_le.
assert (0 < Z.abs m)%Z;[|omega].
now apply Z.abs_pos.
Qed.
486

487 488 489 490
End Fprop_plus_multi.
Section Fprop_plus_multii.
Variable beta : radix.
Notation bpow e := (bpow beta e).
491

492 493 494 495
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
496

497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525
Lemma rnd_0_or_ge_FLT: forall x y e, 
    generic_format beta (FLT_exp emin prec) x -> generic_format beta (FLT_exp emin prec) y ->
    (bpow e <= Rabs x)%R ->
   (round beta (FLT_exp emin prec) rnd (x+y) = 0)%R \/ 
     (bpow (e - prec) <= Rabs (round beta (FLT_exp emin prec) rnd (x+y)))%R.
Proof with auto with typeclass_instances.
intros x y e Fx Fy He.
assert (Zx:(x <> 0)%R).
intros K; contradict He.
apply Rlt_not_le; rewrite K, Rabs_R0.
apply bpow_gt_0.
case rnd_0_or_ge with beta (FLT_exp emin prec) rnd x y...
intros H; right.
apply Rle_trans with (2:=H).
rewrite ulp_neq_0.
unfold canonic_exp.
rewrite <- ln_beta_minus1; try assumption.
unfold FLT_exp; apply bpow_le.
apply Zle_trans with (2:=Z.le_max_l _ _).
destruct (ln_beta beta x) as (n,Hn); simpl.
assert (e < n)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
Qed.
526 527


528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555
Lemma rnd_0_or_ge_FLX: forall x y e, 
    generic_format beta (FLX_exp prec) x -> generic_format beta (FLX_exp prec) y ->
    (bpow e <= Rabs x)%R ->
   (round beta (FLX_exp prec) rnd (x+y) = 0)%R \/ 
     (bpow (e - prec) <= Rabs (round beta (FLX_exp prec) rnd (x+y)))%R.
Proof with auto with typeclass_instances.
intros x y e Fx Fy He.
assert (Zx:(x <> 0)%R).
intros K; contradict He.
apply Rlt_not_le; rewrite K, Rabs_R0.
apply bpow_gt_0.
case rnd_0_or_ge with beta (FLX_exp prec) rnd x y...
intros H; right.
apply Rle_trans with (2:=H).
rewrite ulp_neq_0.
unfold canonic_exp.
rewrite <- ln_beta_minus1; try assumption.
unfold FLX_exp; apply bpow_le.
destruct (ln_beta beta x) as (n,Hn); simpl.
assert (e < n)%Z; try omega.
apply lt_bpow with beta.
apply Rle_lt_trans with (1:=He).
now apply Hn.
apply Rmult_integral_contrapositive_currified; try assumption.
apply Rinv_neq_0_compat.
apply Rgt_not_eq.
apply radix_pos.
Qed.
556

557
End Fprop_plus_multii.