Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Fcore_ulp.v 59.8 KB
Newer Older
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
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
(** * Unit in the Last Place: our definition using fexp and its properties, successor and predecessor *)
21 22 23 24 25
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
26

27
Section Fcore_ulp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
28 29 30

Variable beta : radix.

31
Notation bpow e := (bpow beta e).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
32 33 34

Variable fexp : Z -> Z.

35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52
(** Definition and basic properties about the minimal exponent, when it exists *)

Lemma Z_le_dec_aux: forall x y : Z, (x <= y)%Z \/ ~ (x <= y)%Z.
intros.
destruct (Z_le_dec x y).
now left.
now right.
Qed.


(** [negligible_exp] is either none (as in FLX) or Some n such that n <= fexp n. *)
Definition negligible_exp: option Z :=
  match (LPO_Z _ (fun z => Z_le_dec_aux z (fexp z))) with
   | inleft N => Some (proj1_sig N)
   | inright _ => None
 end.


53 54 55 56 57 58 59 60 61 62 63 64
Inductive negligible_exp_prop: option Z -> Prop :=
  | negligible_None: (forall n, (fexp n < n)%Z) -> negligible_exp_prop None
  | negligible_Some: forall n, (n <= fexp n)%Z -> negligible_exp_prop (Some n).


Lemma negligible_exp_spec: negligible_exp_prop negligible_exp.
Proof.
unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
now apply negligible_Some.
apply negligible_None.
intros n; specialize (Hn n); omega.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
65 66 67 68 69 70 71 72 73

Lemma negligible_exp_spec': (negligible_exp = None /\ forall n, (fexp n < n)%Z)
           \/ exists n, (negligible_exp = Some n /\ (n <= fexp n)%Z).
Proof.
unfold negligible_exp; destruct LPO_Z as [(n,Hn)|Hn].
right; simpl; exists n; now split.
left; split; trivial.
intros n; specialize (Hn n); omega.
Qed.
74

75
Context { valid_exp : Valid_exp fexp }.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
76

77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101
Lemma fexp_negligible_exp_eq: forall n m, (n <= fexp n)%Z -> (m <= fexp m)%Z -> fexp n = fexp m.
Proof.
intros n m Hn Hm.
case (Zle_or_lt n m); intros H.
apply valid_exp; omega.
apply sym_eq, valid_exp; omega.
Qed.


(** Definition and basic properties about the ulp *)

Definition ulp x := match Req_bool x 0 with
  | true   => match negligible_exp with
            | Some n => bpow (fexp n)
            | None => 0%R
            end
  | false  => bpow (canonic_exp beta fexp x)
 end.

Lemma ulp_neq_0 : forall x:R, (x <> 0)%R -> ulp x = bpow (canonic_exp beta fexp x).
Proof.
intros  x Hx.
unfold ulp; case (Req_bool_spec x); trivial.
intros H; now contradict H.
Qed.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
102

103
Notation F := (generic_format beta fexp).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
104

105 106 107 108 109
Theorem ulp_opp :
  forall x, ulp (- x) = ulp x.
Proof.
intros x.
unfold ulp.
110 111 112 113
case Req_bool_spec; intros H1.
rewrite Req_bool_true; trivial.
rewrite <- (Ropp_involutive x), H1; ring.
rewrite Req_bool_false.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
114
now rewrite canonic_exp_opp.
115
intros H2; apply H1; rewrite H2; ring.
116 117 118 119 120 121
Qed.

Theorem ulp_abs :
  forall x, ulp (Rabs x) = ulp x.
Proof.
intros x.
122 123 124 125
unfold ulp; case (Req_bool_spec x 0); intros H1.
rewrite Req_bool_true; trivial.
now rewrite H1, Rabs_R0.
rewrite Req_bool_false.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
126
now rewrite canonic_exp_abs.
127 128 129
now apply Rabs_no_R0.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
130
Theorem ulp_ge_0:
131 132 133 134 135 136 137
  forall x, (0 <= ulp x)%R.
Proof.
intros x; unfold ulp; case Req_bool_spec; intros.
case negligible_exp; intros.
apply bpow_ge_0.
apply Rle_refl.
apply bpow_ge_0.
138 139
Qed.

140

141
Theorem ulp_le_id:
142
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
143
    (0 < x)%R ->
144
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
145 146 147 148 149
    (ulp x <= x)%R.
Proof.
intros x Zx Fx.
rewrite <- (Rmult_1_l (ulp x)).
pattern x at 2; rewrite Fx.
150 151 152
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
unfold F2R; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
153 154 155 156 157
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
apply Z2R_le.
apply Zlt_le_succ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
158
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
159 160 161 162
now rewrite <- Fx.
Qed.

Theorem ulp_le_abs:
163
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
164
    (x <> 0)%R ->
165
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
166 167 168
    (ulp x <= Rabs x)%R.
