Fcore_generic_fmt.v 51.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
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
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.



198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214
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.

215
Theorem scaled_mantissa_generic :
216 217
  forall x,
  generic_format x ->
218
  scaled_mantissa x = Z2R (Ztrunc (scaled_mantissa x)).
219 220
Proof.
intros x Hx.
221
unfold scaled_mantissa.
222 223
pattern x at 1 3 ; rewrite Hx.
unfold F2R. simpl.
224
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
225 226 227
now rewrite Ztrunc_Z2R.
Qed.

228
Theorem scaled_mantissa_mult_bpow :
229
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
230
  (scaled_mantissa x * bpow (canonic_exp x))%R = x.
231 232 233
Proof.
intros x.
unfold scaled_mantissa.
234
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
235 236 237
apply Rmult_1_r.
Qed.

238 239 240 241 242 243
Theorem scaled_mantissa_0 :
  scaled_mantissa 0 = R0.
Proof.
apply Rmult_0_l.
Qed.

244 245 246 247 248 249
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
250
rewrite canonic_exp_opp.
251 252 253
now rewrite Ropp_mult_distr_l_reverse.
Qed.

254 255 256 257 258 259
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
260
rewrite canonic_exp_abs, Rabs_mult.
261 262 263 264 265 266
apply f_equal.
apply sym_eq.
apply Rabs_pos_eq.
apply bpow_ge_0.
Qed.

267 268 269 270 271
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
272
rewrite scaled_mantissa_opp, canonic_exp_opp.
273
rewrite Ztrunc_opp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
274
rewrite F2R_Zopp.
275
now apply f_equal.
276 277
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
278 279 280 281 282
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
283
rewrite scaled_mantissa_abs, canonic_exp_abs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
284
rewrite Ztrunc_abs.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
285
rewrite F2R_Zabs.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
286 287 288
now apply f_equal.
Qed.

289 290 291 292 293 294
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
295
rewrite scaled_mantissa_opp, canonic_exp_opp, Ztrunc_opp.
296 297
intros H.
rewrite <- (Ropp_involutive x) at 1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
298
rewrite H, F2R_Zopp.
299 300 301 302
apply Ropp_involutive.
easy.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
303
Theorem canonic_exp_fexp :
304
  forall x ex,
305
  (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
306
  canonic_exp x = fexp ex.
307 308
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
309
unfold canonic_exp.
310 311 312
now rewrite ln_beta_unique with (1 := Hx).
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
313
Theorem canonic_exp_fexp_pos :
314
  forall x ex,
315
  (bpow (ex - 1) <= x < bpow ex)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
316
  canonic_exp x = fexp ex.
317 318
Proof.
intros x ex Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
319
apply canonic_exp_fexp.
320 321
rewrite Rabs_pos_eq.
exact Hx.
322 323 324 325
apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.

326
(** Properties when the real number is "small" (kind of subnormal) *)
327 328 329 330 331 332 333
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.
334
split.
335 336 337 338 339 340
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.
341
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_l.
342 343
rewrite Rmult_1_r, Rmult_1_l.
apply Rlt_le_trans with (1 := proj2 Hx).
344
now apply bpow_le.
345 346
Qed.

347 348 349 350 351 352 353 354 355 356 357 358
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
359 360
rewrite canonic_exp_abs.
unfold canonic_exp.
361 362 363 364 365 366 367 368
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).
369
now rewrite (proj2 (proj2 (valid_exp _) He)).
370 371
Qed.

372 373 374 375 376 377 378 379 380 381 382 383 384 385 386
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.

387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410
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.

411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
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.
433 434
Qed.

435
(** Generic facts about any format *)
436 437
Theorem generic_format_discrete :
  forall x m,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
438
  let e := canonic_exp x in
