Fcore_ulp.v 58.4 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
(** 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.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
38
Proof.
39 40 41 42 43 44 45 46 47 48 49 50 51 52
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
apply Rmult_le_compat_r.
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
161
apply (Z2R_le (Zsucc 0)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
162
apply Zlt_le_succ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
163
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
164 165 166 167
now rewrite <- Fx.
Qed.

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

BOLDO Sylvie's avatar
BOLDO Sylvie committed
180 181 182

(* was ulp_DN_UP *)
Theorem round_UP_DN_ulp :
183
  forall x, ~ F x ->
184
  round beta fexp Zceil x = (round beta fexp Zfloor x + ulp x)%R.
185
Proof.
186
intros x Fx.
187 188
rewrite ulp_neq_0.
unfold round. simpl.
189 190
unfold F2R. simpl.
rewrite Zceil_floor_neq.
191
rewrite Z2R_plus. simpl.
192
ring.
193
intros H.
194
apply Fx.
195
unfold generic_format, F2R. simpl.
196 197 198
rewrite <- H.
rewrite Ztrunc_Z2R.
rewrite H.
199
now rewrite scaled_mantissa_mult_bpow.
200 201 202 203 204 205 206 207
intros V; apply Fx.
rewrite V.
apply generic_format_0.
Qed.


Theorem ulp_bpow :
  forall e, ulp (bpow e) = bpow (fexp (e + 1)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
208
Proof.
209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
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
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.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
273
Proof.
274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292
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
293 294
case negligible_exp_spec'.
intros (H1,H2); rewrite H1; apply ulp_ge_0.
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 374
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
375
Theorem pred_eq_pos:
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390
  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
391
Theorem succ_eq_pos:
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 422
  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.



423

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

426 427 428
(* 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 :
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 465
  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
466 467
Qed.

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

490 491


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

BOLDO Sylvie's avatar
BOLDO Sylvie committed
557
Lemma generic_format_pred_aux2 :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
558
  forall x, (0 < x)%R -> F x ->
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 585
  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.
586
split.
587 588 589 590 591 592
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.
593 594
apply Rmult_le_compat_r.
apply bpow_ge_0.
595 596 597 598 599 600 601 602
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.
603
rewrite <- bpow_plus.
604 605 606 607 608 609 610 611 612 613 614 615 616 617 618
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.
619 620
Qed.

621

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

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

691

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

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

BOLDO Sylvie's avatar
Fpred  
BOLDO Sylvie committed
719

720 721 722 723 724 725 726 727 728

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

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

759 760 761 762 763 764 765 766

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

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


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

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

823

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

888

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

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

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

1196 1197
Theorem round_DN_minus_eps_pos :
  forall x,  (0 < x)%R -> F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1198
  forall eps, (0 < eps <= ulp (pred x))%R ->
1199
  round beta fexp Zfloor (x - eps) = pred x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1200
Proof.
1201
intros x Hpx Fx eps.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1202
rewrite pred_eq_pos;[intros Heps|now left].
1203 1204
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
1205
2: ring.
1206
rewrite round_DN_plus_eps_pos; trivial.
1207 1208
now apply pred_pos_ge_0.
now apply generic_format_pred_pos.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1209 1210 1211 1212 1213 1214 1215 1216 1217
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
1218

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1219

1220 1221
Theorem round_DN_plus_eps:
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1222 1223
  forall eps, (0 <= eps < if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1224 1225 1226 1227 1228 1229
  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
1230 1231
rewrite Rle_bool_true in Heps; trivial.
now apply Heps.
1232
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1233
rewrite Rle_bool_false in Heps; trivial.
1234 1235 1236 1237 1238 1239 1240 1241 1242 1243
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
1244
apply Heps.
1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256
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
1257

1258 1259
Theorem round_UP_plus_eps :
  forall x, F x ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1260 1261
  forall eps, (0 < eps <= if (Rle_bool 0 x) then (ulp x)
                                     else (ulp (pred (-x))))%R ->
1262 1263 1264 1265 1266
  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
1267 1268
rewrite Rle_bool_true in Heps; trivial.
apply round_UP_plus_eps_pos; assumption.
1269
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1270
rewrite Rle_bool_false in Heps; trivial.
1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283
rewrite <- (Ropp_involutive (x+eps)).
rewrite <- (Ropp_involutive (succ x)).
rewrite round_UP_opp.
apply f_equal.
replace (-(x+eps))%R with (-succ x + (-eps + ulp (pred (-x))))%R.
apply round_DN_plus_eps_pos.
rewrite <- pred_opp.
apply pred_ge_0.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
now apply generic_format_opp, generic_format_succ.
split.
apply Rplus_le_reg_l with eps; ring_simplify.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1284
apply Heps.
1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298
unfold pred; rewrite Ropp_involutive.
apply Rplus_lt_reg_l with (eps-ulp (- succ x))%R; ring_simplify.
apply Heps.
unfold succ; rewrite Rle_bool_false; try assumption.
apply trans_eq with (-x +-eps)%R;[idtac|ring].
pattern (-x)%R at 3; rewrite <- (pred_pos_plus_ulp (-x)).
rewrite pred_eq_pos.
ring.
left; now apply Ropp_0_gt_lt_contravar.
now apply Ropp_0_gt_lt_contravar.
now apply generic_format_opp.
Qed.


1299
Lemma le_pred_pos_lt :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1300 1301
  forall x y,
  F x -> F y ->
1302 1303
  (0 <= x < y)%R ->
  (x <= pred_pos y)%R.
1304
Proof with auto with typeclass_instances.
1305 1306
intros x y Fx Fy H.
case (proj1 H); intros V.
1307
assert (Zy:(0 < y)%R).
1308
apply Rle_lt_trans with (1:=proj1 H).
1309
apply H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1310
(* *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1311 1312
assert (Zp: (0 < pred y)%R).
assert (Zp:(0 <= pred y)%R).
1313
apply pred_ge_0 ; trivial.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1314 1315
destruct Zp; trivial.
generalize H0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1316
rewrite pred_eq_pos;[idtac|now left].
1317
unfold pred_pos.
1318
destruct (ln_beta beta y) as (ey,Hey); simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1319 1320 1321
case Req_bool_spec; intros Hy2.
(* . *)
intros Hy3.
1322
assert (ey-1 = fexp (ey -1))%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1323
apply bpow_inj with beta.
1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341
rewrite <- Hy2, <- Rplus_0_l, Hy3.
ring.
assert (Zx: (x <> 0)%R).
now apply Rgt_not_eq.
destruct (ln_beta beta x) as (ex,Hex).
specialize (Hex Zx).
assert (ex <= ey)%Z.
apply bpow_lt_bpow with beta.
apply Rle_lt_trans with (1:=proj1 Hex).
apply Rlt_trans with (Rabs y).
rewrite 2!Rabs_right.
apply H.
now apply Rgt_ge.
now apply Rgt_ge.
apply Hey.
now apply Rgt_not_eq.
case (Zle_lt_or_eq _ _ H2); intros Hexy.
assert (fexp ex = fexp (ey-1))%Z.
1342
apply valid_exp.
1343 1344 1345 1346 1347 1348
omega.
rewrite <- H1.
omega.
absurd (0 < Ztrunc (scaled_mantissa beta fexp x) < 1)%Z.
omega.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1349
apply F2R_gt_0_reg with beta (canonic_exp beta fexp x).
1350
now rewrite <- Fx.
1351
apply lt_Z2R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1352
apply Rmult_lt_reg_r with (bpow (canonic_exp beta fexp x)).
1353 1354
apply bpow_gt_0.
replace (Z2R (Ztrunc (scaled_mantissa beta fexp x)) *
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1355
 bpow (canonic_exp beta fexp x))%R with x.
1356
rewrite Rmult_1_l.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1357
unfold canonic_exp.
1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373
rewrite ln_beta_unique with beta x ex.
rewrite H3,<-H1, <- Hy2.
apply H.
exact Hex.
absurd (y <= x)%R.
now apply Rlt_not_le.
rewrite Rabs_right in Hex.
apply Rle_trans with (2:=proj1 Hex).
rewrite Hexy, Hy2.
now apply Rle_refl.
now apply Rgt_ge.
(* . *)
intros Hy3.
assert (y = bpow (fexp ey))%R.
apply Rminus_diag_uniq.
rewrite Hy3.
1374 1375
rewrite ulp_neq_0;[idtac|now apply Rgt_not_eq].
unfold canonic_exp.
1376 1377 1378
rewrite (ln_beta_unique beta y ey); trivial.
apply Hey.
now apply Rgt_not_eq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1379
contradict Hy2.
1380 1381 1382 1383 1384 1385 1386 1387
rewrite H1.
apply f_equal.
apply Zplus_reg_l with 1%Z.
ring_simplify.
apply trans_eq with (ln_beta beta y).
apply sym_eq; apply ln_beta_unique.
rewrite H1, Rabs_right.
split.
1388
apply bpow_le.
1389
omega.
1390
apply bpow_lt.
1391 1392 1393 1394 1395
omega.
apply Rle_ge; apply bpow_ge_0.
apply ln_beta_unique.
apply Hey.
now apply Rgt_not_eq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1396
(* *)
1397
case (Rle_or_lt (ulp (pred_pos y)) (y-x)); intros H1.
1398
(* . *)
1399 1400
apply Rplus_le_reg_r with (-x + ulp (pred_pos y))%R.
ring_simplify (x+(-x+ulp (pred_pos y)))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1401
apply Rle_trans with (1:=H1).
BOLDO Sylvie's avatar