Proof.
intros x Zx Fx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
169
rewrite <- ulp_abs.
170
apply ulp_le_id.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
171 172
now apply Rabs_pos_lt.
now apply generic_format_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
173 174
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
175 176 177

(* was ulp_DN_UP *)
Theorem round_UP_DN_ulp :
178
  forall x, ~ F x ->
179
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
180
Proof.
181
intros x Fx.
182 183
rewrite ulp_neq_0.
unfold round. simpl.
184 185
unfold F2R. simpl.
rewrite Zceil_floor_neq.
186
rewrite Z2R_plus. simpl.
187
ring.
188
intros H.
189
apply Fx.
190
unfold generic_format, F2R. simpl.
191 192 193
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
194
now rewrite scaled_mantissa_mult_bpow.
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223
intros V; apply Fx.
rewrite V.
apply generic_format_0.
Qed.


Theorem ulp_bpow :
  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
intros e.
rewrite ulp_neq_0.
apply f_equal.
apply canonic_exp_fexp.
rewrite Rabs_pos_eq.
split.
ring_simplify (e + 1 - 1)%Z.
apply Rle_refl.
apply bpow_lt.
apply Zlt_succ.
apply bpow_ge_0.
apply Rgt_not_eq, Rlt_gt, bpow_gt_0.
Qed.


Lemma generic_format_ulp_0:
  F (ulp 0).
Proof.
unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
224 225
intros _; apply generic_format_0.
intros n H1.
226 227 228 229 230 231 232 233 234 235
apply generic_format_bpow.
now apply valid_exp.
Qed.

Lemma generic_format_bpow_ge_ulp_0:  forall e,
    (ulp 0 <= bpow e)%R -> F (bpow e).
Proof.
intros e; unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
236
intros H1 _.
237
apply generic_format_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
238 239
specialize (H1 (e+1)%Z); omega.
intros n H1 H2.
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 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285
apply generic_format_bpow.
case (Zle_or_lt (e+1) (fexp (e+1))); intros H4.
absurd (e+1 <= e)%Z.
omega.
apply Zle_trans with (1:=H4).
replace (fexp (e+1)) with (fexp n).
now apply le_bpow with beta.
now apply fexp_negligible_exp_eq.
omega.
Qed.

(** The three following properties are equivalent:
      [Exp_not_FTZ] ;  forall x, F (ulp x) ; forall x, ulp 0 <= ulp x *)

Lemma generic_format_ulp: Exp_not_FTZ fexp ->
  forall x,  F (ulp x).
Proof.
unfold Exp_not_FTZ; intros H x.
case (Req_dec x 0); intros Hx.
rewrite Hx; apply generic_format_ulp_0.
rewrite (ulp_neq_0 _ Hx).
apply generic_format_bpow; unfold canonic_exp.
apply H.
Qed.

Lemma not_FTZ_generic_format_ulp:
   (forall x,  F (ulp x)) -> Exp_not_FTZ fexp.
intros H e.
specialize (H (bpow (e-1))).
rewrite ulp_neq_0 in H.
2: apply Rgt_not_eq, bpow_gt_0.
unfold canonic_exp in H.
rewrite ln_beta_bpow in H.
apply generic_format_bpow_inv' in H...
now replace (e-1+1)%Z with e in H by ring.
Qed.


Lemma ulp_ge_ulp_0: Exp_not_FTZ fexp ->
  forall x,  (ulp 0 <= ulp x)%R.
Proof.
unfold Exp_not_FTZ; intros H x.
case (Req_dec x 0); intros Hx.
rewrite Hx; now right.
unfold ulp at 1.
rewrite Req_bool_true; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
286 287
case negligible_exp_spec'.
intros (H1,H2); rewrite H1; apply ulp_ge_0.
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
intros (n,(H1,H2)); rewrite H1.
rewrite ulp_neq_0; trivial.
apply bpow_le; unfold canonic_exp.
generalize (ln_beta beta x); intros l.
case (Zle_or_lt l (fexp l)); intros Hl.
rewrite (fexp_negligible_exp_eq n l); trivial; apply Zle_refl.
case (Zle_or_lt (fexp n) (fexp l)); trivial; intros K.
absurd (fexp n <= fexp l)%Z.
omega.
apply Zle_trans with (2:= H _).
apply Zeq_le, sym_eq, valid_exp; trivial.
omega.
Qed.

Lemma not_FTZ_ulp_ge_ulp_0:
   (forall x,  (ulp 0 <= ulp x)%R) -> Exp_not_FTZ fexp.
Proof.
intros H e.
apply generic_format_bpow_inv' with beta.
apply generic_format_bpow_ge_ulp_0.
replace e with ((e-1)+1)%Z by ring.
rewrite <- ulp_bpow.
apply H.
Qed.



Theorem ulp_le_pos :
  forall { Hm : Monotone_exp fexp },
  forall x y: R,
  (0 <= x)%R -> (x <= y)%R ->
  (ulp x <= ulp y)%R.