439 440 441 442 443 444 445 446 447 448 449 450 451
  (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.
452
now rewrite scaled_mantissa_mult_bpow.
453 454
Qed.

455 456 457 458 459 460
Theorem generic_format_canonic :
  forall f, canonic f ->
  generic_format (F2R f).
Proof.
intros (m, e) Hf.
unfold canonic in Hf. simpl in Hf.
461
unfold generic_format, scaled_mantissa.
462
rewrite <- Hf.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
463
apply F2R_eq_compat.
464
unfold F2R. simpl.
465
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
466 467 468
now rewrite Ztrunc_Z2R.
Qed.

469 470 471 472 473 474 475 476 477 478 479 480 481
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
482
apply F2R_gt_0_reg with beta (canonic_exp x).
483 484 485
now rewrite <- Fx.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
486
Theorem abs_lt_bpow_prec:
487
  forall prec,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
488
  (forall e, (e - prec <= fexp e)%Z) ->
489
  (* OK with FLX, FLT and FTZ *)
490
  forall x,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
491 492
  (Rabs x < bpow (prec + canonic_exp x))%R.
intros prec Hp x.
493 494 495
case (Req_dec x 0); intros Hxz.
rewrite Hxz, Rabs_R0.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
496
unfold canonic_exp.
497 498 499
destruct (ln_beta beta x) as (ex,Ex) ; simpl.
specialize (Ex Hxz).
apply Rlt_le_trans with (1 := proj2 Ex).
500
apply bpow_le.
501
specialize (Hp ex).
502 503 504
omega.
Qed.

505
Theorem generic_format_bpow_inv' :
BOLDO Sylvie's avatar
BOLDO Sylvie committed
506
  forall e,
507 508
  generic_format (bpow e) ->
  (fexp (e + 1) <= e)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
509 510
Proof.
intros e He.
511 512 513 514 515
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
516
rewrite Ztrunc_floor.
517 518 519 520
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
521
split.
522 523 524 525 526 527 528 529 530 531 532 533 534
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
535 536 537
omega.
Qed.

538
Section Fcore_generic_round_pos.
539

BOLDO Sylvie's avatar
BOLDO Sylvie committed
540
(** Rounding functions: R -> Z *)
541 542 543 544

Variable rnd : R -> Z.

Class Valid_rnd := {
545
  Zrnd_le : forall x y, (x <= y)%R -> (rnd x <= rnd y)%Z ;
546
  Zrnd_Z2R : forall n, rnd (Z2R n) = n
547 548
}.

549
Context { valid_rnd : Valid_rnd }.
550

551
Theorem Zrnd_DN_or_UP :
552
  forall x, rnd x = Zfloor x \/ rnd x = Zceil x.
553
Proof.
554
intros x.
555
destruct (Zle_or_lt (rnd x) (Zfloor x)) as [Hx|Hx].
556 557
left.
apply Zle_antisym with (1 := Hx).
558
rewrite <- (Zrnd_Z2R (Zfloor x)).
559
apply Zrnd_le.
560 561 562
apply Zfloor_lb.
right.
apply Zle_antisym.
563
rewrite <- (Zrnd_Z2R (Zceil x)).
564
apply Zrnd_le.
565 566 567 568 569 570 571 572 573
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.

574 575 576 577 578 579 580 581 582 583 584 585 586
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
587
(** the most useful one: R -> F *)
588
Definition round x :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
589
  F2R (Float beta (rnd (scaled_mantissa x)) (canonic_exp x)).
590

591
Theorem round_le_pos :
592
  forall x y, (0 < x)%R -> (x <= y)%R -> (round x <= round y)%R.
593
Proof.
594
intros x y Hx Hxy.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
595
unfold round, scaled_mantissa, canonic_exp.
596 597 598 599 600 601 602 603 604 605
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.
606
apply (lt_bpow beta).
607 608 609 610
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].
611
rewrite (proj2 (proj2 (valid_exp ey) Hy1) ex).
612
apply F2R_le_compat.
613
apply Zrnd_le.
614 615 616 617 618 619
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].
620
rewrite (proj2 (proj2 (valid_exp ex) (Zle_trans _ _ _ He Hx2)) ey Hx2).
621
apply F2R_le_compat.
622
apply Zrnd_le.
623 624 625
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
626
apply Rle_trans with (F2R (Float beta (rnd (bpow (ey - 1) * bpow (- fexp ey))) (fexp ey))).
627
rewrite <- bpow_plus.
628 629 630 631 632
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.
633
rewrite <- (Zrnd_Z2R 1).
634
apply Zrnd_le.
635 636 637 638
apply Rlt_le.
exact (proj2 (mantissa_small_pos _ _ Hex Hx1)).
unfold F2R. simpl.
rewrite Z2R_Zpower. 2: omega.
639
rewrite <- bpow_plus, Rmult_1_l.
640
apply bpow_le.
641
omega.
642
apply Rle_trans with (F2R (Float beta (rnd (bpow ex * bpow (- fexp ex))) (fexp ex))).
643
apply F2R_le_compat.
644
apply Zrnd_le.
645 646 647 648
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hex.
649
rewrite <- bpow_plus.
650 651 652 653
rewrite <- Z2R_Zpower. 2: omega.
rewrite Zrnd_Z2R.
unfold F2R. simpl.
rewrite 2!Z2R_Zpower ; try omega.
654
rewrite <- 2!bpow_plus.
655
apply bpow_le.
656 657
omega.
apply F2R_le_compat.
658
apply Zrnd_le.
659 660 661 662 663
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Hey.
rewrite He'.
apply F2R_le_compat.
664
apply Zrnd_le.
665 666 667 668 669
apply Rmult_le_compat_r.
apply bpow_ge_0.
exact Hxy.
Qed.

670
Theorem round_generic :
671 672
  forall x,
  generic_format x ->
673
  round x = x.
674 675
Proof.
intros x Hx.
676
unfold round.
677 678 679 680 681
rewrite scaled_mantissa_generic with (1 := Hx).
rewrite Zrnd_Z2R.
now apply sym_eq.
Qed.

682 683
Theorem round_0 :
  round 0 = R0.
684
Proof.
685
unfold round, scaled_mantissa.
686 687 688 689 690 691
rewrite Rmult_0_l.
fold (Z2R 0).
rewrite Zrnd_Z2R.
apply F2R_0.
Qed.

