Fcore_ulp.v 55.2 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 416 417
  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.



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

418
Theorem pred_ge_bpow : (* TODO x <> ulp 0 (?) , renommer ? après pred ?*)
419 420 421 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
  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
456 457
Qed.

458
Theorem succ_le_bpow : (* TODO mettre succ ? *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
459 460 461 462 463 464
  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.
465 466
rewrite ulp_neq_0.
unfold F2R. simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
467
pattern (bpow (canonic_exp beta fexp x)) at 2 ; rewrite <- Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
468 469
rewrite <- Rmult_plus_distr_r.
change 1%R with (Z2R 1).
470
rewrite <- Z2R_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
471
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
472
apply F2R_p1_le_bpow.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
473
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
474 475
now rewrite <- Fx.
now rewrite <- Fx.
476
now apply Rgt_not_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
477 478
Qed.

479 480


BOLDO Sylvie's avatar
BOLDO Sylvie committed
481
Lemma generic_format_pred_aux1:
482
  forall x, (0 < x)%R -> F x ->
483 484
  x <> bpow (ln_beta beta x - 1) ->
  F (x - ulp x).
485
Proof.
486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511
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.
512 513
rewrite Rabs_pos_eq.
split.
514 515 516 517 518 519 520 521 522 523 524 525 526
apply pred_ge_bpow; trivial.
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
527
apply ulp_ge_0.
528 529 530 531 532 533 534 535 536 537
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
538
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
539 540 541 542 543
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
544 545
Qed.

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

610

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

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

680

681 682 683
Theorem generic_format_succ :
  forall x, F x ->
  F (succ x).
684
Proof.
685 686 687
intros x Fx.
unfold succ; case Rle_bool_spec; intros Zx.
destruct Zx as [Zx|Zx].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
688
now apply generic_format_succ_aux1.
689 690 691 692 693 694
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.
695 696
Qed.

697 698 699 700 701 702 703 704 705
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.
706 707
Qed.

BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
708

709
(** Rounding x + small epsilon *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
710

711
Theorem ln_beta_plus_eps:
712
  forall x, (0 < x)%R -> F x ->
713 714
  forall eps, (0 <= eps < ulp x)%R ->
  ln_beta beta (x + eps) = ln_beta beta x :> Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
715
Proof.
716 717 718 719 720
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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
721
rewrite Rabs_pos_eq.
722
rewrite Rabs_pos_eq in He.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
723
split.
724 725 726 727 728 729 730 731 732 733 734 735 736 737
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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
738
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
739 740 741 742 743 744 745
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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
746 747
Qed.

748 749 750 751
Theorem round_DN_plus_eps :
  forall x, (0 <= x)%R -> F x ->
  forall eps, (0 <= eps < ulp x)%R ->
  round beta fexp Zfloor (x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
752
Proof.
753 754 755 756 757 758 759 760 761 762 763
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.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
764
split.
765
apply (Rle_trans _ _ _ (Zfloor_lb _)).
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
766 767
apply Rmult_le_compat_r.
apply bpow_ge_0.
768 769 770 771 772 773 774 775 776 777 778 779
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.
780
rewrite <- bpow_plus.
781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
800
intros _ (H1,H2).
801
absurd (0 < 0)%R; auto with real.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
802 803
now apply Rle_lt_trans with (1:=H1).
intros n Hn H.
804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831
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.



832
Theorem round_UP_plus_eps : (* TODO succ ! ou aux...*)
833 834 835 836 837 838 839 840 841 842 843 844 845
  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 x Zx Fx eps Heps).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
846
rewrite round_UP_DN_ulp.
847 848 849 850 851 852 853 854 855 856 857 858 859
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...
BOLDO Sylvie's avatar
BOLDO Sylvie committed
860
now apply generic_format_succ_aux1.
861 862 863 864 865 866 867 868
(* . 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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
869
intros H2.
870 871
intros J; absurd (0 < 0)%R; auto with real.
apply Rlt_trans with eps; try assumption; apply Heps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
872
intros n Hn H.
873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907
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 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
908 909 910 911 912
rewrite <- Rplus_0_r.
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
913 914 915 916 917 918 919
(* *)
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
920
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
921

922
Theorem id_lt_succ : (* TODO succ_gt_id *)
923 924
  forall x, (x <> 0)%R ->
  (x < succ x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
925
Proof.
926 927 928 929 930 931 932 933 934 935
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
936
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
937

938 939 940 941 942 943 944 945 946 947 948 949

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.
apply id_lt_succ.
now auto with real.
Qed.

950
Theorem id_le_succ :(* TODO succ_ge_id *)
951 952 953 954 955
  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
956
rewrite Rplus_0_l; apply ulp_ge_0.
957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973
intros; left; now apply id_lt_succ.
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.
apply id_le_succ.
Qed.


Theorem pred_pos_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred_pos x)%R.
974
Proof.
975 976 977 978 979 980 981 982
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.
983
rewrite ln_beta_bpow.
984 985 986 987
ring_simplify (ex - 1 + 1 - 1)%Z.
apply generic_format_bpow_inv with beta; trivial.
simpl in H.
rewrite <- H; assumption.
988
apply Rle_0_minus.
989
now apply ulp_le_id.
990 991
Qed.

992 993 994
Theorem pred_ge_0 :
  forall x,
  (0 < x)%R -> F x -> (0 <= pred x)%R.
995
Proof.
996
intros x Zx Fx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
997
rewrite pred_eq_pos.
998 999
now apply pred_pos_ge_0.
now left.
1000 1001
Qed.

1002

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1003
Lemma pred_pos_plus_ulp_aux1 :
1004
  forall x, (0 < x)%R -> F x ->
1005
  x <> bpow (ln_beta beta x - 1) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1006
  ((x - ulp x) + ulp (x-ulp x) = x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1007
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1008 1009 1010
intros x Zx Fx Hx.
replace (ulp (x - ulp x)) with (ulp x).
ring.
1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027
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
1028
unfold canonic_exp; apply f_equal.
1029 1030 1031 1032
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
1033
specialize (Hex H).
1034
apply sym_eq, ln_beta_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1035 1036 1037 1038 1039
rewrite Rabs_right.
rewrite Rabs_right in Hex.
2: apply Rle_ge; apply Rlt_le; easy.
split.
destruct Hex as ([H1|H1],H2).
1040
apply Rle_trans with (x-ulp x)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1041
apply pred_ge_bpow; trivial.
1042 1043 1044
rewrite ulp_neq_0; trivial.
rewrite ulp_neq_0; trivial.
right; unfold canonic_exp; now rewrite Lex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1045 1046 1047 1048 1049 1050 1051 1052 1053
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.
1054 1055 1056 1057
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
1058 1059 1060 1061 1062
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
1063
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1064 1065 1066
now rewrite <- Fx.
Qed.

1067

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1068
Lemma pred_pos_plus_ulp_aux2 :
1069
  forall x, (0 < x)%R -> F x ->
1070
  let e := ln_beta_val beta x (ln_beta beta x) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1071 1072 1073
  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
1074
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1075 1076 1077
intros x Zx Fx e Hxe Zp.
replace (ulp (x - bpow (fexp (e - 1)))) with (bpow (fexp (e - 1))).
ring.
1078
assert (He:(fexp (e-1) <= e-1)%Z).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1079 1080
apply generic_format_bpow_inv with beta; trivial.
rewrite <- Hxe; assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1081 1082
case (Zle_lt_or_eq _ _ He); clear He; intros He.
(* *)
1083 1084
rewrite ulp_neq_0; trivial.
apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1085
unfold canonic_exp; apply f_equal.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1086 1087 1088 1089 1090 1091 1092
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.
1093
apply Rplus_le_compat; apply bpow_le; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1094 1095 1096 1097 1098
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.
1099
replace (bpow 1) with (Z2R beta).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1100 1101 1102 1103 1104 1105
apply Z2R_le.
apply <- Zle_is_le_bool.
now destruct beta.
simpl.
unfold Zpower_pos; simpl.
now rewrite Zmult_1_r.
1106
rewrite <- bpow_plus.
1107 1108 1109
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
1110 1111 1112 1113
apply Rplus_lt_compat_l.
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply bpow_gt_0.
1114 1115 1116 1117 1118 1119 1120
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
1121
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1122

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1123
Lemma pred_pos_plus_ulp_aux3 :
1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137
  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
1138
intros K.
1139 1140
specialize (K (e-1)%Z).
contradict K; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1141
intros n Hn.
1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156
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
1157
intros x Zx Fx.
1158
unfold pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1159
case Req_bool_spec; intros H.
1160 1161
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
1162 1163 1164
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
1165 1166
Qed.

1167 1168 1169 1170 1171



Theorem round_UP_pred_plus_eps :
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1172
  forall eps, (0 < eps <= ulp (pred x) )%R ->
1173
  round beta fexp Zceil (pred x + eps) = x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1174 1175
Proof.
intros x Hx Fx eps Heps.
1176
rewrite round_UP_plus_eps; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1177
rewrite pred_eq_pos.
1178 1179 1180
apply pred_pos_plus_ulp; trivial.
now left.
now apply pred_ge_0.
1181
apply generic_format_pred; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1182
Qed.
BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
1183

1184 1185
Theorem round_DN_minus_eps :
  forall x, (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1186
  forall eps, (0 < eps <= ulp (pred x))%R ->
1187
  round beta fexp Zfloor (x - eps) = pred x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1188
Proof.
1189
intros x Hpx Fx eps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1190
rewrite pred_eq_pos;[intros Heps|now left].
1191 1192
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
1193
2: ring.
1194 1195 1196
rewrite round_DN_plus_eps; trivial.
now apply pred_pos_ge_0.
now apply generic_format_pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1197 1198 1199 1200 1201 1202 1203 1204 1205
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
1206

1207
Lemma le_pred_pos_lt :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1208 1209
  forall x y,
  F x -> F y ->
1210 1211
  (0 <= x < y)%R ->
  (x <= pred_pos y)%R.
1212
Proof with auto with typeclass_instances.
1213 1214
intros x y Fx Fy H.
case (proj1 H); intros V.
1215
assert (Zy:(0 < y)%R).
1216
apply Rle_lt_trans with (1:=proj1 H).
1217
apply H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1218
(* *)