Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Fcalc_bracket.v 16.1 KB
Newer Older
1 2 3 4 5
Require Import Fcore.

Section Fcalc_bracket.

Variable d u : R.
6
Hypothesis Hdu : (d < u)%R.
7

8
Inductive location := loc_Exact | loc_Inexact : comparison -> location.
9 10 11 12

Variable x : R.

Inductive inbetween : location -> Prop :=
13 14
  | inbetween_Exact : x = d -> inbetween loc_Exact
  | inbetween_Inexact l : (d < x < u)%R -> Rcompare x ((d + u) / 2)%R = l -> inbetween (loc_Inexact l).
15

Guillaume Melquiond's avatar
Guillaume Melquiond committed
16 17
Section Fcalc_bracket_any.

18 19 20 21
Variable l : location.

Theorem inbetween_bounds :
  inbetween l ->
22
  (d <= x < u)%R.
23
Proof.
24
intros [Hx|l' Hx Hl] ; clear l.
25 26 27 28
rewrite Hx.
split.
apply Rle_refl.
exact Hdu.
29
now split ; try apply Rlt_le.
30 31
Qed.

32
Theorem inbetween_bounds_not_Eq :
33
  inbetween l ->
34
  l <> loc_Exact ->
35 36
  (d < x < u)%R.
Proof.
37 38 39
intros [Hx|l' Hx Hl] H.
now elim H.
exact Hx.
40 41
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
42 43
End Fcalc_bracket_any.

44 45 46 47
Theorem inbetween_distance_inexact :
  forall l,
  inbetween (loc_Inexact l) ->
  Rcompare (x - d) (u - x) = l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
48
Proof.
49 50 51
intros l Hl.
inversion_clear Hl as [|l' Hl' Hx].
now rewrite Rcompare_middle.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52 53
Qed.

54 55 56 57
Theorem inbetween_distance_inexact_abs :
  forall l,
  inbetween (loc_Inexact l) ->
  Rcompare (Rabs (d - x)) (Rabs (u - x)) = l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
58
Proof.
59 60 61
intros l Hl.
rewrite Rabs_left1.
rewrite Rabs_pos_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
62
rewrite Ropp_minus_distr.
63 64 65 66 67 68
now apply inbetween_distance_inexact.
apply Rle_0_minus.
apply Rlt_le.
apply (inbetween_bounds _ Hl).
apply Rle_minus.
apply (inbetween_bounds _ Hl).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
69 70
Qed.

71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
End Fcalc_bracket.

Section Fcalc_bracket_step.

Variable start step : R.
Variable nb_steps : Z.
Variable Hstep : (0 < step)%R.

Lemma ordered_steps :
  forall k,
  (start + Z2R k * step < start + Z2R (k + 1) * step)%R.
Proof.
intros k.
apply Rplus_lt_compat_l.
apply Rmult_lt_compat_r.
exact Hstep.
apply Z2R_lt.
apply Zlt_succ.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
91
Lemma middle_range :
92 93 94 95 96 97 98
  forall k,
  ((start + (start + Z2R k * step)) / 2 = start + (Z2R k / 2 * step))%R.
Proof.
intros k.
field.
Qed.

99 100
Hypothesis (Hnb_steps : (1 < nb_steps)%Z).

101 102
Lemma inbetween_step_not_Eq :
  forall x k l l',
103
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
104 105 106
  (0 < k < nb_steps)%Z ->
  Rcompare x (start + (Z2R nb_steps / 2 * step))%R = l' ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l').
107
Proof.
108
intros x k l l' Hx Hk Hl'.
109 110
constructor.
(* . *)
111 112 113
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
split.
apply Rlt_le_trans with (2 := proj1 Hx').
114 115 116 117 118
rewrite <- (Rplus_0_r start) at 1.
apply Rplus_lt_compat_l.
apply Rmult_lt_0_compat.
now apply (Z2R_lt 0).
exact Hstep.
119
apply Rlt_le_trans with (1 := proj2 Hx').
120 121 122
apply Rplus_le_compat_l.
apply Rmult_le_compat_r.
now apply Rlt_le.
123 124 125
apply Z2R_le.
omega.
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126
now rewrite middle_range.
127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143
Qed.

Theorem inbetween_step_Lo :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  (0 < k)%Z -> (2 * k + 1 < nb_steps)%Z ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).
Proof.
intros x k l Hx Hk1 Hk2.
apply inbetween_step_not_Eq with (1 := Hx).
omega.
apply Rcompare_Lt.
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
apply Rlt_le_trans with (1 := proj2 Hx').
apply Rcompare_not_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply Rcompare_not_Lt.
144 145 146 147
change 2%R with (Z2R 2).
rewrite <- mult_Z2R.
apply Z2R_le.
omega.
148
exact Hstep.
149 150 151 152 153 154
Qed.

Theorem inbetween_step_Hi :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  (nb_steps < 2 * k)%Z -> (k < nb_steps)%Z ->
155
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt).
156 157
Proof.
intros x k l Hx Hk1 Hk2.
158 159 160 161 162 163 164 165
apply inbetween_step_not_Eq with (1 := Hx).
omega.
apply Rcompare_Gt.
assert (Hx' := inbetween_bounds _ _ (ordered_steps _) _ _ Hx).
apply Rlt_le_trans with (2 := proj1 Hx').
apply Rcompare_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
apply Rcompare_Lt.
166 167 168
change 2%R with (Z2R 2).
rewrite <- mult_Z2R.
apply Z2R_lt.
169 170
omega.
exact Hstep.
171 172
Qed.

173
Theorem inbetween_step_Lo_not_Eq :
174 175
  forall x l,
  inbetween start (start + step) x l ->
176 177
  l <> loc_Exact ->
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).
178 179
Proof.
intros x l Hx Hl.
180
assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
181 182
constructor.
(* . *)
183 184 185 186
split.
apply Hx'.
apply Rlt_trans with (1 := proj2 Hx').
apply Rplus_lt_compat_l.
187
rewrite <- (Rmult_1_l step) at 1.
188 189 190 191 192 193
apply Rmult_lt_compat_r.
exact Hstep.
now apply (Z2R_lt 1).
(* . *)
apply Rcompare_Lt.
apply Rlt_le_trans with (1 := proj2 Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
194
rewrite middle_range.
195 196 197 198 199 200 201 202
apply Rcompare_not_Lt_inv.
rewrite <- (Rmult_1_l step) at 2.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_l.
rewrite Rmult_1_r.
apply Rcompare_not_Lt.
apply (Z2R_le 2).
now apply (Zlt_le_succ 1).
exact Hstep.
203 204 205 206 207
Qed.

Lemma middle_odd :
  forall k,
  (2 * k + 1 = nb_steps)%Z ->
208
  (((start + Z2R k * step) + (start + Z2R (k + 1) * step))/2 = start + Z2R nb_steps /2 * step)%R.
209 210
Proof.
intros k Hk.
211 212 213
rewrite <- Hk.
rewrite 2!plus_Z2R, mult_Z2R.
simpl. field.
214 215
Qed.

216
Theorem inbetween_step_any_Mi_odd :
217
  forall x k l,
218
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x (loc_Inexact l) ->
219
  (2 * k + 1 = nb_steps)%Z ->
220
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact l).
221
Proof.
222 223
intros x k l Hx Hk.
apply inbetween_step_not_Eq with (1 := Hx).
224
omega.
225 226
inversion_clear Hx as [|l' _ Hl].
now rewrite (middle_odd _ Hk) in Hl.
227 228
Qed.

229
Theorem inbetween_step_Lo_Mi_Eq_odd :
230
  forall x k,
231
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact ->
232
  (2 * k + 1 = nb_steps)%Z ->
233
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Lt).
234 235
Proof.
intros x k Hx Hk.
236
apply inbetween_step_not_Eq with (1 := Hx).
237
omega.
238 239 240 241 242 243 244 245 246 247
inversion_clear Hx as [Hl|].
rewrite Hl.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
apply Rcompare_Lt.
change 2%R with (Z2R 2).
rewrite <- mult_Z2R.
apply Z2R_lt.
rewrite <- Hk.
apply Zlt_succ.
exact Hstep.
248 249 250 251 252
Qed.

Theorem inbetween_step_Hi_Mi_even :
  forall x k l,
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
253
  l <> loc_Exact ->
254
  (2 * k = nb_steps)%Z ->
255
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Gt).
256 257
Proof.
intros x k l Hx Hl Hk.
258
apply inbetween_step_not_Eq with (1 := Hx).
259
omega.
260 261 262 263 264 265 266 267 268 269 270 271
apply Rcompare_Gt.
assert (Hx' := inbetween_bounds_not_Eq _ _ _ _ Hx Hl).
apply Rle_lt_trans with (2 := proj1 Hx').
apply Rcompare_not_Lt_inv.
rewrite Rcompare_plus_l, Rcompare_mult_r, Rcompare_half_r.
change 2%R with (Z2R 2).
rewrite <- mult_Z2R.
apply Rcompare_not_Lt.
apply Z2R_le.
rewrite Hk.
apply Zle_refl.
exact Hstep.
272 273 274 275
Qed.

Theorem inbetween_step_Mi_Mi_even :
  forall x k,
276
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x loc_Exact ->
277
  (2 * k = nb_steps)%Z ->
278
  inbetween start (start + Z2R nb_steps * step) x (loc_Inexact Eq).
279 280
Proof.
intros x k Hx Hk.
281 282 283 284 285
apply inbetween_step_not_Eq with (1 := Hx).
omega.
apply Rcompare_Eq.
inversion_clear Hx as [Hx'|].
rewrite Hx', <- Hk, mult_Z2R.
286
simpl (Z2R 2).
287
field.
288 289 290 291
Qed.

Definition new_location_even k l :=
  if Zeq_bool k 0 then
292
    match l with loc_Exact => l | _ => loc_Inexact Lt end
293
  else
294
    loc_Inexact
295
    match Zcompare (2 * k) nb_steps with
296 297 298
    | Lt => Lt
    | Eq => match l with loc_Exact => Eq | _ => Gt end
    | Gt => Gt
299 300 301
    end.

Theorem new_location_even_correct :
302
  Zeven nb_steps = true ->
303 304 305 306 307 308 309 310 311 312
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location_even k l).
Proof.
intros He x k l Hk Hx.
unfold new_location_even.
destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
(* k = 0 *)
rewrite Hk0 in Hx.
rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
313 314
set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
315 316 317 318 319
unfold l' ; case l ; try (now left) ; right ; now split.
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
constructor.
rewrite H1 in Hx.
now inversion_clear Hx.
320
now apply inbetween_step_Lo_not_Eq with (2 := H1).
321 322 323 324
(* k <> 0 *)
destruct (Zcompare_spec (2 * k) nb_steps) as [Hk1|Hk1|Hk1].
(* . 2 * k < nb_steps *)
apply inbetween_step_Lo with (1 := Hx).
325
omega.
326 327
destruct (Zeven_ex nb_steps).
rewrite He in H.
328 329
omega.
(* . 2 * k = nb_steps *)
330 331
set (l' := match l with loc_Exact => Eq | _ => Gt end).
assert ((l = loc_Exact /\ l' = Eq) \/ (l <> loc_Exact /\ l' = Gt)).
332 333 334 335 336 337 338 339 340 341 342 343 344
unfold l' ; case l ; try (now left) ; right ; now split.
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
rewrite H1 in Hx.
now apply inbetween_step_Mi_Mi_even with (1 := Hx).
now apply inbetween_step_Hi_Mi_even with (1 := Hx).
(* . 2 * k > nb_steps *)
apply inbetween_step_Hi with (1 := Hx).
exact Hk1.
apply Hk.
Qed.

Definition new_location_odd k l :=
  if Zeq_bool k 0 then
345
    match l with loc_Exact => l | _ => loc_Inexact Lt end
346
  else
347
    loc_Inexact
348
    match Zcompare (2 * k + 1) nb_steps with
349 350 351
    | Lt => Lt
    | Eq => match l with loc_Inexact l => l | loc_Exact => Lt end
    | Gt => Gt
352 353 354
    end.

Theorem new_location_odd_correct :
355
  Zeven nb_steps = false ->
356 357 358 359 360 361 362 363 364 365
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location_odd k l).
Proof.
intros Ho x k l Hk Hx.
unfold new_location_odd.
destruct (Zeq_bool_spec k 0) as [Hk0|Hk0].
(* k = 0 *)
rewrite Hk0 in Hx.
rewrite Rmult_0_l, Rplus_0_r, Rmult_1_l in Hx.
366 367
set (l' := match l with loc_Exact => l | _ => loc_Inexact Lt end).
assert ((l = loc_Exact /\ l' = loc_Exact) \/ (l <> loc_Exact /\ l' = loc_Inexact Lt)).
368 369 370 371 372
unfold l' ; case l ; try (now left) ; right ; now split.
destruct H as [(H1,H2)|(H1,H2)] ; rewrite H2.
constructor.
rewrite H1 in Hx.
now inversion_clear Hx.
373
now apply inbetween_step_Lo_not_Eq with (2 := H1).
374 375 376 377
(* k <> 0 *)
destruct (Zcompare_spec (2 * k + 1) nb_steps) as [Hk1|Hk1|Hk1].
(* . 2 * k + 1 < nb_steps *)
apply inbetween_step_Lo with (1 := Hx) (3 := Hk1).
378
omega.
379 380
(* . 2 * k + 1 = nb_steps *)
destruct l.
381 382
apply inbetween_step_Lo_Mi_Eq_odd with (1 := Hx) (2 := Hk1).
apply inbetween_step_any_Mi_odd with (1 := Hx) (2 := Hk1).
383 384
(* . 2 * k + 1 > nb_steps *)
apply inbetween_step_Hi with (1 := Hx).
385 386
destruct (Zeven_ex nb_steps).
rewrite Ho in H.
387 388 389 390
omega.
apply Hk.
Qed.

391
Definition new_location :=
392
  if Zeven nb_steps then new_location_even else new_location_odd.
393 394 395 396 397 398 399 400 401 402 403 404 405 406

Theorem new_location_correct :
  forall x k l, (0 <= k < nb_steps)%Z ->
  inbetween (start + Z2R k * step) (start + Z2R (k + 1) * step) x l ->
  inbetween start (start + Z2R nb_steps * step) x (new_location k l).
Proof.
intros x k l Hk Hx.
unfold new_location.
generalize (refl_equal nb_steps) (Zle_lt_trans _ _ _ (proj1 Hk) (proj2 Hk)).
pattern nb_steps at 2 3 5 ; case nb_steps.
now intros _.
(* . *)
intros [p|p|] Hp _.
apply new_location_odd_correct with (2 := Hk) (3 := Hx).
407
now rewrite Hp.
408
apply new_location_even_correct with (2 := Hk) (3 := Hx).
409
now rewrite Hp.
410 411 412 413 414
now rewrite Hp in Hnb_steps.
(* . *)
now intros p _.
Qed.

415 416
End Fcalc_bracket_step.

417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
Section Fcalc_bracket_scale.

Lemma inbetween_mult_aux :
  forall x d s,
  ((x * s + d * s) / 2 = (x + d) / 2 * s)%R.
Proof.
intros x d s.
field.
Qed.

Theorem inbetween_mult_compat :
  forall x d u l s,
  (0 < s)%R ->
  inbetween x d u l ->
  inbetween (x * s) (d * s) (u * s) l.
Proof.
433 434 435
intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
now rewrite Hx.
now split ; apply Rmult_lt_compat_r.
436
rewrite inbetween_mult_aux.
437
now rewrite Rcompare_mult_r.
438 439 440 441 442 443 444 445
Qed.

Theorem inbetween_mult_reg :
  forall x d u l s,
  (0 < s)%R ->
  inbetween (x * s) (d * s) (u * s) l ->
  inbetween x d u l.
Proof.
446 447
intros x d u l s Hs [Hx|l' Hx Hl] ; constructor.
apply Rmult_eq_reg_r with (1 := Hx).
448
now apply Rgt_not_eq.
449 450 451
now split ; apply Rmult_lt_reg_r with s.
rewrite <- Rcompare_mult_r with (1 := Hs).
now rewrite inbetween_mult_aux in Hl.
452 453 454 455
Qed.

End Fcalc_bracket_scale.

456 457 458
Section Fcalc_bracket_generic.

Variable beta : radix.
459
Notation bpow e := (bpow beta e).
460 461 462 463 464

Variable fexp : Z -> Z.
Hypothesis prop_exp : valid_exp fexp.
Notation format := (generic_format beta fexp).

465 466 467
Definition inbetween_float m e x l :=
  inbetween (F2R (Float beta m e)) (F2R (Float beta (m + 1) e)) x l.

468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483
Theorem inbetween_float_bounds :
  forall x m e l,
  inbetween_float m e x l ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R.
Proof.
intros x m e l [Hx|l' Hx Hl].
rewrite Hx.
split.
apply Rle_refl.
apply F2R_lt_compat.
apply Zlt_succ.
split.
now apply Rlt_le.
apply Hx.
Qed.

484 485 486
Definition inbetween_int m x l :=
  inbetween (Z2R m) (Z2R (m + 1)) x l.

487
Theorem inbetween_float_new_location :
488 489
  forall x m e l k,
  (0 < k)%Z ->
490
  inbetween_float m e x l ->
491
  inbetween_float (Zdiv m (Zpower (radix_val beta) k)) (e + k) x (new_location (Zpower (radix_val beta) k) (Zmod m (Zpower (radix_val beta) k)) l).
492
Proof.
493
intros x m e l k Hk Hx.
494
unfold inbetween_float in *.
495 496 497 498 499 500 501 502
assert (Hr: forall m, F2R (Float beta m (e + k)) = F2R (Float beta (m * Zpower (radix_val beta) k) e)).
clear -Hk. intros m.
rewrite (F2R_change_exp beta e).
apply (f_equal (fun r => F2R (Float beta (m * Zpower _ r) e))).
ring.
omega.
assert (Hp: (Zpower (radix_val beta) k > 0)%Z).
apply Zlt_gt.
503
now apply Zpower_gt_0.
504 505 506 507 508 509 510
(* . *)
rewrite 2!Hr.
rewrite Zmult_plus_distr_l, Zmult_1_l.
unfold F2R at 2. simpl.
rewrite plus_Z2R, Rmult_plus_distr_r.
apply new_location_correct.
apply bpow_gt_0.
511 512
now apply Zpower_gt_1.
now apply Z_mod_lt.
513 514
rewrite <- 2!Rmult_plus_distr_r, <- 2!plus_Z2R.
rewrite Zmult_comm, Zplus_assoc.
515 516 517 518 519 520 521 522 523 524 525 526
now rewrite <- Z_div_mod_eq.
Qed.

Theorem inbetween_float_new_location_single :
  forall x m e l,
  inbetween_float m e x l ->
  inbetween_float (Zdiv m (radix_val beta)) (e + 1) x (new_location (radix_val beta) (Zmod m (radix_val beta)) l).
Proof.
intros x m e l Hx.
replace (radix_val beta) with (Zpower (radix_val beta) 1).
now apply inbetween_float_new_location.
apply Zmult_1_r.
527 528
Qed.

529 530
Theorem inbetween_float_rounding :
  forall rnd choice,
531
  ( forall x m e l, inbetween_int m x l -> Zrnd rnd x e = choice m e l ) ->
532 533 534
  forall x m l,
  let e := canonic_exponent beta fexp x in
  inbetween_float m e x l ->
535
  rounding beta fexp rnd x = F2R (Float beta (choice m e l) e).
536 537 538 539 540 541 542 543 544 545
Proof.
intros rnd choice Hc x m l e Hl.
unfold rounding, F2R. simpl.
apply (f_equal (fun m => (Z2R m * bpow e)%R)).
apply Hc.
apply inbetween_mult_reg with (bpow e).
apply bpow_gt_0.
now rewrite scaled_mantissa_bpow.
Qed.

546
Theorem inbetween_float_DN :
547 548
  forall x m l,
  let e := canonic_exponent beta fexp x in
549
  inbetween_float m e x l ->
550
  rounding beta fexp ZrndDN x = F2R (Float beta m e).
551
Proof.
552 553 554
apply inbetween_float_rounding with (choice := fun m e l => m).
intros x m e l Hl.
refine (Zfloor_imp m _ _).
555
apply inbetween_bounds with (2 := Hl).
556
apply Z2R_lt.
557 558 559 560 561 562 563
apply Zlt_succ.
Qed.

Definition cond_incr (b : bool) m := if b then (m + 1)%Z else m.

Definition round_UP l :=
  match l with
564
  | loc_Exact => false
565 566 567 568
  | _ => true
  end.

Theorem inbetween_float_UP :
569 570
  forall x m l,
  let e := canonic_exponent beta fexp x in
571
  inbetween_float m e x l ->
572
  rounding beta fexp ZrndUP x = F2R (Float beta (cond_incr (round_UP l) m) e).
573
Proof.
574 575
apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_UP l) m).
intros x m e l Hl.
576
assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)).
577 578
case l ; try (now left) ; now right ; split.
destruct Hl' as [Hl'|(Hl1, Hl2)].
579
(* Exact *)
580 581 582
rewrite Hl'.
destruct Hl ; try easy.
rewrite H.
583
exact (Zceil_Z2R _).
584
(* not Exact *)
585
rewrite Hl2.
586 587 588
simpl.
apply Zceil_imp.
ring_simplify (m + 1 - 1)%Z.
589
refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
590
apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl).
591 592 593 594
Qed.

Definition round_NE (p : bool) l :=
  match l with
595 596 597 598
  | loc_Exact => false
  | loc_Inexact Lt => false
  | loc_Inexact Eq => if p then false else true
  | loc_Inexact Gt => true
599 600 601
  end.

Theorem inbetween_float_NE :
602
  forall x m l,
603
  let e := canonic_exponent beta fexp x in
604
  inbetween_float m e x l ->
605
  rounding beta fexp ZrndNE x = F2R (Float beta (cond_incr (round_NE (Zeven m) l) m) e).
606
Proof.
607 608
apply inbetween_float_rounding with (choice := fun m e l => cond_incr (round_NE (Zeven m) l) m).
intros x m e l Hl.
609 610 611 612 613
inversion_clear Hl as [Hx|l' Hx Hl'].
(* Exact *)
rewrite Hx.
now rewrite Zrnd_Z2R.
(* not Exact *)
614
unfold Zrnd, ZrndNE, ZrndN, Znearest, mkZrounding2.
615 616 617 618 619 620 621 622 623 624 625 626 627 628 629
assert (Hm: Zfloor x = m).
apply Zfloor_imp.
exact (conj (Rlt_le _ _ (proj1 Hx)) (proj2 Hx)).
rewrite Zceil_floor_neq.
rewrite Hm.
replace (Rcompare (x - Z2R m) (/2)) with l'.
now case l'.
rewrite <- Hl'.
rewrite plus_Z2R.
rewrite <- (Rcompare_plus_r (- Z2R m) x).
apply f_equal.
simpl (Z2R 1).
field.
rewrite Hm.
now apply Rlt_not_eq.
630 631
Qed.

632
End Fcalc_bracket_generic.