692
Theorem round_bounded_large_pos :
693 694 695
  forall x ex,
  (fexp ex < ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
696
  (bpow (ex - 1) <= round x <= bpow ex)%R.
697 698
Proof.
intros x ex He Hx.
699
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
700
rewrite (canonic_exp_fexp_pos _ _ Hx).
701
unfold F2R. simpl.
702
destruct (Zrnd_DN_or_UP (x * bpow (- fexp ex))) as [Hr|Hr] ; rewrite Hr.
703 704 705
(* DN *)
split.
replace (ex - 1)%Z with (ex - 1 + - fexp ex + fexp ex)%Z by ring.
706
rewrite bpow_plus.
707 708
apply Rmult_le_compat_r.
apply bpow_ge_0.
709
assert (Hf: Z2R (Zpower beta (ex - 1 - fexp ex)) = bpow (ex - 1 + - fexp ex)).
710 711 712 713 714 715
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zfloor_lub.
rewrite Hf.
716
rewrite bpow_plus.
717 718 719 720 721 722
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.
723
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
724 725 726 727 728 729
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.
730
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
731 732
apply Zceil_ub.
pattern ex at 3 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
733
rewrite bpow_plus.
734 735
apply Rmult_le_compat_r.
apply bpow_ge_0.
736
assert (Hf: Z2R (Zpower beta (ex - fexp ex)) = bpow (ex - fexp ex)).
737 738 739 740 741 742 743
apply Z2R_Zpower.
omega.
rewrite <- Hf.
apply Z2R_le.
apply Zceil_glb.
rewrite Hf.
unfold Zminus.
744
rewrite bpow_plus.
745 746 747 748 749 750
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rlt_le.
apply Hx.
Qed.

751
Theorem round_bounded_small_pos :
752 753 754
  forall x ex,
  (ex <= fexp ex)%Z ->
  (bpow (ex - 1) <= x < bpow ex)%R ->
755
  round x = R0 \/ round x = bpow (fexp ex).
756 757
Proof.
intros x ex He Hx.
758
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
759
rewrite (canonic_exp_fexp_pos _ _ Hx).
760
unfold F2R. simpl.
761
destruct (Zrnd_DN_or_UP (x * bpow (-fexp ex))) as [Hr|Hr] ; rewrite Hr.
762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778
(* 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.

779
Theorem generic_format_round_pos :
780 781
  forall x,
  (0 < x)%R ->
782
  generic_format (round x).
783 784 785 786 787 788 789
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 *)
790
destruct (round_bounded_small_pos _ _ He Hex) as [Hr|Hr] ; rewrite Hr.
791 792
apply generic_format_0.
apply generic_format_bpow.
793
now apply valid_exp.
794
(* large *)
795
generalize (round_bounded_large_pos _ _ He Hex).
796
intros (Hr1, Hr2).
797
destruct (Rle_or_lt (bpow ex) (round x)) as [Hr|Hr].
798 799
rewrite <- (Rle_antisym _ _ Hr Hr2).
apply generic_format_bpow.
800
now apply valid_exp.
801 802
assert (Hr' := conj Hr1 Hr).
unfold generic_format, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
803
rewrite (canonic_exp_fexp_pos _ _ Hr').
804
unfold round, scaled_mantissa.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
805
rewrite (canonic_exp_fexp_pos _ _ Hex).
806
unfold F2R at 3. simpl.
807
rewrite Rmult_assoc, <- bpow_plus, Zplus_opp_r, Rmult_1_r.
808 809 810
now rewrite Ztrunc_Z2R.
Qed.

811
End Fcore_generic_round_pos.
812

813
Theorem round_ext :
814
  forall rnd1 rnd2,
815
  ( forall x, rnd1 x = rnd2 x ) ->
816
  forall x,
817
  round rnd1 x = round rnd2 x.
818 819
Proof.
intros rnd1 rnd2 Hext x.
820
unfold round.
821 822 823
now rewrite Hext.
Qed.

824
Section Zround_opp.
825

826 827
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
828

829
Definition Zrnd_opp x := Zopp (rnd (-x)).
830

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

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

860
End Zround_opp.
861

862
(** IEEE-754 roundings: up, down and to zero *)
863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884

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.

885 886 887 888 889 890 891
Global Instance valid_rnd_AW : Valid_rnd Zaway.
Proof.
split.
apply Zaway_le.
apply Zaway_Z2R.
Qed.

892 893 894 895
Section monotone.

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

897
Theorem round_DN_or_UP :
898 899
  forall x,
  round rnd x = round Zfloor x \/ round rnd x = round Zceil x.
900
Proof.
901
intros x.
902
unfold round.
903
destruct (Zrnd_DN_or_UP rnd (scaled_mantissa x)) as [Hx|Hx].
904 905 906 907
left. now rewrite Hx.
right. now rewrite Hx.
Qed.

908 909 910 911 912 913 914 915 916 917 918
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.

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

966
Theorem round_ge_generic :
967
  forall x y, generic_format x -> (x <= y)%R -> (x <= round rnd y)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
968
Proof.
969
intros x y Hx Hxy.
970
rewrite <- (round_generic rnd x Hx).