Fcore_ulp.v 59.7 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
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 *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
87 88 89 90 91 92
(** Now includes a nice ulp(0): ulp(0) is now 0 when there is no minimal
   exponent, such as in FLX, and beta^(fexp n) when there is a n such
   that n <= fexp n. For instance, the value of ulp(O) is then
   beta^emin in FIX and FLT. The main lemma to use is ulp_neq_0 that
   is equivalent to the previous "unfold ulp" provided the value is
   not zero. *)
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107

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
108

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

111 112 113 114 115
Theorem ulp_opp :
  forall x, ulp (- x) = ulp x.
Proof.
intros x.
unfold ulp.
116 117 118 119
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
120
now rewrite canonic_exp_opp.
121
intros H2; apply H1; rewrite H2; ring.
122 123 124 125 126 127
Qed.

Theorem ulp_abs :
  forall x, ulp (Rabs x) = ulp x.
Proof.
intros x.
128 129 130 131
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
132
now rewrite canonic_exp_abs.
133 134 135
now apply Rabs_no_R0.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
136
Theorem ulp_ge_0:
137 138 139 140 141 142 143
  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.
144 145
Qed.

146

147
Theorem ulp_le_id:
148
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
149
    (0 < x)%R ->
150
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
151 152 153 154 155
    (ulp x <= x)%R.
Proof.
intros x Zx Fx.
rewrite <- (Rmult_1_l (ulp x)).
pattern x at 2; rewrite Fx.
156 157 158
rewrite ulp_neq_0.
2: now apply Rgt_not_eq.
unfold F2R; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
159 160 161 162 163
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
164
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
165 166 167 168
now rewrite <- Fx.
Qed.

Theorem ulp_le_abs:
169
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
170
    (x <> 0)%R ->
171
    F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
172 173 174
    (ulp x <= Rabs x)%R.
Proof.
intros x Zx Fx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
175
rewrite <- ulp_abs.
176
apply ulp_le_id.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
177 178
now apply Rabs_pos_lt.
now apply generic_format_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
179 180
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
181 182 183

(* was ulp_DN_UP *)
Theorem round_UP_DN_ulp :
184
  forall x, ~ F x ->
185
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
186
Proof.
187
intros x Fx.
188 189
rewrite ulp_neq_0.
unfold round. simpl.
190 191
unfold F2R. simpl.
rewrite Zceil_floor_neq.
192
rewrite Z2R_plus. simpl.
193
ring.
194
intros H.
195
apply Fx.
196
unfold generic_format, F2R. simpl.
197 198 199
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
200
now rewrite scaled_mantissa_mult_bpow.
201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
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
230 231
intros _; apply generic_format_0.
intros n H1.
232 233 234 235 236 237 238 239 240 241
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
242
intros H1 _.
243
apply generic_format_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
244 245
specialize (H1 (e+1)%Z); omega.
intros n H1 H2.
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 286 287 288 289 290 291
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
292 293
case negligible_exp_spec'.
intros (H1,H2); rewrite H1; apply ulp_ge_0.
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 368 369 370 371 372 373
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
374
Theorem pred_eq_pos:
375 376 377 378 379 380 381 382 383 384 385 386 387 388 389
  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
390
Theorem succ_eq_pos:
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 416 417 418 419 420 421
  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.



422

423 424
(** pred and succ are in the format *)