Proof with auto with typeclass_instances.
intros Hm x y Hx Hxy.
destruct Hx as [Hx|Hx].
rewrite ulp_neq_0.
rewrite ulp_neq_0.
apply bpow_le.
apply Hm.
now apply ln_beta_le.
apply Rgt_not_eq, Rlt_gt.
now apply Rlt_le_trans with (1:=Hx).
now apply Rgt_not_eq.
rewrite <- Hx.
apply ulp_ge_ulp_0.
apply monotone_exp_not_FTZ...
Qed.


Theorem ulp_le :
  forall { Hm : Monotone_exp fexp },
  forall x y: R,
  (Rabs x <= Rabs y)%R ->
  (ulp x <= ulp y)%R.
Proof.
intros Hm x y Hxy.
rewrite <- ulp_abs.
rewrite <- (ulp_abs y).
apply ulp_le_pos; trivial.
apply Rabs_pos.
Qed.



(** Definition and properties of pred and succ *)

Definition pred_pos x :=
  if Req_bool x (bpow (ln_beta beta x - 1)) then
    (x - bpow (fexp (ln_beta beta x - 1)))%R
  else
    (x - ulp x)%R.

Definition succ x :=
   if (Rle_bool 0 x) then
          (x+ulp x)%R
   else
     (- pred_pos (-x))%R.

Definition pred x := (- succ (-x))%R.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
368
Theorem pred_eq_pos:
369 370 371 372 373 374 375 376 377 378 379 380 381 382 383
  forall x, (0 <= x)%R -> (pred x = pred_pos x)%R.
Proof.
intros x Hx; unfold pred, succ.
case Rle_bool_spec; intros Hx'.
assert (K:(x = 0)%R).
apply Rle_antisym; try assumption.
apply Ropp_le_cancel.
now rewrite Ropp_0.
rewrite K; unfold pred_pos.
rewrite Req_bool_false.
2: apply Rlt_not_eq, bpow_gt_0.
rewrite Ropp_0; ring.
now rewrite 2!Ropp_involutive.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
384
Theorem succ_eq_pos:
385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415
  forall x, (0 <= x)%R -> (succ x = x + ulp x)%R.
Proof.
intros x Hx; unfold succ.
now rewrite Rle_bool_true.
Qed.

Lemma pred_eq_opp_succ_opp: forall x, pred x = (- succ (-x))%R.
Proof.
reflexivity.
Qed.

Lemma succ_eq_opp_pred_opp: forall x, succ x = (- pred (-x))%R.
Proof.
intros x; unfold pred.
now rewrite 2!Ropp_involutive.
Qed.

Lemma succ_opp: forall x, (succ (-x) = - pred x)%R.
Proof.
intros x; rewrite succ_eq_opp_pred_opp.
now rewrite Ropp_involutive.
Qed.

Lemma pred_opp: forall x, (pred (-x) = - succ x)%R.
Proof.
intros x; rewrite pred_eq_opp_succ_opp.
now rewrite Ropp_involutive.
Qed.



416

417 418
(** pred and succ are in the format *)

419 420 421
(* cannont be x <> ulp 0, due to the counter-example 1-bit FP format fexp: e -> e-1 *)
(* was pred_ge_bpow *)
Theorem id_m_ulp_ge_bpow :
422 423 424 425 426 427 428 429 430 431 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
  forall x e,  F x ->
  x <> ulp x ->
  (bpow e < x)%R ->
  (bpow e <= x - ulp x)%R.
Proof.
intros x e Fx Hx' Hx.
(* *)
assert (1 <= Ztrunc (scaled_mantissa beta fexp x))%Z.
assert (0 <  Ztrunc (scaled_mantissa beta fexp x))%Z.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
rewrite <- Fx.
apply Rle_lt_trans with (2:=Hx).
apply bpow_ge_0.
omega.
case (Zle_lt_or_eq _ _ H); intros Hm.
(* *)
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_minus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_minus.
change (bpow e <= F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) - 1) (canonic_exp beta fexp x)))%R.
apply bpow_le_F2R_m1; trivial.
now rewrite <- Fx.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_trans with (2:=Hx), bpow_gt_0.
(* *)
contradict Hx'.
pattern x at 1; rewrite Fx.
rewrite  <- Hm.
rewrite ulp_neq_0.
unfold F2R; simpl.
now rewrite Rmult_1_l.
apply Rgt_not_eq, Rlt_gt.
apply Rlt_trans with (2:=Hx), bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
459 460
Qed.

461 462
(* was succ_le_bpow *)
Theorem id_p_ulp_le_bpow :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
463 464 465 466 467 468
  forall x e, (0 < x)%R -> F x ->
  (x < bpow e)%R ->
  (x + ulp x <= bpow e)%R.
