Fcore_generic_fmt.v 50.7 KB
Newer Older
1
(**
2 3 4
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

BOLDO Sylvie's avatar
BOLDO Sylvie committed
5
Copyright (C) 2010-2011 Sylvie Boldo
6
#<br />#
BOLDO Sylvie's avatar
BOLDO Sylvie committed
7
Copyright (C) 2010-2011 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 168 169 170 171 172 173 174
now apply Zle_left.
Qed.

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
175
now rewrite F2R_Zopp, canonic_exp_opp.
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
Qed.

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.

195
Theorem scaled_mantissa_generic :
196 197
  forall x,
  generic_format x ->
198
  scaled_mantissa x = Z2R (Ztrunc (scaled_mantissa x)).
199 200
Proof.
intros x Hx.
201
unfold scaled_mantissa.
202 203
pattern x at 1 3 ; rewrite Hx.
unfold F2R. simpl.
204
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
205 206 207
now rewrite Ztrunc_Z2R.
Qed.

208
Theorem scaled_mantissa_mult_bpow :
209
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
210
  (scaled_mantissa x * bpow (canonic_exp x))%R = x.
211 212 213
Proof.
intros x.
unfold scaled_mantissa.
214
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
215 216 217
apply Rmult_1_r.
Qed.

218 219 220 221 222 223
Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = R0.
Proof.
apply Rmult_0_l.
Qed.

224 225 226 227 228 229
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
230
rewrite canonic_exp_opp.
231 232 233
now rewrite Ropp_mult_distr_l_reverse.
Qed.

234 235 236 237 238 239
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
240
rewrite canonic_exp_abs, Rabs_mult.
241 242 243 244 245 246
apply f_equal.
apply sym_eq.
apply Rabs_pos_eq.
apply bpow_ge_0.
Qed.

247 248 249 250 251
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
252
rewrite scaled_mantissa_opp, canonic_exp_opp.
253
rewrite Ztrunc_opp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
254
rewrite F2R_Zopp.
255
now apply f_equal.
256 257
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
258 259 260 261 262
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
263
rewrite scaled_mantissa_abs, canonic_exp_abs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
264
rewrite Ztrunc_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
265
rewrite F2R_Zabs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
266 267 268
now apply f_equal.
Qed.

269 270 271 272 273 274
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
275
rewrite scaled_mantissa_opp, canonic_exp_opp, Ztrunc_opp.
276 277
intros H.
rewrite <- (Ropp_involutive x) at 1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
278
rewrite H, F2R_Zopp.
279 280 281 282
apply Ropp_involutive.
easy.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
283
Theorem canonic_exp_fexp :
284
  forall x ex,
285
  (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
286
  canonic_exp x = fexp ex.
287 288
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
289
unfold canonic_exp.
290 291 292
now rewrite ln_beta_unique with (1 := Hx).
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
293
Theorem canonic_exp_fexp_pos :
294
  forall x ex,
295
  (bpow (ex - 1) <= x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
296
  canonic_exp x = fexp ex.
297 298
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
299
apply canonic_exp_fexp.
300 301
rewrite Rabs_pos_eq.
exact Hx.
302 303 304 305
apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.

306
(** Properties when the real number is "small" (kind of subnormal) *)
307 308 309 310 311 312 313
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.
314
split.
315 316 317 318 319 320
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.
321
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
322 323
rewrite Rmult_1_r, Rmult_1_l.
apply Rlt_le_trans with (1 := proj2 Hx).
324
now apply bpow_le.
325 326
Qed.

327 328 329 330 331 332 333 334 335 336 337 338
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
339 340
rewrite canonic_exp_abs.
unfold canonic_exp.
341 342 343 344 345 346 347 348
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).
349
now rewrite (proj2 (proj2 (valid_exp _) He)).
350 351
Qed.

352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
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.

367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390
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.

391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412
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.
413 414
Qed.

415
(** Generic facts about any format *)
416 417
Theorem generic_format_discrete :
  forall x m,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
418
  let e := canonic_exp x in
419 420 421 422 423 424 425 426 427 428 429 430 431
  (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.
432
now rewrite scaled_mantissa_mult_bpow.
433 434
Qed.

435 436 437 438 439 440
Theorem generic_format_canonic :
  forall f, canonic f ->
  generic_format (F2R f).
Proof.
intros (m, e) Hf.
unfold canonic in Hf. simpl in Hf.
441
unfold generic_format, scaled_mantissa.
442
rewrite <- Hf.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
443
apply F2R_eq_compat.
444
unfold F2R. simpl.
445
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
446 447 448
now rewrite Ztrunc_Z2R.
Qed.

449 450 451 452 453 454 455 456 457 458 459 460 461
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
462
apply F2R_gt_0_reg with beta (canonic_exp x).
463 464 465
now rewrite <- Fx.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
466
Theorem abs_lt_bpow_prec:
467
  forall prec,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
468
  (forall e, (e - prec <= fexp e)%Z) ->
469
  (* OK with FLX, FLT and FTZ *)
470
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
471 472
  (Rabs x < bpow (prec + canonic_exp x))%R.
intros prec Hp x.
473 474 475
case (Req_dec x 0); intros Hxz.
rewrite Hxz, Rabs_R0.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
476
unfold canonic_exp.
477 478 479
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Hxz).
apply Rlt_le_trans with (1 := proj2 Ex).
480
apply bpow_le.
481
specialize (Hp ex).
482 483 484
omega.
Qed.

485
Theorem generic_format_bpow_inv' :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
486
  forall e,
487 488
  generic_format (bpow e) ->
  (fexp (e + 1) <= e)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
489 490
Proof.
intros e He.
491 492 493 494 495
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
496
rewrite Ztrunc_floor.
497 498 499 500
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
501
split.
502 503 504 505 506 507 508 509 510 511 512 513 514
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
515 516 517
omega.
Qed.

518
Section Fcore_generic_round_pos.
519

BOLDO Sylvie's avatar
BOLDO Sylvie committed
520
(** Rounding functions: R -> Z *)
521 522 523 524

Variable rnd : R -> Z.

Class Valid_rnd := {
525
  Zrnd_le : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z ;
526
  Zrnd_Z2R : forall n, rnd (Z2R n) = n
527 528
}.

529
Context { valid_rnd : Valid_rnd }.
530

531
Theorem Zrnd_DN_or_UP :
532
  forall x, rnd x = Zfloor x \/ rnd x = Zceil x.
533
Proof.
534
intros x.
535
destruct (Zle_or_lt (rnd x) (Zfloor x)) as [Hx|Hx].
536 537
left.
apply Zle_antisym with (1 := Hx).
538
rewrite <- (Zrnd_Z2R (Zfloor x)).
539
apply Zrnd_le.
540 541 542
apply Zfloor_lb.
right.
apply Zle_antisym.
543
rewrite <- (Zrnd_Z2R (Zceil x)).
544
apply Zrnd_le.
545 546 547 548 549 550 551 552 553
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.

554 555 556 557 558 559 560 561 562 563 564 565 566
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
567
(** the most useful one: R -> F *)
568
Definition round x :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
569
  F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
570

571
Theorem round_le_pos :
572
  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
573
Proof.
574
intros x y Hx Hxy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
575
unfold round, scaled_mantissa, canonic_exp.
576 577 578 579 580 581 582 583 584 585
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.
586
apply (lt_bpow beta).
587 588 589 590
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].
591
rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex).
592
apply F2R_le_compat.
593
apply Zrnd_le.
594 595 596 597 598 599
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].
600
rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
601
apply F2R_le_compat.
602
apply Zrnd_le.
603 604 605
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
606
apply Rle_trans with (F2R (Float beta (rnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))).
607
rewrite <- bpow_plus.
608 609 610 611 612
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.
613
rewrite <- (Zrnd_Z2R 1).
614
apply Zrnd_le.
615 616 617 618
apply Rlt_le.
exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
unfold F2R. simpl.
rewrite Z2R_Zpower. 2: omega.
619
rewrite <- bpow_plus, Rmult_1_l.
620
apply bpow_le.
621
omega.
622
apply Rle_trans with (F2R (Float beta (rnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
623
apply F2R_le_compat.
624
apply Zrnd_le.
625 626 627 628
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hex.
629
rewrite <- bpow_plus.
630 631 632 633
rewrite <- Z2R_Zpower. 2: omega.
rewrite Zrnd_Z2R.
unfold F2R. simpl.
rewrite 2!Z2R_Zpower ; try omega.
634
rewrite <- 2!bpow_plus.
635
apply bpow_le.
636 637
omega.
apply F2R_le_compat.
638
apply Zrnd_le.
639 640 641 642 643
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Hey.
rewrite He'.
apply F2R_le_compat.
644
apply Zrnd_le.
645 646 647 648 649
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
Qed.

650
Theorem round_generic :
651 652
  forall x,
  generic_format x ->
653
  round x = x.
654 655
Proof.
intros x Hx.
656
unfold round.
657 658 659 660 661
rewrite scaled_mantissa_generic with (1 := Hx).
rewrite Zrnd_Z2R.
now apply sym_eq.
Qed.

662 663
Theorem round_0 :
  round 0 = R0.
664
Proof.
665
unfold round, scaled_mantissa.
666 667 668 669 670 671
rewrite Rmult_0_l.
fold (Z2R 0).
rewrite Zrnd_Z2R.
apply F2R_0.
Qed.

672
Theorem round_bounded_large_pos :
673 674 675
  forall x ex,
  (fexp ex < ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
676
  (bpow (ex - 1) <= round x <= bpow ex)%R.
677 678
Proof.
intros x ex He Hx.
679
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
680
rewrite (canonic_exp_fexp_pos _ _ Hx).
681
unfold F2R. simpl.
682
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr.
683 684 685
(* DN *)
split.
replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
686
rewrite bpow_plus.
687 688
apply Rmult_le_compat_r.
apply bpow_ge_0.
689
assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
690 691 692 693 694 695
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zfloor_lub.
rewrite Hf.
696
rewrite bpow_plus.
697 698 699 700 701 702
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.
703
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
704 705 706 707 708 709
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.
710
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
711 712
apply Zceil_ub.
pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
713
rewrite bpow_plus.
714 715
apply Rmult_le_compat_r.
apply bpow_ge_0.
716
assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
717 718 719 720 721 722 723
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zceil_glb.
rewrite Hf.
unfold Zminus.
724
rewrite bpow_plus.
725 726 727 728 729 730
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hx.
Qed.

731
Theorem round_bounded_small_pos :
732 733 734
  forall x ex,
  (ex <= fexp ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
735
  round x = R0 \/ round x = bpow (fexp ex).
736 737
Proof.
intros x ex He Hx.
738
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
739
rewrite (canonic_exp_fexp_pos _ _ Hx).
740
unfold F2R. simpl.
741
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr.
742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758
(* 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.

759
Theorem generic_format_round_pos :
760 761
  forall x,
  (0 < x)%R ->
762
  generic_format (round x).
763 764 765 766 767 768 769
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 *)
770
destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr.
771 772
apply generic_format_0.
apply generic_format_bpow.
773
now apply valid_exp.
774
(* large *)
775
generalize (round_bounded_large_pos _ _ He Hex).
776
intros (Hr1, Hr2).
777
destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
778 779
rewrite <- (Rle_antisym _ _ Hr Hr2).
apply generic_format_bpow.
780
now apply valid_exp.
781 782
assert (Hr' := conj Hr1 Hr).
unfold generic_format, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
783
rewrite (canonic_exp_fexp_pos _ _ Hr').
784
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
785
rewrite (canonic_exp_fexp_pos _ _ Hex).
786
unfold F2R at 3. simpl.
787
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
788 789 790
now rewrite Ztrunc_Z2R.
Qed.

791
End Fcore_generic_round_pos.
792

793
Theorem round_ext :
794
  forall rnd1 rnd2,
795
  ( forall x, rnd1 x = rnd2 x ) ->
796
  forall x,
797
  round rnd1 x = round rnd2 x.
798 799
Proof.
intros rnd1 rnd2 Hext x.
800
unfold round.
801 802 803
now rewrite Hext.
Qed.

804
Section Zround_opp.
805

806 807
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
808

809
Definition Zrnd_opp x := Zopp (rnd (-x)).
810

811 812 813 814
Global Instance valid_rnd_opp : Valid_rnd Zrnd_opp.
Proof with auto with typeclass_instances.
split.
(* *)
815
intros x y Hxy.
816
unfold Zrnd_opp.
817 818
apply Zopp_le_cancel.
rewrite 2!Zopp_involutive.
819
apply Zrnd_le...
820
now apply Ropp_le_contravar.
821
(* *)
822
intros n.
823
unfold Zrnd_opp.
824
rewrite <- Z2R_opp, Zrnd_Z2R...
825 826 827
apply Zopp_involutive.
Qed.

828
Theorem round_opp :
829
  forall x,
830
  round rnd (- x) = Ropp (round Zrnd_opp x).
831 832
Proof.
intros x.
833
unfold round.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
834
rewrite <- F2R_Zopp, canonic_exp_opp, scaled_mantissa_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
835
apply F2R_eq_compat.
836 837 838 839
apply sym_eq.
exact (Zopp_involutive _).
Qed.

840
End Zround_opp.
841

842
(** IEEE-754 roundings: up, down and to zero *)
843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864

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.

865 866 867 868 869 870 871
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Proof.
split.
apply Zaway_le.
apply Zaway_Z2R.
Qed.

872 873 874 875
Section monotone.

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

877
Theorem round_DN_or_UP :
878 879
  forall x,
  round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
880
Proof.
881
intros x.
882
unfold round.
883
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx].
884 885 886 887
left. now rewrite Hx.
right. now rewrite Hx.
Qed.

888 889 890 891 892 893 894 895 896 897 898
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.

899
Theorem round_le :
900 901 902
  forall x y, (x <= y)%R -> (round rnd x <= round rnd y)%R.
Proof with auto with typeclass_instances.
intros x y Hxy.
903
destruct (total_order_T x 0) as [[Hx|Hx]|Hx].
904
3: now apply round_le_pos.
905
(* x < 0 *)
906
unfold round.
907 908 909 910
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
911
rewrite (canonic_exp_opp (-x)), (canonic_exp_opp (-y)).
912
apply Ropp_le_cancel.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
913
rewrite <- 2!F2R_Zopp.
914
apply (round_le_pos (Zrnd_opp rnd) (-y) (-x)).
915 916 917 918 919 920
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.
921
rewrite <- (Zrnd_Z2R rnd 0).
922
apply Zrnd_le...
923
simpl.
924
rewrite <- (Rmult_0_l (bpow (- fexp (ln_beta beta x)))).
925 926 927 928
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply Rlt_le.
apply F2R_ge_0_compat. simpl.
929
rewrite <- (Zrnd_Z2R rnd 0).
930
apply Zrnd_le...
931 932 933 934 935
apply Rmult_le_pos.
exact Hy.
apply bpow_ge_0.
(* x = 0 *)
rewrite Hx.
936
rewrite round_0...
937 938
apply F2R_ge_0_compat.
simpl.
939
rewrite <- (Zrnd_Z2R rnd 0).
940
apply Zrnd_le...
941 942 943 944 945
apply Rmult_le_pos.
now rewrite <- Hx.
apply bpow_ge_0.
Qed.

946
Theorem round_ge_generic :
947
  forall x y, generic_format x -> (x <= y)%R -> (x <= round rnd y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
948
Proof.
949
intros x y Hx Hxy.
950
rewrite <- (round_generic rnd x Hx).
951
now apply round_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
952
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
953

954
Theorem round_le_generic :
955
  forall x y, generic_format y -> (x <= y)%R -> (round rnd x <= y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
956
Proof.