Fcore_generic_fmt.v 53.9 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.
*)

20
(** * What is a real number belonging to a format, and many properties. *)
21 22 23 24
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
25

26
Section Generic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
27 28 29

Variable beta : radix.

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

32 33
Section Format.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
34 35
Variable fexp : Z -> Z.

36
(** To be a good fexp *)
37 38 39

Class Valid_exp :=
  valid_exp :
40 41 42 43 44 45
  forall k : Z,
  ( (fexp k < k)%Z -> (fexp (k + 1) <= k)%Z ) /\
  ( (k <= fexp k)%Z ->
    (fexp (fexp k + 1) <= fexp k)%Z /\
    forall l : Z, (l <= fexp k)%Z -> fexp l = fexp k ).

46
Context { valid_exp_ : Valid_exp }.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
47

48 49 50 51 52 53
Theorem valid_exp_large :
  forall k l,
  (fexp k < k)%Z -> (k <= l)%Z ->
  (fexp l < l)%Z.
Proof.
intros k l Hk H.
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73
apply Znot_ge_lt.
intros Hl.
apply Zge_le in Hl.
assert (H' := proj2 (proj2 (valid_exp l) Hl) k).
omega.
Qed.

Theorem valid_exp_large' :
  forall k l,
  (fexp k < k)%Z -> (l <= k)%Z ->
  (fexp l < k)%Z.
Proof.
intros k l Hk H.
apply Znot_ge_lt.
intros H'.
apply Zge_le in H'.
assert (Hl := Zle_trans _ _ _ H H').
apply valid_exp in Hl.
assert (H1 := proj2 Hl k H').
omega.
74 75
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
76
Definition canonic_exp x :=
77
  fexp (ln_beta beta x).
78 79

Definition canonic (f : float beta) :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
80
  Fexp f = canonic_exp (F2R f).
81

82
Definition scaled_mantissa x :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
83
  (x * bpow (- canonic_exp x))%R.
84

Guillaume Melquiond's avatar
Guillaume Melquiond committed
85
Definition generic_format (x : R) :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
86
  x = F2R (Float beta (Ztrunc (scaled_mantissa x)) (canonic_exp x)).
87

88
(** Basic facts *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
89 90 91
Theorem generic_format_0 :
  generic_format 0.
Proof.
92
unfold generic_format, scaled_mantissa.
93 94 95 96 97
rewrite Rmult_0_l.
change (Ztrunc 0) with (Ztrunc (Z2R 0)).
now rewrite Ztrunc_Z2R, F2R_0.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
98
Theorem canonic_exp_opp :
99
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
100
  canonic_exp (-x) = canonic_exp x.
101 102
Proof.
intros x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
103
unfold canonic_exp.
104
now rewrite ln_beta_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
105 106
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
107
Theorem canonic_exp_abs :
108
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
109
  canonic_exp (Rabs x) = canonic_exp x.
110 111
Proof.
intros x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
112
unfold canonic_exp.
113 114 115
now rewrite ln_beta_abs.
Qed.

116 117 118 119 120
Theorem generic_format_bpow :
  forall e, (fexp (e + 1) <= e)%Z ->
  generic_format (bpow e).
Proof.
intros e H.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
121
unfold generic_format, scaled_mantissa, canonic_exp.
122
rewrite ln_beta_bpow.
123
rewrite <- bpow_plus.
124 125 126 127 128
rewrite <- (Z2R_Zpower beta (e + - fexp (e + 1))).
rewrite Ztrunc_Z2R.
rewrite <- F2R_bpow.
rewrite F2R_change_exp with (1 := H).
now rewrite Zmult_1_l.
129 130 131 132 133 134 135 136 137 138
now apply Zle_minus_le_0.
Qed.

Theorem generic_format_bpow' :
  forall e, (fexp e <= e)%Z ->
  generic_format (bpow e).
Proof.
intros e He.
apply generic_format_bpow.
destruct (Zle_lt_or_eq _ _ He).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
now apply valid_exp_.
140
rewrite <- H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141
apply valid_exp.
142 143
rewrite H.
apply Zle_refl.
144 145
Qed.

146
Theorem generic_format_F2R :
147
  forall m e,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
148
  ( m <> 0 -> canonic_exp (F2R (Float beta m e)) <= e )%Z ->
149 150 151
  generic_format (F2R (Float beta m e)).
Proof.
intros m e.
152 153 154 155
destruct (Z_eq_dec m 0) as [Zm|Zm].
intros _.
rewrite Zm, F2R_0.
apply generic_format_0.
156
unfold generic_format, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
157
set (e' := canonic_exp (F2R (Float beta m e))).
158
intros He.
159
specialize (He Zm).
160
unfold F2R at 3. simpl.
161 162 163 164
rewrite  F2R_change_exp with (1 := He).
apply F2R_eq_compat.
rewrite Rmult_assoc, <- bpow_plus, <- Z2R_Zpower, <- Z2R_mult.
now rewrite Ztrunc_Z2R.
165 166 167
now apply Zle_left.
Qed.

168
Lemma generic_format_F2R': forall (x:R) (f:float beta),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
169
       F2R f = x -> ((x <> 0)%R ->
170 171 172 173 174 175 176 177 178 179 180 181 182 183
       (canonic_exp x <= Fexp f)%Z) ->
       generic_format x.
Proof.
intros x f H1 H2.
rewrite <- H1; destruct f as (m,e).
apply  generic_format_F2R.
simpl in *; intros H3.
rewrite H1; apply H2.
intros Y; apply H3.
apply F2R_eq_0_reg with beta e.
now rewrite H1.
Qed.


184 185 186 187 188 189 190
Theorem canonic_opp :
  forall m e,
  canonic (Float beta m e) ->
  canonic (Float beta (-m) e).
Proof.
intros m e H.
unfold canonic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
191
now rewrite F2R_Zopp, canonic_exp_opp.
192 193
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213
Theorem canonic_abs :
  forall m e,
  canonic (Float beta m e) ->
  canonic (Float beta (Zabs m) e).
Proof.
intros m e H.
unfold canonic.
now rewrite F2R_Zabs, canonic_exp_abs.
Qed.

Theorem canonic_0: canonic (Float beta 0 (fexp (ln_beta beta 0%R))).
Proof.
unfold canonic; simpl; unfold canonic_exp.
replace (F2R {| Fnum := 0; Fexp := fexp (ln_beta beta 0) |}) with 0%R.
reflexivity.
unfold F2R; simpl; ring.
Qed.



214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
Theorem canonic_unicity :
  forall f1 f2,
  canonic f1 ->
  canonic f2 ->
  F2R f1 = F2R f2 ->
  f1 = f2.
Proof.
intros (m1, e1) (m2, e2).
unfold canonic. simpl.
intros H1 H2 H.
rewrite H in H1.
rewrite <- H2 in H1. clear H2.
rewrite H1 in H |- *.
apply (f_equal (fun m => Float beta m e2)).
apply F2R_eq_reg with (1 := H).
Qed.

231
Theorem scaled_mantissa_generic :
232 233
  forall x,
  generic_format x ->
234
  scaled_mantissa x = Z2R (Ztrunc (scaled_mantissa x)).
235 236
Proof.
intros x Hx.
237
unfold scaled_mantissa.
238 239
pattern x at 1 3 ; rewrite Hx.
unfold F2R. simpl.
240
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
241 242 243
now rewrite Ztrunc_Z2R.
Qed.

244
Theorem scaled_mantissa_mult_bpow :
245
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
246
  (scaled_mantissa x * bpow (canonic_exp x))%R = x.
247 248 249
Proof.
intros x.
unfold scaled_mantissa.
250
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
251 252 253
apply Rmult_1_r.
Qed.

254 255 256 257 258 259
Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = R0.
Proof.
apply Rmult_0_l.
Qed.

260 261 262 263 264 265
Theorem scaled_mantissa_opp :
  forall x,
  scaled_mantissa (-x) = (-scaled_mantissa x)%R.
Proof.
intros x.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
266
rewrite canonic_exp_opp.
267 268 269
now rewrite Ropp_mult_distr_l_reverse.
Qed.

270 271 272 273 274 275
Theorem scaled_mantissa_abs :
  forall x,
  scaled_mantissa (Rabs x) = Rabs (scaled_mantissa x).
Proof.
intros x.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
276
rewrite canonic_exp_abs, Rabs_mult.
277 278 279 280 281 282
apply f_equal.
apply sym_eq.
apply Rabs_pos_eq.
apply bpow_ge_0.
Qed.

283 284 285 286 287
Theorem generic_format_opp :
  forall x, generic_format x -> generic_format (-x).
Proof.
intros x Hx.
unfold generic_format.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
288
rewrite scaled_mantissa_opp, canonic_exp_opp.
289
rewrite Ztrunc_opp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
290
rewrite F2R_Zopp.
291
now apply f_equal.
292 293
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
294 295 296 297 298
Theorem generic_format_abs :
  forall x, generic_format x -> generic_format (Rabs x).
Proof.
intros x Hx.
unfold generic_format.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
299
rewrite scaled_mantissa_abs, canonic_exp_abs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
300
rewrite Ztrunc_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
301
rewrite F2R_Zabs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
302 303 304
now apply f_equal.
Qed.

305 306 307 308 309 310
Theorem generic_format_abs_inv :
  forall x, generic_format (Rabs x) -> generic_format x.
Proof.
intros x.
unfold generic_format, Rabs.
case Rcase_abs ; intros _.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
311
rewrite scaled_mantissa_opp, canonic_exp_opp, Ztrunc_opp.
312 313
intros H.
rewrite <- (Ropp_involutive x) at 1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
314
rewrite H, F2R_Zopp.
315 316 317 318
apply Ropp_involutive.
easy.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
319
Theorem canonic_exp_fexp :
320
  forall x ex,
321
  (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
322
  canonic_exp x = fexp ex.
323 324
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
325
unfold canonic_exp.
326 327 328
now rewrite ln_beta_unique with (1 := Hx).
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
329
Theorem canonic_exp_fexp_pos :
330
  forall x ex,
331
  (bpow (ex - 1) <= x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
332
  canonic_exp x = fexp ex.
333 334
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
335
apply canonic_exp_fexp.
336 337
rewrite Rabs_pos_eq.
exact Hx.
338 339 340 341
apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.

342
(** Properties when the real number is "small" (kind of subnormal) *)
343 344 345 346 347 348 349
Theorem mantissa_small_pos :
  forall x ex,
  (bpow (ex - 1) <= x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  (0 < x * bpow (- fexp ex) < 1)%R.
Proof.
intros x ex Hx He.
350
split.
351 352 353 354 355 356
apply Rmult_lt_0_compat.
apply Rlt_le_trans with (2 := proj1 Hx).
apply bpow_gt_0.
apply bpow_gt_0.
apply Rmult_lt_reg_r with (bpow (fexp ex)).
apply bpow_gt_0.
357
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
358 359
rewrite Rmult_1_r, Rmult_1_l.
apply Rlt_le_trans with (1 := proj2 Hx).
360
now apply bpow_le.
361 362
Qed.

363 364 365 366 367 368 369 370 371 372 373 374
Theorem scaled_mantissa_small :
  forall x ex,
  (Rabs x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  (Rabs (scaled_mantissa x) < 1)%R.
Proof.
intros x ex Ex He.
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx, scaled_mantissa_0, Rabs_R0.
now apply (Z2R_lt 0 1).
rewrite <- scaled_mantissa_abs.
unfold scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
375 376
rewrite canonic_exp_abs.
unfold canonic_exp.
377 378 379 380 381 382 383 384
destruct (ln_beta beta x) as (ex', Ex').
simpl.
specialize (Ex' Zx).
apply (mantissa_small_pos _ _ Ex').
assert (ex' <= fexp ex)%Z.
apply Zle_trans with (2 := He).
apply bpow_lt_bpow with beta.
now apply Rle_lt_trans with (2 := Ex).
385
now rewrite (proj2 (proj2 (valid_exp _) He)).
386 387
Qed.

388 389 390 391 392 393 394 395 396 397 398 399 400 401 402
Theorem abs_scaled_mantissa_lt_bpow :
  forall x,
  (Rabs (scaled_mantissa x) < bpow (ln_beta beta x - canonic_exp x))%R.
Proof.
intros x.
destruct (Req_dec x 0) as [Zx|Zx].
rewrite Zx, scaled_mantissa_0, Rabs_R0.
apply bpow_gt_0.
apply Rlt_le_trans with (1 := bpow_ln_beta_gt beta _).
apply bpow_le.
unfold scaled_mantissa.
rewrite ln_beta_mult_bpow with (1 := Zx).
apply Zle_refl.
Qed.

403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426
Theorem ln_beta_generic_gt :
  forall x, (x <> 0)%R ->
  generic_format x ->
  (canonic_exp x < ln_beta beta x)%Z.
Proof.
intros x Zx Gx.
apply Znot_ge_lt.
unfold canonic_exp.
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Zx).
intros H.
apply Zge_le in H.
generalize (scaled_mantissa_small x ex (proj2 Ex) H).
contradict Zx.
rewrite Gx.
replace (Ztrunc (scaled_mantissa x)) with Z0.
apply F2R_0.
cut (Zabs (Ztrunc (scaled_mantissa x)) < 1)%Z.
clear ; zify ; omega.
apply lt_Z2R.
rewrite Z2R_abs.
now rewrite <- scaled_mantissa_generic.
Qed.

427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
Theorem mantissa_DN_small_pos :
  forall x ex,
  (bpow (ex - 1) <= x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  Zfloor (x * bpow (- fexp ex)) = Z0.
Proof.
intros x ex Hx He.
apply Zfloor_imp. simpl.
assert (H := mantissa_small_pos x ex Hx He).
split ; try apply Rlt_le ; apply H.
Qed.

Theorem mantissa_UP_small_pos :
  forall x ex,
  (bpow (ex - 1) <= x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  Zceil (x * bpow (- fexp ex)) = 1%Z.
Proof.
intros x ex Hx He.
apply Zceil_imp. simpl.
assert (H := mantissa_small_pos x ex Hx He).
split ; try apply Rlt_le ; apply H.
449 450
Qed.

451
(** Generic facts about any format *)
452 453
Theorem generic_format_discrete :
  forall x m,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
454
  let e := canonic_exp x in
455 456 457 458 459 460 461 462 463 464 465 466 467
  (F2R (Float beta m e) < x < F2R (Float beta (m + 1) e))%R ->
  ~ generic_format x.
Proof.
intros x m e (Hx,Hx2) Hf.
apply Rlt_not_le with (1 := Hx2). clear Hx2.
rewrite Hf.
fold e.
apply F2R_le_compat.
apply Zlt_le_succ.
apply lt_Z2R.
rewrite <- scaled_mantissa_generic with (1 := Hf).
apply Rmult_lt_reg_r with (bpow e).
apply bpow_gt_0.
468
now rewrite scaled_mantissa_mult_bpow.
469 470
Qed.

471 472 473 474 475 476
Theorem generic_format_canonic :
  forall f, canonic f ->
  generic_format (F2R f).
Proof.
intros (m, e) Hf.
unfold canonic in Hf. simpl in Hf.
477
unfold generic_format, scaled_mantissa.
478
rewrite <- Hf.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
479
apply F2R_eq_compat.
480
unfold F2R. simpl.
481
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
482 483 484
now rewrite Ztrunc_Z2R.
Qed.

485 486 487 488 489 490 491 492 493 494 495 496 497
Theorem generic_format_ge_bpow :
  forall emin,
  ( forall e, (emin <= fexp e)%Z ) ->
  forall x,
  (0 < x)%R ->
  generic_format x ->
  (bpow emin <= x)%R.
Proof.
intros emin Emin x Hx Fx.
rewrite Fx.
apply Rle_trans with (bpow (fexp (ln_beta beta x))).
now apply bpow_le.
apply bpow_le_F2R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
498
apply F2R_gt_0_reg with beta (canonic_exp x).
499 500 501
now rewrite <- Fx.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
502
Theorem abs_lt_bpow_prec:
503
  forall prec,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
504
  (forall e, (e - prec <= fexp e)%Z) ->
505
  (* OK with FLX, FLT and FTZ *)
506
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
507 508
  (Rabs x < bpow (prec + canonic_exp x))%R.
intros prec Hp x.
509 510 511
case (Req_dec x 0); intros Hxz.
rewrite Hxz, Rabs_R0.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
512
unfold canonic_exp.
513 514 515
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Hxz).
apply Rlt_le_trans with (1 := proj2 Ex).
516
apply bpow_le.
517
specialize (Hp ex).
518 519 520
omega.
Qed.

521
Theorem generic_format_bpow_inv' :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
522
  forall e,
523 524
  generic_format (bpow e) ->
  (fexp (e + 1) <= e)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
525 526
Proof.
intros e He.
527 528 529 530 531
apply Znot_gt_le.
contradict He.
unfold generic_format, scaled_mantissa, canonic_exp, F2R. simpl.
rewrite ln_beta_bpow, <- bpow_plus.
apply Rgt_not_eq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
532
rewrite Ztrunc_floor.
533 534 535 536
2: apply bpow_ge_0.
rewrite Zfloor_imp with (n := Z0).
rewrite Rmult_0_l.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
537
split.
538 539 540 541 542 543 544 545 546 547 548 549 550
apply bpow_ge_0.
apply (bpow_lt _ _ 0).
clear -He ; omega.
Qed.

Theorem generic_format_bpow_inv :
  forall e,
  generic_format (bpow e) ->
  (fexp e <= e)%Z.
Proof.
intros e He.
apply generic_format_bpow_inv' in He.
assert (H := valid_exp_large' (e + 1) e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
551 552 553
omega.
Qed.

554
Section Fcore_generic_round_pos.
555

BOLDO Sylvie's avatar
BOLDO Sylvie committed
556
(** Rounding functions: R -> Z *)
557 558 559 560

Variable rnd : R -> Z.

Class Valid_rnd := {
561
  Zrnd_le : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z ;
562
  Zrnd_Z2R : forall n, rnd (Z2R n) = n
563 564
}.

565
Context { valid_rnd : Valid_rnd }.
566

567
Theorem Zrnd_DN_or_UP :
568
  forall x, rnd x = Zfloor x \/ rnd x = Zceil x.
569
Proof.
570
intros x.
571
destruct (Zle_or_lt (rnd x) (Zfloor x)) as [Hx|Hx].
572 573
left.
apply Zle_antisym with (1 := Hx).
574
rewrite <- (Zrnd_Z2R (Zfloor x)).
575
apply Zrnd_le.
576 577 578
apply Zfloor_lb.
right.
apply Zle_antisym.
579
rewrite <- (Zrnd_Z2R (Zceil x)).
580
apply Zrnd_le.
581 582 583 584 585 586 587 588 589
apply Zceil_ub.
rewrite Zceil_floor_neq.
omega.
intros H.
rewrite <- H in Hx.
rewrite Zfloor_Z2R, Zrnd_Z2R in Hx.
apply Zlt_irrefl with (1 := Hx).
Qed.

590 591 592 593 594 595 596 597 598 599 600 601 602
Theorem Zrnd_ZR_or_AW :
  forall x, rnd x = Ztrunc x \/ rnd x = Zaway x.
Proof.
intros x.
unfold Ztrunc, Zaway.
destruct (Zrnd_DN_or_UP x) as [Hx|Hx] ;
  case Rlt_bool.
now right.
now left.
now left.
now right.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
603
(** the most useful one: R -> F *)
604
Definition round x :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
605
  F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
606

607
Theorem round_bounded_large_pos :
608 609 610
  forall x ex,
  (fexp ex < ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
611
  (bpow (ex - 1) <= round x <= bpow ex)%R.
612 613
Proof.
intros x ex He Hx.
614
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
615
rewrite (canonic_exp_fexp_pos _ _ Hx).
616
unfold F2R. simpl.
617
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr.
618 619 620
(* DN *)
split.
replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
621
rewrite bpow_plus.
622 623
apply Rmult_le_compat_r.
apply bpow_ge_0.
624
assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
625 626 627 628 629 630
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zfloor_lub.
rewrite Hf.
631
rewrite bpow_plus.
632 633 634 635 636 637
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Hx.
apply Rle_trans with (2 := Rlt_le _ _ (proj2 Hx)).
apply Rmult_le_reg_r with (bpow (- fexp ex)).
apply bpow_gt_0.
638
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
639 640 641 642 643 644
apply Zfloor_lb.
(* UP *)
split.
apply Rle_trans with (1 := proj1 Hx).
apply Rmult_le_reg_r with (bpow (- fexp ex)).
apply bpow_gt_0.
645
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
646 647
apply Zceil_ub.
pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
648
rewrite bpow_plus.
649 650
apply Rmult_le_compat_r.
apply bpow_ge_0.
651
assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
652 653 654 655 656 657 658
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zceil_glb.
rewrite Hf.
unfold Zminus.
659
rewrite bpow_plus.
660 661 662 663 664 665
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hx.
Qed.

666
Theorem round_bounded_small_pos :
667 668 669
  forall x ex,
  (ex <= fexp ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
670
  round x = R0 \/ round x = bpow (fexp ex).
671 672
Proof.
intros x ex He Hx.
673
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
674
rewrite (canonic_exp_fexp_pos _ _ Hx).
675
unfold F2R. simpl.
676
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr.
677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693
(* DN *)
left.
apply Rmult_eq_0_compat_r.
apply (@f_equal _ _ Z2R _ Z0).
apply Zfloor_imp.
refine (let H := _ in conj (Rlt_le _ _ (proj1 H)) (proj2 H)).
now apply mantissa_small_pos.
(* UP *)
right.
pattern (bpow (fexp ex)) at 2 ; rewrite <- Rmult_1_l.
apply (f_equal (fun m => (m * bpow (fexp ex))%R)).
apply (@f_equal _ _ Z2R _ 1%Z).
apply Zceil_imp.
refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))).
now apply mantissa_small_pos.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761
Theorem round_le_pos :
  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
Proof.
intros x y Hx Hxy.
destruct (ln_beta beta x) as [ex Hex].
destruct (ln_beta beta y) as [ey Hey].
specialize (Hex (Rgt_not_eq _ _ Hx)).
specialize (Hey (Rgt_not_eq _ _ (Rlt_le_trans _ _ _ Hx Hxy))).
rewrite Rabs_pos_eq in Hex.
2: now apply Rlt_le.
rewrite Rabs_pos_eq in Hey.
2: apply Rle_trans with (2:=Hxy); now apply Rlt_le.
assert (He: (ex <= ey)%Z).
  apply bpow_lt_bpow with beta.
  apply Rle_lt_trans with (1 := proj1 Hex).
  now apply Rle_lt_trans with y.
assert (Heq: fexp ex = fexp ey -> (round x <= round y)%R).
  intros H.
  unfold round, scaled_mantissa, canonic_exp.
  rewrite ln_beta_unique_pos with (1 := Hex).
  rewrite ln_beta_unique_pos with (1 := Hey).
  rewrite H.
  apply F2R_le_compat.
  apply Zrnd_le.
  apply Rmult_le_compat_r with (2 := Hxy).
  apply bpow_ge_0.
destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
  apply Heq.
  apply valid_exp with (1 := Hy1).
  now apply Zle_trans with ey.
destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
2: now apply Heq, f_equal.
apply Rle_trans with (bpow (ey - 1)).
2: now apply round_bounded_large_pos.
destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
  destruct (round_bounded_small_pos _ _ Hx1 Hex) as [-> | ->].
  apply bpow_ge_0.
  apply bpow_le.
  apply valid_exp, proj2 in Hx1.
  specialize (Hx1 ey).
  omega.
apply Rle_trans with (bpow ex).
now apply round_bounded_large_pos.
apply bpow_le.
now apply Z.lt_le_pred.
Qed.

Theorem round_generic :
  forall x,
  generic_format x ->
  round x = x.
Proof.
intros x Hx.
unfold round.
rewrite scaled_mantissa_generic with (1 := Hx).
rewrite Zrnd_Z2R.
now apply sym_eq.
Qed.

Theorem round_0 :
  round 0 = R0.
Proof.
unfold round, scaled_mantissa.
rewrite Rmult_0_l.
fold (Z2R 0).
rewrite Zrnd_Z2R.
apply F2R_0.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
762 763

Theorem exp_small_round_0_pos :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
764 765
  forall x ex,
 (bpow (ex - 1) <= x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
766 767 768 769 770 771 772 773 774 775 776
   round x =R0 -> (ex <= fexp ex)%Z .
Proof.
intros x ex H H1.
case (Zle_or_lt ex (fexp ex)); trivial; intros V.
contradict H1.
apply Rgt_not_eq.
apply Rlt_le_trans with (bpow (ex-1)).
apply bpow_gt_0.
apply  (round_bounded_large_pos); assumption.
Qed.

777
Theorem generic_format_round_pos :
778 779
  forall x,
  (0 < x)%R ->
780
  generic_format (round x).
781 782 783 784 785 786 787
Proof.
intros x Hx0.
destruct (ln_beta beta x) as (ex, Hex).
specialize (Hex (Rgt_not_eq _ _ Hx0)).
rewrite Rabs_pos_eq in Hex. 2: now apply Rlt_le.
destruct (Zle_or_lt ex (fexp ex)) as [He|He].
(* small *)
788
destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr.
789 790
apply generic_format_0.
apply generic_format_bpow.
791
now apply valid_exp.
792
(* large *)
793
generalize (round_bounded_large_pos _ _ He Hex).
794
intros (Hr1, Hr2).
795
destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
796 797
rewrite <- (Rle_antisym _ _ Hr Hr2).
apply generic_format_bpow.
798
now apply valid_exp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
799 800 801
apply generic_format_F2R.
intros _.
rewrite (canonic_exp_fexp_pos (F2R _) _ (conj Hr1 Hr)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
802
rewrite (canonic_exp_fexp_pos _ _ Hex).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
803
now apply Zeq_le.
804 805
Qed.

806
End Fcore_generic_round_pos.
807

808
Theorem round_ext :
809
  forall rnd1 rnd2,
810
  ( forall x, rnd1 x = rnd2 x ) ->
811
  forall x,
812
  round rnd1 x = round rnd2 x.
813 814
Proof.
intros rnd1 rnd2 Hext x.
815
unfold round.
816 817 818
now rewrite Hext.
Qed.

819
Section Zround_opp.
820

821 822
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
823

824
Definition Zrnd_opp x := Zopp (rnd (-x)).
825

826 827 828 829
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Proof with auto with typeclass_instances.
split.
(* *)
830
intros x y Hxy.
831
unfold Zrnd_opp.
832 833
apply Zopp_le_cancel.
rewrite 2!Zopp_involutive.
834
apply Zrnd_le...
835
now apply Ropp_le_contravar.
836
(* *)
837
intros n.
838
unfold Zrnd_opp.
839
rewrite <- Z2R_opp, Zrnd_Z2R...
840 841 842
apply Zopp_involutive.
Qed.

843
Theorem round_opp :
844
  forall x,
845
  round rnd (- x) = Ropp (round Zrnd_opp x).
846 847
Proof.
intros x.
848
unfold round.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
849
rewrite <- F2R_Zopp, canonic_exp_opp, scaled_mantissa_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
850
apply F2R_eq_compat.
851 852 853 854
apply sym_eq.
exact (Zopp_involutive _).
Qed.

855
End Zround_opp.
856

857
(** IEEE-754 roundings: up, down and to zero *)
858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879

Global Instance valid_rnd_DN : Valid_rnd Zfloor.
Proof.
split.
apply Zfloor_le.
apply Zfloor_Z2R.
Qed.

Global Instance valid_rnd_UP : Valid_rnd Zceil.
Proof.
split.
apply Zceil_le.
apply Zceil_Z2R.
Qed.

Global Instance valid_rnd_ZR : Valid_rnd Ztrunc.
Proof.
split.
apply Ztrunc_le.
apply Ztrunc_Z2R.
Qed.

880 881 882 883 884 885 886
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Proof.
split.
apply Zaway_le.
apply Zaway_Z2R.
Qed.

887 888 889 890
Section monotone.

Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
891

892
Theorem round_DN_or_UP :
893 894
  forall x,
  round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
895
Proof.
896
intros x.
897
unfold round.
898
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx].
899 900 901 902
left. now rewrite Hx.
right. now rewrite Hx.
Qed.

903 904 905 906 907 908 909 910 911 912 913
Theorem round_ZR_or_AW :
  forall x,
  round rnd x = round Ztrunc x \/ round rnd x = round Zaway x.
Proof.
intros x.
unfold round.
destruct (Zrnd_ZR_or_AW rnd (scaled_mantissa x)) as [Hx|Hx].
left. now rewrite Hx.
right. now rewrite Hx.
Qed.

914
Theorem round_le :
915 916 917
  forall x y, (x <= y)%R -> (round rnd x <= round rnd y)%R.
Proof with auto with typeclass_instances.
intros x y Hxy.
918
destruct (total_order_T x 0) as [[Hx|Hx]|Hx].
919
3: now apply round_le_pos.
920
(* x < 0 *)
921
unfold round.
922 923 924 925
destruct (Rlt_or_le y 0) as [Hy|Hy].
(* . y < 0 *)
rewrite <- (Ropp_involutive x), <- (Ropp_involutive y).
rewrite (scaled_mantissa_opp (-x)), (scaled_mantissa_opp (-y)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
926
rewrite (canonic_exp_opp (-x)), (canonic_exp_opp (-y)).
927
apply Ropp_le_cancel.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
928
rewrite <- 2!F2R_Zopp.
929
apply (round_le_pos (Zrnd_opp rnd) (-y) (-x)).
930 931 932 933 934 935
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
now apply Ropp_le_contravar.
(* . 0 <= y *)
apply Rle_trans with R0.
apply F2R_le_0_compat. simpl.
936
rewrite <- (Zrnd_Z2R rnd 0).
937
apply Zrnd_le...
938
simpl.
939
rewrite <- (Rmult_0_l (bpow (- fexp (ln_beta beta x)))).
940 941 942 943
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
apply F2R_ge_0_compat. simpl.
944
rewrite <- (Zrnd_Z2R rnd 0).
945
apply Zrnd_le...
946 947 948 949 950
apply Rmult_le_pos.
exact Hy.
apply bpow_ge_0.
(* x = 0 *)
rewrite Hx.
951
rewrite round_0...
952 953
apply F2R_ge_0_compat.
simpl.
954
rewrite <- (Zrnd_Z2R rnd 0).
955
apply Zrnd_le...
956 957 958 959 960
apply Rmult_le_pos.
now rewrite <- Hx.
apply bpow_ge_0.
Qed.

961
Theorem round_ge_generic :
962
  forall x y, generic_format x -> (x <= y)%R -> (x <= round rnd y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
963
Proof.
964
intros x y Hx Hxy.
965
rewrite <- (round_generic rnd x Hx).
966
now apply round_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
967
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
968

969
Theorem round_le_generic :
970
  forall x y, generic_format y -> (x <= y)%R -> (round rnd x <= y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
971
Proof.
972
intros x y Hy Hxy.
973
rewrite <- (round_generic rnd y Hy).
974
now apply round_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
975
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
976

977 978
End monotone.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
979
Theorem round_abs_abs :
980
  forall P : R -> R -> Prop,
981
  ( forall rnd (Hr : Valid_rnd rnd) x, (0 <= x)%R -> P x (round rnd x) ) ->
982 983 984
  forall rnd {Hr : Valid_rnd rnd} x, P (Rabs x) (Rabs (round rnd x)).
Proof with auto with typeclass_instances.
intros P HP rnd Hr x.
985 986 987
destruct (Rle_or_lt 0 x) as [Hx|Hx].
(* . *)
rewrite 2!Rabs_pos_eq.
988
now apply HP.
989
rewrite <- (round_0 rnd).
990
now apply round_le.
991 992 993 994 995
exact Hx.
(* . *)
rewrite (Rabs_left _ Hx).
rewrite Rabs_left1.
pattern x at 2 ; rewrite <- Ropp_involutive.
996
rewrite round_opp.
997
rewrite Ropp_involutive.
998
apply HP...
999 1000 1001
rewrite <- Ropp_0.
apply Ropp_le_contravar.
now apply Rlt_le.
1002
rewrite <- (round_0 rnd).
1003
apply round_le...
1004 1005 1006
now apply Rlt_le.
Qed.

1007 1008 1009 1010