425 426 427
(* 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 :
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 459 460 461 462 463 464
  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
465 466
Qed.

467 468
(* was succ_le_bpow *)
Theorem id_p_ulp_le_bpow :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
469 470 471 472 473 474
  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.
475 476
rewrite ulp_neq_0.
unfold F2R. simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
477
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478 479
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
480
rewrite <- Z2R_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
481
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
482
apply F2R_p1_le_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
483
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
484 485
now rewrite <- Fx.
now rewrite <- Fx.
486
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
487 488
Qed.

489 490


BOLDO Sylvie's avatar
BOLDO Sylvie committed
491
Lemma generic_format_pred_aux1:
492
  forall x, (0 < x)%R -> F x ->
493 494
  x <> bpow (ln_beta beta x - 1) ->
  F (x - ulp x).
495
Proof.
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
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.
522 523
rewrite Rabs_pos_eq.
split.
524
apply id_m_ulp_ge_bpow; trivial.
525 526 527 528 529 530 531 532 533 534 535 536
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
537
apply ulp_ge_0.
538 539 540 541 542 543 544 545 546 547
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
548
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
549 550 551 552 553
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
554 555
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
556
Lemma generic_format_pred_aux2 :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
557
  forall x, (0 < x)%R -> F x ->
558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584
  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.
585
split.
586 587 588 589 590 591
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.
592 593
apply Rmult_le_compat_r.
apply bpow_ge_0.
594 595 596 597 598 599 600 601
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.
602
rewrite <- bpow_plus.
603 604 605 606 607 608 609 610 611 612 613 614 615 616 617
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.
618 619
Qed.

620

BOLDO Sylvie's avatar
BOLDO Sylvie committed
621
Theorem generic_format_succ_aux1 :
622 623 624 625 626 627 628 629
  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'.
630
destruct (id_p_ulp_le_bpow x ex) ; try easy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
631
unfold generic_format, scaled_mantissa, canonic_exp.
632 633
rewrite ln_beta_unique with beta (x + ulp x)%R ex.
pattern x at 1 3 ; rewrite Fx.
634 635
rewrite ulp_neq_0.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
636
rewrite canonic_exp_fexp with (1 := Ex).
637
unfold F2R. simpl.
638 639
rewrite Rmult_plus_distr_r.
rewrite Rmult_assoc.
640
rewrite <- bpow_plus, Zplus_opp_r, Rmult_1_r.
641
change (bpow 0) with (Z2R 1).
642
rewrite <- Z2R_plus.
643
rewrite Ztrunc_Z2R.
644
rewrite Z2R_plus.
645 646
rewrite Rmult_plus_distr_r.
now rewrite Rmult_1_l.
647
now apply Rgt_not_eq.
648 649 650 651 652
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
653
apply ulp_ge_0.
654 655 656
exact H.
apply Rplus_le_le_0_compat.
now apply Rlt_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
657
apply ulp_ge_0.
658 659
rewrite H.
apply generic_format_bpow.
660
apply valid_exp.
661 662 663 664 665 666 667
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
668
rewrite canonic_exp_fexp with (1 := Ex).
669 670 671 672 673 674 675 676
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.
677 678 679
now apply Rlt_le.
Qed.

680 681 682
Theorem generic_format_pred_pos :
  forall x, F x -> (0 < x)%R ->
  F (pred_pos x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
683
Proof.
684 685
intros x Fx Zx.
unfold pred_pos; case Req_bool_spec; intros H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
686 687
now apply generic_format_pred_aux2.
now apply generic_format_pred_aux1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
688 689
Qed.

690

691 692 693
Theorem generic_format_succ :
  forall x, F x ->
  F (succ x).
694
Proof.
695 696 697
intros x Fx.
unfold succ; case Rle_bool_spec; intros Zx.
destruct Zx as [Zx|Zx].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
698
now apply generic_format_succ_aux1.
699 700 701 702 703 704
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.
705 706
Qed.

707 708 709 710 711 712 713 714 715
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.
716 717
Qed.

BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
718

719 720 721 722 723 724 725 726 727

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
728 729 730 731 732
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
733 734 735 736 737 738 739
(* *)
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
740
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
741

BOLDO Sylvie's avatar
BOLDO Sylvie committed
742
Theorem succ_gt_id :
743 744
  forall x, (x <> 0)%R ->
  (x < succ x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
745
Proof.
746 747 748 749 750 751 752 753 754 755
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
756
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
757

758 759 760 761 762 763 764 765

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
766
apply succ_gt_id.
767 768 769
now auto with real.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
770
Theorem succ_ge_id :
771 772 773 774 775
  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
776
rewrite Rplus_0_l; apply ulp_ge_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
777
intros; left; now apply succ_gt_id.
778 779 780 781 782 783 784 785 786
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
787
apply succ_ge_id.
788 789 790 791 792 793
Qed.


Theorem pred_pos_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
794
Proof.
795 796 797 798 799 800 801 802
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.
803
rewrite ln_beta_bpow.
804 805 806 807
ring_simplify (ex - 1 + 1 - 1)%Z.
apply generic_format_bpow_inv with beta; trivial.
simpl in H.
rewrite <- H; assumption.
808
apply Rle_0_minus.
809
now apply ulp_le_id.
810 811
Qed.

812 813 814
Theorem pred_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred x)%R.
815
Proof.
816
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
817
rewrite pred_eq_pos.
818 819
now apply pred_pos_ge_0.
now left.
820 821
Qed.

822

BOLDO Sylvie's avatar
BOLDO Sylvie committed
823
Lemma pred_pos_plus_ulp_aux1 :
824
  forall x, (0 < x)%R -> F x ->
825
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
826
  ((x - ulp x) + ulp (x-ulp x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
827
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
828 829 830
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847
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
848
unfold canonic_exp; apply f_equal.
849 850 851 852
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
853
specialize (Hex H).
854
apply sym_eq, ln_beta_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
855 856 857 858 859
rewrite Rabs_right.
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
split.
destruct Hex as ([H1|H1],H2).
860
apply Rle_trans with (x-ulp x)%R.
861
apply id_m_ulp_ge_bpow; trivial.
862 863 864
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold canonic_exp; now rewrite Lex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
865 866 867 868 869 870 871 872 873
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.
874 875 876 877
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
878 879 880 881 882
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
883
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
884 885 886
now rewrite <- Fx.
Qed.

887

BOLDO Sylvie's avatar
BOLDO Sylvie committed
888
Lemma pred_pos_plus_ulp_aux2 :
889
  forall x, (0 < x)%R -> F x ->
890
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
891 892 893
  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
894
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
895 896 897
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
898
assert (He:(fexp (e-1) <= e-1)%Z).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
899 900
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
901 902
case (Zle_lt_or_eq _ _ He); clear He; intros He.
(* *)
903 904
rewrite ulp_neq_0; trivial.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
905
unfold canonic_exp; apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
906 907 908 909 910 911 912
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.
913
apply Rplus_le_compat; apply bpow_le; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
914 915 916 917 918
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.
919
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
920 921 922 923 924 925
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
926
rewrite <- bpow_plus.
927 928 929
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
930 931 932 933
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
934 935 936 937 938 939 940
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
941
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
942

BOLDO Sylvie's avatar
BOLDO Sylvie committed
943
Lemma pred_pos_plus_ulp_aux3 :
944 945 946 947 948 949 950 951 952 953 954 955 956 957
  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
958
intros K.
959 960
specialize (K (e-1)%Z).
contradict K; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
961
intros n Hn.
962 963 964 965 966 967 968 969 970 971 972 973 974 975 976
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
977
intros x Zx Fx.
978
unfold pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
979
case Req_bool_spec; intros H.
980 981
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
982 983 984
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
985 986
Qed.

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 1176 1177 1178 1179 1180 1181
(** 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 :
1182
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1183
  forall eps, (0 < eps <= ulp (pred x) )%R ->
1184
  round beta fexp Zceil (pred x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1185 1186
Proof.
intros x Hx Fx eps Heps.
1187
rewrite round_UP_plus_eps_pos; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1188
rewrite pred_eq_pos.
1189 1190 1191
apply pred_pos_plus_ulp; trivial.
now left.
now apply pred_ge_0.
1192
apply generic_format_pred; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1193
Qed.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
1194

1195 1196
Theorem round_DN_minus_eps_pos :
  forall x,  (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1197
  forall eps, (0 < eps <= ulp (pred x))%R ->
1198
  round beta fexp Zfloor (x - eps) = pred x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1199
Proof.
1200
intros x Hpx Fx eps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1201
rewrite pred_eq_pos;[intros Heps|now left].
1202 1203
replace (x-eps)%R with (pred_pos x + (ulp (pred_pos x)-eps))%R.
2: pattern x at 3; rewrite <- (pred_pos_plus_ulp x); trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1204
2: ring.
1205
rewrite round_DN_plus_eps_pos; trivial.
1206 1207
now apply pred_pos_ge_0.
now apply generic_format_pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1208 1209 1210 1211 1212 1213 1214 1215 1216
split.
apply Rle_0_minus.
now apply Heps.
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
now apply Heps.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1217

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1218

1219 1220
Theorem round_DN_plus_eps:
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1221 1222
  forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1223 1224 1225 1226 1227 1228
  round beta fexp Zfloor (x + eps) = x.
Proof.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
apply round_DN_plus_eps_pos; try assumption.
split; try apply Heps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1229 1230
rewrite Rle_bool_true in Heps; trivial.
now apply Heps.
1231
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1232
rewrite Rle_bool_false in Heps; trivial.
1233 1234 1235 1236 1237 1238 1239 1240 1241 1242
rewrite <- (Ropp_involutive (x+eps)).
pattern x at 2; rewrite <- (Ropp_involutive x).
rewrite round_DN_opp.
apply f_equal.
replace (-(x+eps))%R with (pred (-x) + (ulp (pred (-x)) - eps))%R.
rewrite round_UP_pred_plus_eps_pos; try reflexivity.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
split.
apply Rplus_lt_reg_l with eps; ring_simplify.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1243
apply Heps.
1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255
apply Rplus_le_reg_l with (eps-ulp (pred (- x)))%R; ring_simplify.
apply Heps.
unfold pred.
rewrite Ropp_involutive.
unfold succ; rewrite Rle_bool_false; try assumption.
rewrite Ropp_involutive; unfold Rminus.
rewrite <- Rplus_assoc, pred_pos_plus_ulp.
ring.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1256

1257 1258
Theorem round_UP_plus_eps :
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1259 1260
  forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1261 1262 1263 1264 1265
  round beta fexp Zceil (x + eps) = (succ x)%R.
Proof with auto with typeclass_instances.
intros x Fx eps Heps.
case (Rle_or_lt 0 x); intros Zx.
rewrite succ_eq_pos; try assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed