Fcore_generic_fmt.v 52.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 139 140 141 142 143
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).
now apply valid_exp.
rewrite <- H.
apply valid_exp_.
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 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183
Lemma generic_format_F2R_2: forall (x:R) (f:float beta),
       F2R f = x -> ((x <> 0)%R -> 
       (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_le_pos :
608
  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
609
Proof.
610
intros x y Hx Hxy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
611
unfold round, scaled_mantissa, canonic_exp.
612 613 614 615 616 617 618 619 620 621
destruct (ln_beta beta x) as (ex, Hex). simpl.
destruct (ln_beta beta y) as (ey, Hey). simpl.
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).
cut (ex - 1 < ey)%Z. omega.
622
apply (lt_bpow beta).
623 624 625 626
apply Rle_lt_trans with (1 := proj1 Hex).
apply Rle_lt_trans with (1 := Hxy).
apply Hey.
destruct (Zle_or_lt ey (fexp ey)) as [Hy1|Hy1].
627
rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex).
628
apply F2R_le_compat.
629
apply Zrnd_le.
630 631 632 633 634 635
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
now apply Zle_trans with ey.
destruct (Zle_lt_or_eq _ _ He) as [He'|He'].
destruct (Zle_or_lt ey (fexp ex)) as [Hx2|Hx2].
636
rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
637
apply F2R_le_compat.
638
apply Zrnd_le.
639 640 641
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
642
apply Rle_trans with (F2R (Float beta (rnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))).
643
rewrite <- bpow_plus.
644 645 646 647 648
rewrite <- (Z2R_Zpower beta (ey - 1 + -fexp ey)). 2: omega.
rewrite Zrnd_Z2R.
destruct (Zle_or_lt ex (fexp ex)) as [Hx1|Hx1].
apply Rle_trans with (F2R (Float beta 1 (fexp ex))).
apply F2R_le_compat.
649
rewrite <- (Zrnd_Z2R 1).
650
apply Zrnd_le.
651 652 653 654
apply Rlt_le.
exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
unfold F2R. simpl.
rewrite Z2R_Zpower. 2: omega.
655
rewrite <- bpow_plus, Rmult_1_l.
656
apply bpow_le.
657
omega.
658
apply Rle_trans with (F2R (Float beta (rnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
659
apply F2R_le_compat.
660
apply Zrnd_le.
661 662 663 664
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hex.
665
rewrite <- bpow_plus.
666 667 668 669
rewrite <- Z2R_Zpower. 2: omega.
rewrite Zrnd_Z2R.
unfold F2R. simpl.
rewrite 2!Z2R_Zpower ; try omega.
670
rewrite <- 2!bpow_plus.
671
apply bpow_le.
672 673
omega.
apply F2R_le_compat.
674
apply Zrnd_le.
675 676 677 678 679
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Hey.
rewrite He'.
apply F2R_le_compat.
680
apply Zrnd_le.
681 682 683 684 685
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
Qed.

686
Theorem round_generic :
687 688
  forall x,
  generic_format x ->
689
  round x = x.
690 691
Proof.
intros x Hx.
692
unfold round.
693 694 695 696 697
rewrite scaled_mantissa_generic with (1 := Hx).
rewrite Zrnd_Z2R.
now apply sym_eq.
Qed.

698 699
Theorem round_0 :
  round 0 = R0.
700
Proof.
701
unfold round, scaled_mantissa.
702 703 704 705 706 707
rewrite Rmult_0_l.
fold (Z2R 0).
rewrite Zrnd_Z2R.
apply F2R_0.
Qed.

708
Theorem round_bounded_large_pos :
709 710 711
  forall x ex,
  (fexp ex < ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
712
  (bpow (ex - 1) <= round x <= bpow ex)%R.
713 714
Proof.
intros x ex He Hx.
715
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
716
rewrite (canonic_exp_fexp_pos _ _ Hx).
717
unfold F2R. simpl.
718
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr.
719 720 721
(* DN *)
split.
replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
722
rewrite bpow_plus.
723 724
apply Rmult_le_compat_r.
apply bpow_ge_0.
725
assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
726 727 728 729 730 731
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zfloor_lub.
rewrite Hf.
732
rewrite bpow_plus.
733 734 735 736 737 738
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.
739
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
740 741 742 743 744 745
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.
746
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
747 748
apply Zceil_ub.
pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
749
rewrite bpow_plus.
750 751
apply Rmult_le_compat_r.
apply bpow_ge_0.
752
assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
753 754 755 756 757 758 759
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zceil_glb.
rewrite Hf.
unfold Zminus.
760
rewrite bpow_plus.
761 762 763 764 765 766
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hx.
Qed.

767
Theorem round_bounded_small_pos :
768 769 770
  forall x ex,
  (ex <= fexp ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
771
  round x = R0 \/ round x = bpow (fexp ex).
772 773
Proof.
intros x ex He Hx.
774
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
775
rewrite (canonic_exp_fexp_pos _ _ Hx).
776
unfold F2R. simpl.
777
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr.
778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794
(* 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.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812

Theorem exp_small_round_0_pos :
  forall x ex, 
 (bpow (ex - 1) <= x < bpow ex)%R ->  
   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.




813
Theorem generic_format_round_pos :
814 815
  forall x,
  (0 < x)%R ->
816
  generic_format (round x).
817 818 819 820 821 822 823
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 *)
824
destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr.
825 826
apply generic_format_0.
apply generic_format_bpow.
827
now apply valid_exp.
828
(* large *)
829
generalize (round_bounded_large_pos _ _ He Hex).
830
intros (Hr1, Hr2).
831
destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
832 833
rewrite <- (Rle_antisym _ _ Hr Hr2).
apply generic_format_bpow.
834
now apply valid_exp.
835 836
assert (Hr' := conj Hr1 Hr).
unfold generic_format, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
837
rewrite (canonic_exp_fexp_pos _ _ Hr').
838
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
839
rewrite (canonic_exp_fexp_pos _ _ Hex).
840
unfold F2R at 3. simpl.
841
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
842 843 844
now rewrite Ztrunc_Z2R.
Qed.

845
End Fcore_generic_round_pos.
846

847
Theorem round_ext :
848
  forall rnd1 rnd2,
849
  ( forall x, rnd1 x = rnd2 x ) ->
850
  forall x,
851
  round rnd1 x = round rnd2 x.
852 853
Proof.
intros rnd1 rnd2 Hext x.
854
unfold round.
855 856 857
now rewrite Hext.
Qed.

858
Section Zround_opp.
859

860 861
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
862

863
Definition Zrnd_opp x := Zopp (rnd (-x)).
864

865 866 867 868
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Proof with auto with typeclass_instances.
split.
(* *)
869
intros x y Hxy.
870
unfold Zrnd_opp.
871 872
apply Zopp_le_cancel.
rewrite 2!Zopp_involutive.
873
apply Zrnd_le...
874
now apply Ropp_le_contravar.
875
(* *)
876
intros n.
877
unfold Zrnd_opp.
878
rewrite <- Z2R_opp, Zrnd_Z2R...
879 880 881
apply Zopp_involutive.
Qed.

882
Theorem round_opp :
883
  forall x,
884
  round rnd (- x) = Ropp (round Zrnd_opp x).
885 886
Proof.
intros x.
887
unfold round.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
888
rewrite <- F2R_Zopp, canonic_exp_opp, scaled_mantissa_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
889
apply F2R_eq_compat.
890 891 892 893
apply sym_eq.
exact (Zopp_involutive _).
Qed.

894
End Zround_opp.
895

896
(** IEEE-754 roundings: up, down and to zero *)
897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918

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.

919 920 921 922 923 924 925
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Proof.
split.
apply Zaway_le.
apply Zaway_Z2R.
Qed.

926 927 928 929
Section monotone.

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

931
Theorem round_DN_or_UP :
932 933
  forall x,
  round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
934
Proof.
935
intros x.
936
unfold round.
937
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx].
938 939 940 941
left. now rewrite Hx.
right. now rewrite Hx.
Qed.

942 943 944 945 946 947 948 949 950 951 952
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.

953
Theorem round_le :
954 955 956
  forall x y, (x <= y)%R -> (round rnd x <= round rnd y)%R.
Proof with auto with typeclass_instances.
intros x y Hxy.
957
destruct (total_order_T x 0) as [[Hx|Hx]|Hx].
958
3: now apply round_le_pos.
959
(* x < 0 *)
960
unfold round.
961 962 963 964
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
965
rewrite (canonic_exp_opp (-x)), (canonic_exp_opp (-y)).
966
apply Ropp_le_cancel.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
967
rewrite <- 2!F2R_Zopp.
968
apply (round_le_pos (Zrnd_opp rnd) (-y) (-x)).
969 970 971 972 973 974
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.
975
rewrite <- (Zrnd_Z2R rnd 0).
976
apply Zrnd_le...
977
simpl.
978
rewrite <- (Rmult_0_l (bpow (- fexp (ln_beta beta x)))).
979 980 981 982
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
apply F2R_ge_0_compat. simpl.
983
rewrite <- (Zrnd_Z2R rnd 0).
984
apply Zrnd_le...
985 986 987 988 989
apply Rmult_le_pos.
exact Hy.
apply bpow_ge_0.
(* x = 0 *)
rewrite Hx.
990
rewrite round_0...