Proof.
intros x e Zx Fx Hx.
pattern x at 1 ; rewrite Fx.
469 470
rewrite ulp_neq_0.
unfold F2R. simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
471
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
472 473
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
474
rewrite <- Z2R_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
475
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow e)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
476
apply F2R_p1_le_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
477
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478 479
now rewrite <- Fx.
now rewrite <- Fx.
480
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
481 482
Qed.

483 484


BOLDO Sylvie's avatar
BOLDO Sylvie committed
485
Lemma generic_format_pred_aux1:
486
  forall x, (0 < x)%R -> F x ->
487 488
  x <> bpow (ln_beta beta x - 1) ->
  F (x - ulp x).
489
Proof.
490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515
intros x Zx Fx Hx.
destruct (ln_beta beta x) as (ex, Ex).
simpl in Hx.
specialize (Ex (Rgt_not_eq _ _ Zx)).
assert (Ex' : (bpow (ex - 1) < x < bpow ex)%R).
rewrite Rabs_pos_eq in Ex.
destruct Ex as (H,H'); destruct H; split; trivial.
contradict Hx; easy.
now apply Rlt_le.
unfold generic_format, scaled_mantissa, canonic_exp.
rewrite ln_beta_unique with beta (x - ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
rewrite ulp_neq_0.
unfold scaled_mantissa.
rewrite canonic_exp_fexp with (1 := Ex).
unfold F2R. simpl.
rewrite Rmult_minus_distr_r.
rewrite Rmult_assoc.
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
change (bpow 0) with (Z2R 1).
rewrite <- Z2R_minus.
rewrite Ztrunc_Z2R.
rewrite Z2R_minus.
rewrite Rmult_minus_distr_r.
now rewrite Rmult_1_l.
now apply Rgt_not_eq.
516 517
rewrite Rabs_pos_eq.
split.
518
apply id_m_ulp_ge_bpow; trivial.
519 520 521 522 523 524 525 526 527 528 529 530
rewrite ulp_neq_0.
intro H.
assert (ex-1 < canonic_exp beta fexp x  < ex)%Z.
split ; apply (lt_bpow beta) ; rewrite <- H ; easy.
clear -H0. omega.
now apply Rgt_not_eq.
apply Ex'.
apply Rle_lt_trans with (2 := proj2 Ex').
pattern x at 3 ; rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
rewrite <-Ropp_0.
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
531
apply ulp_ge_0.
532 533 534 535 536 537 538 539 540 541
apply Rle_0_minus.
pattern x at 2; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R; simpl.
pattern (bpow (canonic_exp beta fexp x)) at 1; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R 1) by reflexivity.
apply Z2R_le.
assert (0 <  Ztrunc (scaled_mantissa beta fexp x))%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
542
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
543 544 545 546 547
rewrite <- Fx.
apply Rle_lt_trans with (2:=proj1 Ex').
apply bpow_ge_0.
omega.
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
548 549
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
550
Lemma generic_format_pred_aux2 :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
551
  forall x, (0 < x)%R -> F x ->
552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578
  let e := ln_beta_val beta x (ln_beta beta x) in
  x =  bpow (e - 1) ->
  F (x - bpow (fexp (e - 1))).
Proof.
intros x Zx Fx e Hx.
pose (f:=(x - bpow (fexp (e - 1)))%R).
fold f.
assert (He:(fexp (e-1) <= e-1)%Z).
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hx; assumption.
case (Zle_lt_or_eq _ _ He); clear He; intros He.
assert (f = F2R (Float beta (Zpower beta (e-1-(fexp (e-1))) -1) (fexp (e-1))))%R.
unfold f; rewrite Hx.
unfold F2R; simpl.
rewrite Z2R_minus, Z2R_Zpower.
rewrite Rmult_minus_distr_r, Rmult_1_l.
rewrite <- bpow_plus.
now replace (e - 1 - fexp (e - 1) + fexp (e - 1))%Z with (e-1)%Z by ring.
omega.
rewrite H.
apply generic_format_F2R.
intros _.
apply Zeq_le.
apply canonic_exp_fexp.
rewrite <- H.
unfold f; rewrite Hx.
rewrite Rabs_right.
579
split.
580 581 582 583 584 585
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
apply Rplus_le_compat ; apply bpow_le ; omega.
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
586 587
apply Rmult_le_compat_r.
apply bpow_ge_0.
588 589 590 591 592 593 594 595
replace 2%R with (Z2R 2) by reflexivity.
replace (bpow 1) with (Z2R beta).
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
596
rewrite <- bpow_plus.
597 598 599 600 601 602 603 604 605 606 607 608 609 610 611
replace (1+(e-2))%Z with (e-1)%Z by ring.
now right.
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
apply Rle_ge; apply Rle_0_minus.
apply bpow_le.
omega.
replace f with 0%R.
apply generic_format_0.
unfold f.
rewrite Hx, He.
ring.
612 613
Qed.

614

BOLDO Sylvie's avatar
BOLDO Sylvie committed
615
Theorem generic_format_succ_aux1 :
616 617 618 619 620 621 622 623
  forall x, (0 < x)%R -> F x ->
  F (x + ulp x).
Proof.
intros x Zx Fx.
destruct (ln_beta beta x) as (ex, Ex).
specialize (Ex (Rgt_not_eq _ _ Zx)).
assert (Ex' := Ex).
rewrite Rabs_pos_eq in Ex'.
624
destruct (id_p_ulp_le_bpow x ex) ; try easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
625
unfold generic_format, scaled_mantissa, canonic_exp.
626 627
rewrite ln_beta_unique with beta (x + ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
628 629
rewrite ulp_neq_0.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
630
rewrite canonic_exp_fexp with (1 := Ex).
631
unfold F2R. simpl.
632 633
rewrite Rmult_plus_distr_r.
rewrite Rmult_assoc.
634
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
635
change (bpow 0) with (Z2R 1).
636
rewrite <- Z2R_plus.
637
rewrite Ztrunc_Z2R.
638
rewrite Z2R_plus.
639 640
rewrite Rmult_plus_distr_r.
now rewrite Rmult_1_l.
641
now apply Rgt_not_eq.
642 643 644 645 646
rewrite Rabs_pos_eq.
split.
apply Rle_trans with (1 := proj1 Ex').
pattern x at 1 ; rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
647
apply ulp_ge_0.
648 649 650
exact H.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
651
apply ulp_ge_0.
652 653
rewrite H.
apply generic_format_bpow.
654
apply valid_exp.
655 656 657 658 659 660 661
destruct (Zle_or_lt ex (fexp ex)) ; trivial.
elim Rlt_not_le with (1 := Zx).
rewrite Fx.
replace (Ztrunc (scaled_mantissa beta fexp x)) with Z0.
rewrite F2R_0.
apply Rle_refl.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
662
rewrite canonic_exp_fexp with (1 := Ex).
663 664 665 666 667 668 669 670
destruct (mantissa_small_pos beta fexp x ex) ; trivial.
rewrite Ztrunc_floor.
apply sym_eq.
apply Zfloor_imp.
split.
now apply Rlt_le.
exact H2.
now apply Rlt_le.
671 672 673
now apply Rlt_le.
Qed.

674 675 676
Theorem generic_format_pred_pos :
  forall x, F x -> (0 < x)%R ->
  F (pred_pos x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
677
Proof.
678 679
intros x Fx Zx.
unfold pred_pos; case Req_bool_spec; intros H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
680 681
now apply generic_format_pred_aux2.
now apply generic_format_pred_aux1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
682 683
Qed.

684

685 686 687
Theorem generic_format_succ :
  forall x, F x ->
  F (succ x).
688
Proof.
689 690 691
intros x Fx.
unfold succ; case Rle_bool_spec; intros Zx.
destruct Zx as [Zx|Zx].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
692
now apply generic_format_succ_aux1.
693 694 695 696 697 698
rewrite <- Zx, Rplus_0_l.
apply generic_format_ulp_0.
apply generic_format_opp.
apply generic_format_pred_pos.
now apply generic_format_opp.
now apply Ropp_0_gt_lt_contravar.
699 700
Qed.

701 702 703 704 705 706 707 708 709
Theorem generic_format_pred :
  forall x, F x ->
  F (pred x).
Proof.
intros x Fx.
unfold pred.
apply generic_format_opp.
apply generic_format_succ.
now apply generic_format_opp.
710 711
Qed.

BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
712

713 714 715 716 717 718 719 720 721

Theorem pred_pos_lt_id :
  forall x, (x <> 0)%R ->
  (pred_pos x < x)%R.
Proof.
intros x Zx.
unfold pred_pos.
case Req_bool_spec; intros H.
(* *)
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
722 723 724 725 726
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
727 728 729 730 731 732 733
(* *)
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
rewrite ulp_neq_0; trivial.
apply bpow_gt_0.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
734
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
735

BOLDO Sylvie's avatar
BOLDO Sylvie committed
736
Theorem succ_gt_id :
737 738
  forall x, (x <> 0)%R ->
  (x < succ x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
739
Proof.
740 741 742 743 744 745 746 747 748 749
intros x Zx; unfold succ.
case Rle_bool_spec; intros Hx.
pattern x at 1; rewrite <- (Rplus_0_r x).
apply Rplus_lt_compat_l.
rewrite ulp_neq_0; trivial.
apply bpow_gt_0.
pattern x at 1; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
apply pred_pos_lt_id.
now auto with real.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
750
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
751

752 753 754 755 756 757 758 759

Theorem pred_lt_id :
  forall x,  (x <> 0)%R ->
  (pred x < x)%R.
Proof.
intros x Zx; unfold pred.
pattern x at 2; rewrite <- (Ropp_involutive x).
apply Ropp_lt_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
760
apply succ_gt_id.
761 762 763
now auto with real.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
764
Theorem succ_ge_id :
765 766 767 768 769
  forall x, (x <= succ x)%R.
Proof.
intros x; case (Req_dec x 0).
intros V; rewrite V.
unfold succ; rewrite Rle_bool_true;[idtac|now right].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
770
rewrite Rplus_0_l; apply ulp_ge_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
771
intros; left; now apply succ_gt_id.
772 773 774 775 776 777 778 779 780
Qed.


Theorem pred_le_id :
  forall x,  (pred x <= x)%R.
Proof.
intros x; unfold pred.
pattern x at 2; rewrite <- (Ropp_involutive x).
apply Ropp_le_contravar.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
781
apply succ_ge_id.
782 783 784 785 786 787
Qed.


Theorem pred_pos_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
788
Proof.
789 790 791 792 793 794 795 796
intros x Zx Fx.
unfold pred_pos.
case Req_bool_spec; intros H.
(* *)
apply Rle_0_minus.
rewrite H.
apply bpow_le.
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
797
rewrite ln_beta_bpow.
798 799 800 801
ring_simplify (ex - 1 + 1 - 1)%Z.
apply generic_format_bpow_inv with beta; trivial.
simpl in H.
rewrite <- H; assumption.
802
apply Rle_0_minus.
803
now apply ulp_le_id.
804 805
Qed.

806 807 808
Theorem pred_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred x)%R.
809
Proof.
810
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
811
rewrite pred_eq_pos.
812 813
now apply pred_pos_ge_0.
now left.
814 815
Qed.

816

BOLDO Sylvie's avatar
BOLDO Sylvie committed
817
Lemma pred_pos_plus_ulp_aux1 :
818
  forall x, (0 < x)%R -> F x ->
819
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
820
  ((x - ulp x) + ulp (x-ulp x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
821
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
822 823 824
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841
assert (H:(x <> 0)%R) by auto with real.
assert (H':(x <> bpow (canonic_exp beta fexp x))%R).
unfold canonic_exp; intros M.
case_eq (ln_beta beta x); intros ex Hex T.
assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
rewrite T; reflexivity.
rewrite Lex in *.
clear T; simpl in *; specialize (Hex H).
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
assert (ex-1 < fexp ex  < ex)%Z.
split ; apply (lt_bpow beta); rewrite <- M;[idtac|easy].
destruct (proj1 Hex);[trivial|idtac].
contradict Hx; auto with real.
omega.
rewrite 2!ulp_neq_0; try auto with real.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
842
unfold canonic_exp; apply f_equal.
843 844 845 846
case_eq (ln_beta beta x); intros ex Hex T.
assert (Lex:(ln_beta_val beta x (ln_beta beta x) = ex)%Z).
rewrite T; reflexivity.
rewrite Lex in *; simpl in *; clear T.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
847
specialize (Hex H).
848
apply sym_eq, ln_beta_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
849 850 851 852 853
rewrite Rabs_right.
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
split.
destruct Hex as ([H1|H1],H2).
854
apply Rle_trans with (x-ulp x)%R.
855
apply id_m_ulp_ge_bpow; trivial.
856 857 858
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold canonic_exp; now rewrite Lex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
859 860 861 862 863 864 865 866 867
contradict Hx; auto with real.
apply Rle_lt_trans with (2:=proj2 Hex).
rewrite <- Rplus_0_r.
apply Rplus_le_compat_l.
rewrite <- Ropp_0.
apply Ropp_le_contravar.
apply bpow_ge_0.
apply Rle_ge.
apply Rle_0_minus.
868 869 870 871
rewrite Fx.
unfold F2R, canonic_exp; simpl.
rewrite Lex.
pattern (bpow (fexp ex)) at 1; rewrite <- Rmult_1_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
872 873 874 875 876
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R (Zsucc 0)) by reflexivity.
apply Z2R_le.
apply Zlt_le_succ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
877
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
878 879 880
now rewrite <- Fx.
Qed.

881

BOLDO Sylvie's avatar
BOLDO Sylvie committed
882
Lemma pred_pos_plus_ulp_aux2 :
883
  forall x, (0 < x)%R -> F x ->
884
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
885 886 887
  x =  bpow (e - 1) ->
  (x - bpow (fexp (e-1)) <> 0)%R ->
  ((x - bpow (fexp (e-1))) + ulp (x - bpow (fexp (e-1))) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
888
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
889 890 891
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
892
assert (He:(fexp (e-1) <= e-1)%Z).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
893 894
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
895 896
case (Zle_lt_or_eq _ _ He); clear He; intros He.
(* *)
897 898
rewrite ulp_neq_0; trivial.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
899
unfold canonic_exp; apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
900 901 902 903 904 905 906
apply sym_eq.
apply ln_beta_unique.
rewrite Rabs_right.
split.
apply Rplus_le_reg_l with (bpow (fexp (e-1))).
ring_simplify.
apply Rle_trans with (bpow (e - 2) + bpow (e - 2))%R.
907
apply Rplus_le_compat; apply bpow_le; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
908 909 910 911 912
apply Rle_trans with (2*bpow (e - 2))%R;[right; ring|idtac].
apply Rle_trans with (bpow 1*bpow (e - 2))%R.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 2%R with (Z2R 2) by reflexivity.
913
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
914 915 916 917 918 919
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
920
rewrite <- bpow_plus.
921 922 923
replace (1+(e-2))%Z with (e-1)%Z by ring.
now right.
rewrite <- Rplus_0_r, Hxe.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
924 925 926 927
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
928 929 930 931 932 933 934
apply Rle_ge; apply Rle_0_minus.
rewrite Hxe.
apply bpow_le.
omega.
(* *)
contradict Zp.
rewrite Hxe, He; ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
935
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
936

BOLDO Sylvie's avatar
BOLDO Sylvie committed
937
Lemma pred_pos_plus_ulp_aux3 :
938 939 940 941 942 943 944 945 946 947 948 949 950 951
  forall x, (0 < x)%R -> F x ->
  let e := ln_beta_val beta x (ln_beta beta x) in
  x =  bpow (e - 1) ->
  (x - bpow (fexp (e-1)) = 0)%R ->
  (ulp 0 = x)%R.
Proof.
intros x Hx Fx e H1 H2.
assert (H3:(x = bpow (fexp (e - 1)))).
now apply Rminus_diag_uniq.
assert (H4: (fexp (e-1) = e-1)%Z).
apply bpow_inj with beta.
now rewrite <- H1.
unfold ulp; rewrite Req_bool_true; trivial.
case negligible_exp_spec.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
952
intros K.
953 954
specialize (K (e-1)%Z).
contradict K; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
955
intros n Hn.
956 957 958 959 960 961 962 963 964 965 966 967 968 969 970
rewrite H3; apply f_equal.
case (Zle_or_lt n (e-1)); intros H6.
apply valid_exp; omega.
apply sym_eq, valid_exp; omega.
Qed.




(** The following one is false for x = 0 in FTZ *)

Theorem pred_pos_plus_ulp :
  forall x, (0 < x)%R -> F x ->
  (pred_pos x + ulp (pred_pos x) = x)%R.
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
971
intros x Zx Fx.
972
unfold pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
973
case Req_bool_spec; intros H.
974 975
case (Req_EM_T (x - bpow (fexp (ln_beta_val beta x (ln_beta beta x) -1))) 0); intros H1.
rewrite H1, Rplus_0_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
976 977 978
now apply pred_pos_plus_ulp_aux3.
now apply pred_pos_plus_ulp_aux2.
now apply pred_pos_plus_ulp_aux1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
979 980
Qed.

981 982 983



984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175
(** Rounding x + small epsilon *)

Theorem ln_beta_plus_eps:
  forall x, (0 < x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  ln_beta beta (x + eps) = ln_beta beta x :> Z.
Proof.
intros x Zx Fx eps Heps.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rgt_not_eq _ _ Zx)).
apply ln_beta_unique.
rewrite Rabs_pos_eq.
rewrite Rabs_pos_eq in He.
split.
apply Rle_trans with (1 := proj1 He).
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with (x + ulp x)%R.
now apply Rplus_lt_compat_l.
pattern x at 1 ; rewrite Fx.
rewrite ulp_neq_0.
unfold F2R. simpl.
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
rewrite <- Z2R_plus.
change (F2R (Float beta (Ztrunc (scaled_mantissa beta fexp x) + 1) (canonic_exp beta fexp x)) <= bpow ex)%R.
apply F2R_p1_le_bpow.
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
now rewrite <- Fx.
now rewrite <- Fx.
now apply Rgt_not_eq.
now apply Rlt_le.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
apply Heps.
Qed.

Theorem round_DN_plus_eps_pos:
  forall x, (0 <= x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Zx Fx eps Heps.
destruct Zx as [Zx|Zx].
(* . 0 < x *)
pattern x at 2 ; rewrite Fx.
unfold round.
unfold scaled_mantissa. simpl.
unfold canonic_exp at 1 2.
rewrite ln_beta_plus_eps ; trivial.
apply (f_equal (fun m => F2R (Float beta m _))).
rewrite Ztrunc_floor.
apply Zfloor_imp.
split.
apply (Rle_trans _ _ _ (Zfloor_lb _)).
apply Rmult_le_compat_r.
apply bpow_ge_0.
pattern x at 1 ; rewrite <- Rplus_0_r.
now apply Rplus_le_compat_l.
apply Rlt_le_trans with ((x + ulp x) * bpow (- canonic_exp beta fexp x))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply Rplus_lt_compat_l.
rewrite Rmult_plus_distr_r.
rewrite Z2R_plus.
apply Rplus_le_compat.
pattern x at 1 3 ; rewrite Fx.
unfold F2R. simpl.
rewrite Rmult_assoc.
rewrite <- bpow_plus.
rewrite Zplus_opp_r.
rewrite Rmult_1_r.
rewrite Zfloor_Z2R.
apply Rle_refl.
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
rewrite <- bpow_plus.
rewrite Zplus_opp_r.
apply Rle_refl.
apply Rmult_le_pos.
now apply Rlt_le.
apply bpow_ge_0.
(* . x=0 *)
rewrite <- Zx, Rplus_0_l; rewrite <- Zx in Heps.
case (proj1 Heps); intros P.
unfold round, scaled_mantissa, canonic_exp.
revert Heps; unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros _ (H1,H2).
absurd (0 < 0)%R; auto with real.
now apply Rle_lt_trans with (1:=H1).
intros n Hn H.
assert (fexp (ln_beta beta eps) = fexp n).
apply valid_exp; try assumption.
assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=proj2 H).
destruct (ln_beta beta eps) as (e,He).
simpl; rewrite Rabs_pos_eq in He.
now apply He, Rgt_not_eq.
now left.
replace (Zfloor (eps * bpow (- fexp (ln_beta beta eps)))) with 0%Z.
unfold F2R; simpl; ring.
apply sym_eq, Zfloor_imp.
split.
apply Rmult_le_pos.
now left.
apply bpow_ge_0.
apply Rmult_lt_reg_r with (bpow (fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_plus.
rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
simpl; rewrite Rmult_1_l, Rmult_1_r.
apply H.
rewrite <- P, round_0; trivial.
apply valid_rnd_DN.
Qed.


Theorem round_UP_plus_eps_pos :
  forall x, (0 <= x)%R -> F x ->
  forall eps, (0 < eps <= ulp x)%R ->
  round beta fexp Zceil (x + eps) = (x + ulp x)%R.
Proof with auto with typeclass_instances.
intros x Zx Fx eps.
case Zx; intros Zx1.
(* . 0 < x *)
intros (Heps1,[Heps2|Heps2]).
assert (Heps: (0 <= eps < ulp x)%R).
split.
now apply Rlt_le.
exact Heps2.
assert (Hd := round_DN_plus_eps_pos x Zx Fx eps Heps).
rewrite round_UP_DN_ulp.
rewrite Hd.
rewrite 2!ulp_neq_0.
unfold canonic_exp.
now rewrite ln_beta_plus_eps.
now apply Rgt_not_eq.
now apply Rgt_not_eq, Rplus_lt_0_compat.
intros Fs.
rewrite round_generic in Hd...
apply Rgt_not_eq with (2 := Hd).
pattern x at 2 ; rewrite <- Rplus_0_r.
now apply Rplus_lt_compat_l.
rewrite Heps2.
apply round_generic...
now apply generic_format_succ_aux1.
(* . x=0 *)
rewrite <- Zx1, 2!Rplus_0_l.
intros Heps.
case (proj2 Heps).
unfold round, scaled_mantissa, canonic_exp.
unfold ulp.
rewrite Req_bool_true; trivial.
case negligible_exp_spec.
intros H2.
intros J; absurd (0 < 0)%R; auto with real.
apply Rlt_trans with eps; try assumption; apply Heps.
intros n Hn H.
assert (fexp (ln_beta beta eps) = fexp n).
apply valid_exp; try assumption.
assert(ln_beta beta eps-1 < fexp n)%Z;[idtac|omega].
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=H).
destruct (ln_beta beta eps) as (e,He).
simpl; rewrite Rabs_pos_eq in He.
now apply He, Rgt_not_eq.
now left.
replace (Zceil (eps * bpow (- fexp (ln_beta beta eps)))) with 1%Z.
unfold F2R; simpl; rewrite H0; ring.
apply sym_eq, Zceil_imp.
split.
simpl; apply Rmult_lt_0_compat.
apply Heps.
apply bpow_gt_0.
apply Rmult_le_reg_r with (bpow (fexp n)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_plus.
rewrite H0; ring_simplify (-fexp n + fexp n)%Z.
simpl; rewrite Rmult_1_l, Rmult_1_r.
now left.
intros P; rewrite P.
apply round_generic...
apply generic_format_ulp_0.
Qed.


Theorem round_UP_pred_plus_eps_pos :
1176
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1177
  forall eps, (0 < eps <= ulp (pred x) )%R ->
1178
  round beta fexp Zceil (pred x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1179 1180
Proof.
intros x Hx Fx eps Heps.
1181
rewrite round_UP_plus_eps_pos; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1182
rewrite pred_eq_pos.
1183 1184 1185
apply pred_pos_plus_ulp; trivial.
now left.
now apply pred_ge_0.
1186