Fcore_generic_fmt.v 17.3 KB
Newer Older
1 2 3 4
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5 6 7 8 9

Section RND_generic.

Variable beta : radix.

10
Notation bpow e := (bpow beta e).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
11 12 13

Variable fexp : Z -> Z.

14 15 16 17 18 19 20 21
Definition valid_exp :=
  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 ).

Variable prop_exp : valid_exp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
22

23 24 25 26 27
Definition canonic_exponent x :=
  fexp (projT1 (ln_beta beta x)).

Definition canonic (f : float beta) :=
  Fexp f = canonic_exponent (F2R f).
28

Guillaume Melquiond's avatar
Guillaume Melquiond committed
29
Definition generic_format (x : R) :=
30 31 32 33 34 35 36 37 38 39 40
  x = F2R (Float beta (Ztrunc (x * bpow (- canonic_exponent x))) (canonic_exponent x)).

(*
Theorem canonic_mantissa_0 :
  canonic_mantissa 0 = Z0.
Proof.
unfold canonic_mantissa.
rewrite Rmult_0_l.
exact (Zfloor_Z 0).
Qed.
*)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
41

Guillaume Melquiond's avatar
Guillaume Melquiond committed
42 43 44
Theorem generic_format_0 :
  generic_format 0.
Proof.
45 46 47 48 49 50 51 52 53 54 55 56 57
unfold generic_format.
rewrite Rmult_0_l.
change (Ztrunc 0) with (Ztrunc (Z2R 0)).
now rewrite Ztrunc_Z2R, F2R_0.
Qed.

Theorem canonic_exponent_opp :
  forall x,
  canonic_exponent (-x) = canonic_exponent x.
Proof.
intros x.
unfold canonic_exponent.
now rewrite ln_beta_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
58 59
Qed.

60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
(*
Theorem canonic_mantissa_opp :
  forall x,
  generic_format x ->
  canonic_mantissa (-x) = (- canonic_mantissa x)%Z.
Proof.
unfold generic_format, canonic_mantissa.
intros x Hx.
rewrite canonic_exponent_opp.
rewrite Hx at 1 3.
generalize (canonic_exponent x).
intros e.
clear.
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r.
rewrite Rmult_1_r.
rewrite <- opp_Z2R.
now rewrite 2!Zfloor_Z.
Qed.
*)

82 83 84 85 86
Theorem generic_format_bpow :
  forall e, (fexp (e + 1) <= e)%Z ->
  generic_format (bpow e).
Proof.
intros e H.
87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
unfold generic_format, canonic_exponent.
rewrite ln_beta_bpow.
rewrite <- bpow_add.
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.
omega.
Qed.

Theorem generic_format_canonic_exponent :
  forall m e,
  (canonic_exponent (F2R (Float beta m e)) <= e)%Z ->
  generic_format (F2R (Float beta m e)).
Proof.
intros m e.
unfold generic_format.
set (e' := canonic_exponent (F2R (Float beta m e))).
intros He.
unfold F2R at 3. simpl.
assert (H: (Z2R m * bpow e * bpow (- e') = Z2R (m * Zpower (radix_val beta) (e + -e')))%R).
rewrite Rmult_assoc, <- bpow_add, mult_Z2R.
rewrite Z2R_Zpower.
apply refl_equal.
now apply Zle_left.
rewrite H, Ztrunc_Z2R.
unfold F2R. simpl.
rewrite <- H.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l.
now rewrite Rmult_1_r.
Qed.

Theorem canonic_opp :
  forall m e,
  canonic (Float beta m e) ->
  canonic (Float beta (-m) e).
Proof.
intros m e H.
unfold canonic.
now rewrite <- opp_F2R, canonic_exponent_opp.
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.

Theorem generic_format_opp :
  forall x, generic_format x -> generic_format (-x).
Proof.
intros x Hx.
unfold generic_format.
rewrite canonic_exponent_opp.
pattern x at 2 ; rewrite Hx.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse, <- opp_Z2R.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
rewrite Ztrunc_Z2R.
rewrite opp_Z2R, Ropp_mult_distr_l_reverse.
now apply f_equal.
Qed.

Theorem canonic_exponent_fexp_pos :
  forall x ex,
  (bpow (ex - 1) <= x < bpow ex)%R ->
  canonic_exponent x = fexp ex.
Proof.
intros x ex Hx.
unfold canonic_exponent.
rewrite <- (Rabs_pos_eq x) in Hx.
now rewrite ln_beta_unique with (1 := Hx).
apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.

Theorem canonic_exponent_fexp_neg :
  forall x ex,
  (bpow (ex - 1) <= -x < bpow ex)%R ->
  canonic_exponent x = fexp ex.
Proof.
intros x ex Hx.
unfold canonic_exponent.
rewrite <- (Rabs_left1 x) in Hx.
now rewrite ln_beta_unique with (1 := Hx).
apply Ropp_le_cancel.
rewrite Ropp_0.
apply Rle_trans with (2 := proj1 Hx).
apply bpow_ge_0.
Qed.

Theorem canonic_exponent_fexp :
  forall x ex,
  (bpow (ex - 1) <= Rabs x < bpow ex)%R ->
  canonic_exponent x = fexp ex.
Proof.
intros x ex Hx.
unfold canonic_exponent.
now rewrite ln_beta_unique with (1 := Hx).
Qed.

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.
207
split.
208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
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.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_l.
rewrite Rmult_1_r, Rmult_1_l.
apply Rlt_le_trans with (1 := proj2 Hx).
now apply -> bpow_le.
Qed.

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.
242 243
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
244
Theorem generic_DN_pt_large_pos_ge_pow_aux :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
245 246
  forall x ex,
  (fexp ex < ex)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
247 248
  (bpow (ex - 1) <= x)%R ->
  (bpow (ex - 1) <= F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
249
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
250
intros x ex He1 Hx1.
251
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
252
replace (ex - 1)%Z with ((ex - 1 - fexp ex) + fexp ex)%Z by ring.
253
rewrite bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
254
apply Rmult_le_compat_r.
255
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
256
assert (Hx2 : bpow (ex - 1 - fexp ex) = Z2R (Zpower (radix_val beta) (ex - 1 - fexp ex))).
257 258 259 260 261 262 263 264
apply sym_eq.
apply Z2R_Zpower.
omega.
rewrite Hx2.
apply Z2R_le.
apply Zfloor_lub.
rewrite <- Hx2.
unfold Zminus at 1.
265
rewrite bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
266
apply Rmult_le_compat_r.
267
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
268
exact Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
269 270
Qed.

271 272 273 274 275 276 277 278 279 280 281 282 283 284
Theorem generic_format_canonic :
  forall f, canonic f ->
  generic_format (F2R f).
Proof.
intros (m, e) Hf.
unfold canonic in Hf. simpl in Hf.
unfold generic_format.
rewrite <- Hf.
apply (f_equal (fun m => F2R (Float beta m e))).
unfold F2R. simpl.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
now rewrite Ztrunc_Z2R.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
285
Theorem generic_DN_pt_pos :
286 287
  forall x, (0 < x)%R ->
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (- canonic_exponent x))) (canonic_exponent x))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
288
Proof.
289 290 291 292 293 294
intros x H0x.
unfold canonic_exponent.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rgt_not_eq _ _ H0x)).
rewrite (Rabs_pos_eq _ (Rlt_le _ _ H0x)) in He.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
295 296
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - positive big enough *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
297
assert (Hbl : (bpow (ex - 1) <= F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)))%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
298
now apply generic_DN_pt_large_pos_ge_pow_aux.
299
(* - . smaller *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
300
assert (Hrx : (F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)) <= x)%R).
301
unfold F2R. simpl.
302 303 304
apply Rmult_le_reg_r with (bpow (- fexp ex)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
305
apply Zfloor_lb.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
306 307
split.
(* - . rounded *)
308
apply generic_format_canonic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
309
apply sym_eq.
310
apply canonic_exponent_fexp_pos.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
311 312
split.
exact Hbl.
313
now apply Rle_lt_trans with (2 := proj2 He).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
314
split.
315
exact Hrx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
316
(* - . biggest *)
317
intros g Hg Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
318 319 320
destruct (Rle_or_lt g R0) as [Hg3|Hg3].
apply Rle_trans with (2 := Hbl).
apply Rle_trans with (1 := Hg3).
321
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
322 323
apply Rnot_lt_le.
intros Hrg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
324
assert (bpow (ex - 1) <= g < bpow ex)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
325 326 327 328
split.
apply Rle_trans with (1 := Hbl).
now apply Rlt_le.
now apply Rle_lt_trans with (1 := Hgx).
329 330
assert (Hcg: canonic_exponent g = fexp ex).
unfold canonic_exponent.
331
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in H.
332
now rewrite ln_beta_unique with (1 := H).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
333
apply Rlt_not_le with (1 := Hrg).
334 335
rewrite Hg.
rewrite Hcg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
336
apply F2R_le_compat.
337
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
338
apply Rmult_le_reg_r with (bpow (fexp ex)).
339
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
340
rewrite Rmult_assoc.
341
rewrite <- bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
342 343
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
344 345
rewrite <- Hcg.
now rewrite Hg in Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
346
(* - positive too small *)
347
rewrite mantissa_DN_small_pos with (1 := He) (2 := He1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
348
rewrite F2R_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
349
split.
350
(* - . rounded *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
351
exact generic_format_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
352
split.
353
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
354
(* - . biggest *)
355
intros g Hg Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
356 357
apply Rnot_lt_le.
intros Hg3.
358 359
destruct (ln_beta beta g) as (ge, Hg4).
simpl in Hg.
360
specialize (Hg4 (Rgt_not_eq _ _ Hg3)).
361 362 363
assert (Hcg: canonic_exponent g = fexp ge).
unfold canonic_exponent.
now rewrite ln_beta_unique with (1 := Hg4).
364
rewrite Rabs_pos_eq in Hg4.
365 366
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx (proj2 He))).
apply Rle_trans with (bpow (fexp ge)).
367
apply -> bpow_le.
368
rewrite (proj2 (proj2 (prop_exp ex) He1) ge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
369 370
exact He1.
apply Zle_trans with (2 := He1).
371
cut (ge - 1 < ex)%Z. omega.
372
apply <- bpow_lt.
373
apply Rle_lt_trans with (2 := proj2 He).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
374 375
apply Rle_trans with (2 := Hgx).
exact (proj1 Hg4).
376
rewrite Hg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
377
rewrite <- F2R_bpow.
378
rewrite Hcg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
379
apply F2R_le_compat.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
380
apply (Zlt_le_succ 0).
381 382 383
apply F2R_lt_reg with beta (fexp ge).
rewrite F2R_0, <- Hcg.
now rewrite Hg in Hg3.
384
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
385 386 387
Qed.

Theorem generic_DN_pt_neg :
388 389
  forall x, (x < 0)%R ->
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (- canonic_exponent x))) (canonic_exponent x))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
390
Proof.
391 392 393 394 395 396
intros x Hx0.
unfold canonic_exponent.
destruct (ln_beta beta x) as (ex, He).
simpl.
specialize (He (Rlt_not_eq _ _ Hx0)).
rewrite (Rabs_left _ Hx0) in He.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
397
assert (Hbr : (F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)) <= x)%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
398 399
(* - bounded right *)
unfold F2R. simpl.
400 401 402
apply Rmult_le_reg_r with (bpow (-fexp ex)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
403
apply Zfloor_lb.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
404 405
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - negative big enough *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
406
assert (Hbl : (- bpow ex <= F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)))%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
407 408
(* - . bounded left *)
unfold F2R. simpl.
409 410 411 412 413 414
apply Rmult_le_reg_r with (bpow (-fexp ex)).
apply bpow_gt_0.
rewrite Rmult_assoc, <- bpow_add, Zplus_opp_r, Rmult_1_r.
assert (Hp : (- bpow ex * bpow (-fexp ex) = Z2R (- Zpower (radix_val beta) (ex - fexp ex)))%R).
rewrite Ropp_mult_distr_l_reverse.
rewrite <- bpow_add, <- Z2R_Zpower.
415
now rewrite opp_Z2R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
416
omega.
417 418 419
rewrite Hp.
apply Z2R_le.
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
420
rewrite <- Hp.
421
apply Rmult_le_compat_r.
422
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
423 424
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
425 426 427 428 429
now apply Rlt_le.
split.
(* - . rounded *)
destruct (Rle_lt_or_eq_dec _ _ Hbl) as [Hbl2|Hbl2].
(* - . . not a radix power *)
430 431
apply generic_format_canonic.
assert (Hb: (bpow (ex - 1) <= - F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)) < bpow ex)%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
432
split.
433 434
apply Rle_trans with (1 := proj1 He).
now apply Ropp_le_contravar.
435 436
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
437 438
apply sym_eq.
apply canonic_exponent_fexp_neg with (1 := Hb).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
439 440
(* - . . a radix power *)
rewrite <- Hbl2.
441 442 443
apply generic_format_opp.
apply generic_format_bpow.
exact (proj1 (prop_exp _) He1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
444 445 446
split.
exact Hbr.
(* - . biggest *)
447
intros g Hg Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
448 449 450 451
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
452
destruct (ln_beta beta g) as (ge, Hge).
453
specialize (Hge (Rlt_not_eq _ _ Hg4)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
454
apply Rlt_not_le with (1 := Hg3).
455 456
rewrite Hg.
assert (Hge' : ge = ex).
457
apply bpow_unique with (1 := Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
458
split.
459
apply Rle_trans with (1 := proj1 He).
460
rewrite Rabs_left with (1 := Hg4).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
461 462
now apply Ropp_le_contravar.
apply Ropp_lt_cancel.
463 464 465
rewrite Rabs_left with (1 := Hg4).
rewrite Ropp_involutive.
now apply Rle_lt_trans with (1 := Hbl).
466 467 468 469 470
assert (Hcg: canonic_exponent g = fexp ex).
rewrite <- Hge'.
now apply canonic_exponent_fexp.
rewrite Hcg.
apply F2R_le_compat.
471
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
472
apply Rmult_le_reg_r with (bpow (fexp ex)).
473
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
474
rewrite Rmult_assoc.
475 476 477
rewrite <- bpow_add, Zplus_opp_l, Rmult_1_r.
rewrite <- Hcg.
now rewrite Hg in Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478
(* - negative too small *)
479 480 481 482 483
rewrite <- (Zopp_involutive (Zfloor (x * bpow (- fexp ex)))).
rewrite <- (Ropp_involutive x) at 2.
rewrite Ropp_mult_distr_l_reverse.
change (- Zfloor (- (- x * bpow (- fexp ex))))%Z with (Zceil (- x * bpow (- fexp ex)))%Z.
rewrite mantissa_UP_small_pos ; try assumption.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
484 485 486 487 488
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
rewrite Rmult_1_l.
(* - . rounded *)
split.
489 490 491
apply generic_format_opp.
apply generic_format_bpow.
exact (proj1 (proj2 (prop_exp _) He1)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
492 493
split.
(* - . smaller *)
494 495
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
496
apply Rlt_le.
497
apply Rlt_le_trans with (1 := proj2 He).
498
now apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
499
(* - . biggest *)
500
intros g Hg Hgx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
501 502 503 504
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
505 506
destruct (ln_beta beta g) as (ge, Hge).
simpl in Hg.
507
specialize (Hge (Rlt_not_eq g 0 Hg4)).
508
rewrite (Rabs_left _ Hg4) in Hge.
509 510
assert (Hge' : (ge <= fexp ex)%Z).
cut (ge - 1 < fexp ex)%Z. omega.
511
apply <- bpow_lt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
512 513 514
apply Rle_lt_trans with (1 := proj1 Hge).
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
515 516 517 518 519
assert (Hcg: canonic_exponent g = fexp ex).
unfold canonic_exponent.
rewrite <- Rabs_left with (1 := Hg4) in Hge.
rewrite ln_beta_unique with (1 := Hge).
exact (proj2 (proj2 (prop_exp _) He1) _ Hge').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
520
apply Rlt_not_le with (1 := proj2 Hge).
521
rewrite Hg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
522 523
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
524 525
rewrite Hcg.
pattern (fexp ex) at 2 ; replace (fexp ex) with (fexp ex - ge + ge)%Z by ring.
526
rewrite bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
527
rewrite <- Rmult_assoc.
528
pattern (bpow ge) at 1 ; rewrite <- Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
529
apply Rmult_le_compat_r.
530
apply bpow_ge_0.
531 532 533 534 535 536
assert (- Z2R (Ztrunc (g * bpow (- fexp ex))) * bpow (fexp ex - ge) = Z2R (- Ztrunc (g * bpow (-fexp ex)) * Zpower (radix_val beta) (fexp ex - ge)))%R.
rewrite mult_Z2R.
rewrite Z2R_Zpower. 2: omega.
now rewrite opp_Z2R.
rewrite H.
apply (Z2R_le 1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
537 538
apply (Zlt_le_succ 0).
apply lt_Z2R.
539 540 541 542
rewrite <- H.
unfold Zminus.
rewrite bpow_add, <- Rmult_assoc.
apply Rmult_lt_0_compat.
543
rewrite <- Ropp_0.
544
rewrite Ropp_mult_distr_l_reverse.
545 546 547
apply Ropp_lt_contravar.
rewrite <- Hcg.
now rewrite Hg in Hg4.
548
apply bpow_gt_0.
549 550 551 552 553
Qed.

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.
Proof.
554
split.
555
(* symmetric set *)
556
exact generic_format_0.
557
exact generic_format_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
558
(* rounding down *)
559 560
intros x.
exists (match Req_EM_T x 0 with
561
  | left Hx => R0
562
  | right Hx => F2R (Float beta (Zfloor (x * bpow (- canonic_exponent x))) (canonic_exponent x))
Guillaume Melquiond's avatar
Guillaume Melquiond committed
563
  end).
564 565
destruct (Req_EM_T x 0) as [Hx|Hx].
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
566
split.
567 568
apply generic_format_0.
rewrite Hx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
569 570
split.
apply Rle_refl.
571 572 573
now intros g _ H.
(* . *)
destruct (ln_beta beta x) as (ex, H1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
574
simpl.
575 576
specialize (H1 Hx).
destruct (Rdichotomy _ _ Hx) as [H2|H2].
577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607
now apply generic_DN_pt_neg.
now apply generic_DN_pt_pos.
Qed.

Theorem generic_DN_pt :
  forall x,
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (- canonic_exponent x))) (canonic_exponent x))).
Proof.
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
now apply generic_DN_pt_pos.
rewrite <- Hx, Rmult_0_l.
fold (Z2R 0).
rewrite Zfloor_Z, F2R_0.
apply Rnd_DN_pt_refl.
apply generic_format_0.
now apply generic_DN_pt_neg.
Qed.

Theorem generic_UP_pt :
  forall x,
  Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (- canonic_exponent x))) (canonic_exponent x))).
Proof.
intros x.
apply Rnd_DN_UP_pt_sym.
apply generic_format_satisfies_any.
unfold Zceil.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite opp_F2R, Zopp_involutive.
rewrite <- canonic_exponent_opp.
apply generic_DN_pt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
608 609 610
Qed.

Theorem generic_DN_pt_small_pos :
611
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
612
  (bpow (ex - 1) <= x < bpow ex)%R ->
613 614 615 616
  (ex <= fexp ex)%Z ->
  Rnd_DN_pt generic_format x R0.
Proof.
intros x ex Hx He.
617 618 619 620
rewrite <- (F2R_0 beta (canonic_exponent x)).
rewrite <- mantissa_DN_small_pos with (1 := Hx) (2 := He).
rewrite <- canonic_exponent_fexp_pos with (1 := Hx).
apply generic_DN_pt.
621 622
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
623
Theorem generic_UP_pt_small_pos :
624
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
625
  (bpow (ex - 1) <= x < bpow ex)%R ->
626 627 628 629
  (ex <= fexp ex)%Z ->
  Rnd_UP_pt generic_format x (bpow (fexp ex)).
Proof.
intros x ex Hx He.
630 631 632 633
rewrite <- F2R_bpow.
rewrite <- mantissa_UP_small_pos with (1 := Hx) (2 := He).
rewrite <- canonic_exponent_fexp_pos with (1 := Hx).
apply generic_UP_pt.
634 635
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
636
Theorem generic_UP_pt_large_pos_le_pow :
637
  forall x xu ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
638
  (bpow (ex - 1) <= x < bpow ex)%R ->
639 640 641 642
  (fexp ex < ex)%Z ->
  Rnd_UP_pt generic_format x xu ->
  (xu <= bpow ex)%R.
Proof.
643 644 645 646
intros x xu ex Hx He (_, (_, Hu4)).
apply Hu4 with (2 := Rlt_le _ _ (proj2 Hx)).
apply generic_format_bpow.
exact (proj1 (prop_exp _) He).
647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667
Qed.

Theorem generic_format_EM :
  forall x,
  generic_format x \/ ~generic_format x.
Proof.
intros x.
destruct (proj1 (satisfies_any_imp_DN _ generic_format_satisfies_any) x) as (d, Hd).
destruct (Rle_lt_or_eq_dec d x) as [Hxd|Hxd].
apply Hd.
right.
intros Fx.
apply Rlt_not_le with (1 := Hxd).
apply Req_le.
apply sym_eq.
now apply Rnd_DN_pt_idempotent with (1 := Hd).
left.
rewrite <- Hxd.
apply Hd.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696
Theorem generic_DN_pt_large_pos_ge_pow :
  forall x d e,
  (0 < d)%R ->
  Rnd_DN_pt generic_format x d ->
  (bpow e <= x)%R ->
  (bpow e <= d)%R.
Proof.
intros x d e Hd Hxd Hex.
destruct (ln_beta beta x) as (ex, He).
assert (Hx: (0 < x)%R).
apply Rlt_le_trans with (1 := Hd).
apply Hxd.
specialize (He (Rgt_not_eq _ _ Hx)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
apply Rle_trans with (bpow (ex - 1)).
apply -> bpow_le.
cut (e < ex)%Z. omega.
apply <- bpow_lt.
now apply Rle_lt_trans with (2 := proj2 He).
apply Hxd with (2 := proj1 He).
apply generic_format_bpow.
destruct (Zle_or_lt ex (fexp ex)).
elim Rgt_not_eq with (1 := Hd).
apply Rnd_DN_pt_unicity with (1 := Hxd).
now apply generic_DN_pt_small_pos with (1 := He).
ring_simplify (ex - 1 + 1)%Z.
omega.
Qed.

697
End RND_generic.