Flocq_rnd_generic.v 16.2 KB
Newer Older
Guillaume Melquiond's avatar
Guillaume Melquiond committed
1 2 3
Require Import Flocq_Raux.
Require Import Flocq_defs.
Require Import Flocq_rnd_ex.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
Require Import Flocq_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5 6 7 8 9 10 11 12 13

Section RND_generic.

Variable beta : radix.

Notation bpow := (epow beta).

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

Definition generic_format (x : R) :=
  exists f : float beta,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
25
  x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
26

Guillaume Melquiond's avatar
Guillaume Melquiond committed
27 28 29 30
Theorem generic_DN_pt_large_pos_ge_pow :
  forall x ex,
  (fexp ex < ex)%Z ->
  (bpow (ex - 1)%Z <= x)%R ->
31
  (bpow (ex - 1)%Z <= F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex)))%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
32
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
33
intros x ex He1 Hx1.
34
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
35 36 37 38
replace (ex - 1)%Z with ((ex - 1 - fexp ex) + fexp ex)%Z by ring.
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
39 40 41 42 43 44 45 46 47
assert (Hx2 : bpow (ex - 1 - fexp ex)%Z = Z2R (Zpower (radix_val beta) (ex - 1 - fexp ex))).
apply sym_eq.
apply Z2R_Zpower.
omega.
rewrite Hx2.
apply Z2R_le.
apply Zfloor_lub.
rewrite <- Hx2.
unfold Zminus at 1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
48 49 50 51
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
exact Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
52 53 54 55 56
Qed.

Theorem generic_DN_pt_pos :
  forall x ex,
  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
57
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (Zopp (fexp ex)))) (fexp ex))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
58 59 60 61
Proof.
intros x ex (Hx1, Hx2).
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - positive big enough *)
62
assert (Hbl : (bpow (ex - 1)%Z <= F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex)))%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
63
now apply generic_DN_pt_large_pos_ge_pow.
64 65 66 67 68 69 70 71 72 73 74
(* - . smaller *)
assert (Hrx : (F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex)) <= x)%R).
unfold F2R. simpl.
pattern x at 2 ; replace x with ((x * bpow (- fexp ex)%Z) * bpow (fexp ex))%R.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Zfloor_lb.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
apply Rmult_1_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
75 76
split.
(* - . rounded *)
77
eexists ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
78 79 80 81 82 83 84
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
rewrite Rabs_right.
split.
exact Hbl.
85
now apply Rle_lt_trans with (2 := Hx2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
86 87 88 89
apply Rle_ge.
apply Rle_trans with (2 := Hbl).
apply epow_ge_0.
split.
90
exact Hrx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
91 92 93 94 95 96 97 98 99 100 101 102 103
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
destruct (Rle_or_lt g R0) as [Hg3|Hg3].
apply Rle_trans with (2 := Hbl).
apply Rle_trans with (1 := Hg3).
apply epow_ge_0.
apply Rnot_lt_le.
intros Hrg.
assert (bpow (ex - 1)%Z <= g < bpow ex)%R.
split.
apply Rle_trans with (1 := Hbl).
now apply Rlt_le.
now apply Rle_lt_trans with (1 := Hgx).
104
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
105 106 107 108 109 110 111 112
rewrite ln_beta_unique with (1 := H) in Hg2.
simpl in Hg2.
apply Rlt_not_le with (1 := Hrg).
rewrite Hg1, Hg2.
unfold F2R. simpl.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
113
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
114 115 116 117 118 119 120 121
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
unfold F2R in Hg1.
simpl in Hg1.
122
rewrite <- Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
123 124
now rewrite <- Hg1.
(* - positive too small *)
125
replace (Zfloor (x * bpow (- fexp ex)%Z)) with Z0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126 127 128 129
(* - . rounded *)
unfold F2R. simpl.
rewrite Rmult_0_l.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
130
exists (Float beta Z0 _) ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
131 132 133
unfold F2R. simpl.
now rewrite Rmult_0_l.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
134 135
apply Rle_trans with (2 := Hx1).
apply epow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
136 137 138 139
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
140 141
destruct (ln_beta beta g) as (ge', Hg4).
specialize (Hg4 Hg3).
142 143 144
generalize Hg4. intros Hg5.
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in Hg5.
rewrite ln_beta_unique with (1 := Hg5) in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
145 146 147
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)).
apply Rle_trans with (bpow ge).
apply -> epow_le.
148
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
149
rewrite Hg2.
150
rewrite (proj2 (proj2 (prop_exp ex) He1) ge').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151 152
exact He1.
apply Zle_trans with (2 := He1).
153
cut (ge' - 1 < ex)%Z. omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
apply <- epow_lt.
apply Rle_lt_trans with (2 := Hx2).
apply Rle_trans with (2 := Hgx).
exact (proj1 Hg4).
rewrite Hg1.
unfold F2R. simpl.
pattern (bpow ge) at 1 ; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow ge).
apply epow_gt_0.
rewrite Rmult_0_l.
unfold F2R in Hg1. simpl in Hg1.
now rewrite <- Hg1.
(* - . . *)
apply sym_eq.
173 174 175 176 177 178 179 180
apply Zfloor_imp.
simpl.
split.
apply Rmult_le_pos.
apply Rle_trans with (2 := Hx1).
apply epow_ge_0.
apply epow_ge_0.
apply Rmult_lt_reg_r with (bpow (fexp ex)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
181
apply epow_gt_0.
182 183 184 185
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r, Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
186 187
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
188 189 190 191 192
Qed.

Theorem generic_DN_pt_neg :
  forall x ex,
  (bpow (ex - 1)%Z <= -x < bpow ex)%R ->
193
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (Zopp (fexp ex)))) (fexp ex))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
194
Proof.
195
unfold Zfloor.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
196 197 198 199 200 201
intros x ex (Hx1, Hx2).
assert (Hx : (x < 0)%R).
apply Ropp_lt_cancel.
rewrite Ropp_0.
apply Rlt_le_trans with (2 := Hx1).
apply epow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
202 203 204 205 206 207 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 242 243 244 245 246 247 248 249 250 251 252 253
assert (Hbr : (F2R (Float beta (up (x * bpow (- fexp ex)%Z) - 1) (fexp ex)) <= x)%R).
(* - bounded right *)
unfold F2R. simpl.
pattern x at 2 ; rewrite <- Rmult_1_r.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_l (fexp ex)).
rewrite epow_add.
rewrite <- Rmult_assoc.
generalize (x * bpow (- fexp ex)%Z)%R.
clear.
intros x.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite minus_Z2R.
simpl.
rewrite Z2R_IZR.
apply Rplus_le_reg_l with (-x + 1)%R.
ring_simplify.
rewrite Rplus_comm.
exact (proj2 (archimed x)).
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - negative big enough *)
assert (Hbl : (- bpow ex <= F2R (Float beta (up (x * bpow (- fexp ex)%Z) - 1) (fexp ex)))%R).
(* - . bounded left *)
unfold F2R. simpl.
pattern ex at 1 ; replace ex with (ex - fexp ex + fexp ex)%Z by ring.
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
cut (0 < ex - fexp ex)%Z. 2: omega.
case_eq (ex - fexp ex)%Z ; try (intros ; discriminate H0).
intros ep Hp _.
simpl.
rewrite <- opp_Z2R.
apply Z2R_le.
cut (- Zpower_pos (radix_val beta) ep < up (x * bpow (- fexp ex)%Z))%Z.
omega.
apply lt_Z2R.
apply Rle_lt_trans with (x * bpow (- fexp ex)%Z)%R.
rewrite opp_Z2R.
change (- bpow (Zpos ep) <= x * bpow (- fexp ex)%Z)%R.
rewrite <- Hp.
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- epow_add.
replace (ex - fexp ex + fexp ex)%Z with ex by ring.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
254 255
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
256 257 258 259 260 261 262
now apply Rlt_le.
rewrite Z2R_IZR.
exact (proj1 (archimed _)).
split.
(* - . rounded *)
destruct (Rle_lt_or_eq_dec _ _ Hbl) as [Hbl2|Hbl2].
(* - . . not a radix power *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
263
eexists ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
264 265 266 267
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
268
rewrite Rabs_left.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
269
split.
270 271
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
272
apply Rle_trans with (1 := Hbr).
273 274 275 276
apply Ropp_le_cancel.
now rewrite Ropp_involutive.
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
277 278 279 280
apply Rle_lt_trans with (1 := Hbr).
exact Hx.
(* - . . a radix power *)
rewrite <- Hbl2.
281
generalize (proj1 (prop_exp _) He1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299
clear.
intros He2.
exists (Float beta (- Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
unfold F2R. simpl.
split.
clear -He2.
pattern ex at 1 ; replace ex with (ex - fexp (ex + 1) + fexp (ex + 1))%Z by ring.
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite opp_Z2R.
apply (f_equal (fun x => (- x * _)%R)).
cut (0 <= ex - fexp (ex + 1))%Z. 2: omega.
case (ex - fexp (ex + 1))%Z ; trivial.
intros ep H.
now elim H.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
300 301
rewrite Rabs_Ropp.
rewrite Rabs_right.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316
split.
apply -> epow_le.
omega.
apply -> epow_lt.
apply Zlt_succ.
apply Rle_ge.
apply epow_ge_0.
split.
exact Hbr.
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
317
destruct (ln_beta beta (Rabs g)) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
318
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
319
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
320 321 322 323 324 325 326 327
apply Rlt_not_le with (1 := Hg3).
rewrite Hg1.
unfold F2R. simpl.
rewrite Hg2.
assert (Hge' : ge' = ex).
apply epow_unique with (1 := Hge).
split.
apply Rle_trans with (1 := Hx1).
328
rewrite Rabs_left with (1 := Hg4).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
329 330
now apply Ropp_le_contravar.
apply Ropp_lt_cancel.
331 332 333
rewrite Rabs_left with (1 := Hg4).
rewrite Ropp_involutive.
now apply Rle_lt_trans with (1 := Hbl).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
334 335 336 337
rewrite Hge'.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
338
cut (gm < up (x * bpow (- fexp ex)%Z))%Z. omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358
apply lt_IZR.
apply Rle_lt_trans with (2 := proj1 (archimed _)).
rewrite <- Z2R_IZR.
apply Rmult_le_reg_r with (bpow (fexp ex)).
apply epow_gt_0.
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
rewrite <- Hge'.
rewrite <- Hg2.
unfold F2R in Hg1. simpl in Hg1.
now rewrite <- Hg1.
(* - negative too small *)
cutrewrite (up (x * bpow (- fexp ex)%Z) = 0%Z).
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
rewrite Rmult_1_l.
(* - . rounded *)
split.
359
destruct (proj2 (prop_exp _) He1) as (He2, _).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
exists (Float beta (- Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1))).
unfold F2R. simpl.
split.
rewrite opp_Z2R.
pattern (fexp ex) at 1 ; replace (fexp ex) with (fexp ex - fexp (fexp ex + 1) + fexp (fexp ex + 1))%Z by ring.
rewrite epow_add.
rewrite Ropp_mult_distr_l_reverse.
apply (f_equal (fun x => (- (x * _))%R)).
cut (0 <= fexp ex - fexp (fexp ex + 1))%Z. 2: omega.
clear.
case (fexp ex - fexp (fexp ex + 1))%Z ; trivial.
intros ep Hp.
now elim Hp.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
376 377
rewrite Rabs_left.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
378 379 380 381 382
split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply Rle_refl.
apply -> epow_lt.
apply Zlt_succ.
383 384 385
rewrite <- Ropp_0.
apply Ropp_lt_contravar.
apply epow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
386 387
split.
(* - . smaller *)
388 389
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
390 391 392 393 394 395 396 397 398
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
assert (Hg4 : (g < 0)%R).
now apply Rle_lt_trans with (1 := Hgx).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
399
destruct (ln_beta beta (Rabs g)) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
400
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
401
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
402
rewrite (Rabs_left _ Hg4) in Hge.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
403 404 405 406 407 408
assert (Hge' : (ge' <= fexp ex)%Z).
cut (ge' - 1 < fexp ex)%Z. omega.
apply <- epow_lt.
apply Rle_lt_trans with (1 := proj1 Hge).
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
409
rewrite (proj2 (proj2 (prop_exp _) He1) _ Hge') in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
rewrite <- Hg2 in Hge'.
apply Rlt_not_le with (1 := proj2 Hge).
rewrite Hg1.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
replace ge with (ge - ge' + ge')%Z by ring.
rewrite epow_add.
rewrite <- Rmult_assoc.
pattern (bpow ge') at 1 ; rewrite <- Rmult_1_l.
apply Rmult_le_compat_r.
apply epow_ge_0.
rewrite <- opp_Z2R.
assert (1 <= -gm)%Z.
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow ge).
apply epow_gt_0.
rewrite Rmult_0_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
428 429
change (0 < F2R (Float beta (-gm) ge))%R.
rewrite <- opp_F2R.
430 431 432
rewrite <- Hg1.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
433 434 435 436 437 438 439 440 441 442 443
apply Rle_trans with (1 * bpow (ge - ge')%Z)%R.
rewrite Rmult_1_l.
cut (0 <= ge - ge')%Z. 2: omega.
clear.
case (ge - ge')%Z.
intros _.
apply Rle_refl.
intros ep _.
simpl.
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
444
apply Zpower_pos_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471
now apply Zlt_le_trans with (2 := radix_prop beta).
intros ep Hp. now elim Hp.
apply Rmult_le_compat_r.
apply epow_ge_0.
now apply (Z2R_le 1).
(* - . . *)
apply sym_eq.
apply (up_tech _ (-1)).
apply Ropp_le_cancel.
simpl.
rewrite Ropp_involutive.
change R1 with (bpow Z0).
rewrite <- (Zplus_opp_r (fexp ex)).
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Rlt_le.
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
simpl.
rewrite <- (Rmult_0_l (bpow (- fexp ex)%Z)).
apply Rmult_lt_compat_r.
apply epow_gt_0.
exact Hx.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
472 473 474 475 476
Theorem generic_format_satisfies_any :
  satisfies_any generic_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
477
exists (Float beta 0 _) ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478 479 480
unfold F2R. simpl.
now rewrite Rmult_0_l.
intros x ((m,e),(H1,H2)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
481 482 483 484 485 486
exists (Float beta (-m) _) ; repeat split.
rewrite H1 at 1.
rewrite Rabs_Ropp.
rewrite opp_F2R.
apply (f_equal (fun v => F2R (Float beta (- m) v))).
exact H2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
487 488 489 490
(* rounding down *)
exists (fun x =>
  match total_order_T 0 x with
  | inleft (left Hx) =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
491
    let e := fexp (projT1 (ln_beta beta x)) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
492 493 494
    F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
  | inleft (right _) => R0
  | inright Hx =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
495
    let e := fexp (projT1 (ln_beta beta (-x))) in
Guillaume Melquiond's avatar
Guillaume Melquiond committed
496 497 498 499 500
    F2R (Float beta (up (x * bpow (Zopp e)) - 1) e)
  end).
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* positive *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
501
destruct (ln_beta beta x) as (ex, Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
502
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
503 504
apply generic_DN_pt_pos.
now apply Hx'.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
505 506
(* zero *)
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
507 508
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
509 510 511 512 513 514 515
now rewrite Rmult_0_l.
rewrite <- Hx.
split.
apply Rle_refl.
intros g _ H.
exact H.
(* negative *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
516
destruct (ln_beta beta (- x)) as (ex, Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
517
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
518 519 520 521
apply generic_DN_pt_neg.
apply Hx'.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
522 523 524
Qed.

Theorem generic_DN_pt_small_pos :
525 526 527 528 529 530 531
  forall x ex,
  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  Rnd_DN_pt generic_format x R0.
Proof.
intros x ex Hx He.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
532
exists (Float beta 0 _) ; repeat split.
533 534 535 536 537 538 539 540 541
unfold F2R. simpl.
now rewrite Rmult_0_l.
split.
apply Rle_trans with (2 := proj1 Hx).
apply epow_ge_0.
(* . *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
542
destruct (ln_beta beta (Rabs g)) as (eg, Hg4).
543
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
544
specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))).
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564
rewrite Rabs_right in Hg4.
apply Rle_not_lt with (1 := Hgx).
rewrite Hg1.
apply Rlt_le_trans with (1 := proj2 Hx).
rewrite (proj2 (proj2 (prop_exp _) He) eg) in Hg2.
rewrite Hg2.
apply Rle_trans with (bpow (fexp ex)).
now apply -> epow_le.
rewrite <- Hg2.
rewrite Hg1 in Hg3.
apply epow_le_F2R with (1 := Hg3).
apply epow_lt_epow with beta.
apply Rlt_le_trans with (bpow ex).
apply Rle_lt_trans with (2 := proj2 Hx).
now apply Rle_trans with g.
now apply -> epow_le.
apply Rle_ge.
now apply Rlt_le.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
565
Theorem generic_UP_pt_small_pos :
566 567 568 569 570 571
  forall x ex,
  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
  (ex <= fexp ex)%Z ->
  Rnd_UP_pt generic_format x (bpow (fexp ex)).
Proof.
intros x ex Hx He.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
572
assert (bpow (fexp ex) = F2R (Float beta (Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1)))).
573
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
574 575 576 577
rewrite Z2R_Zpower.
rewrite <- epow_add.
apply f_equal.
ring.
578 579 580 581 582
generalize (proj1 (proj2 (prop_exp ex) He)).
omega.
split.
(* . *)
rewrite H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
583
eexists ; repeat split.
584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
rewrite <- H.
split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply RRle_abs.
rewrite Rabs_right.
apply -> epow_lt.
apply Zle_lt_succ.
apply Zle_refl.
apply Rle_ge.
apply epow_ge_0.
split.
(* . *)
apply Rlt_le.
apply Rlt_le_trans with (1 := proj2 Hx).
now apply -> epow_le.
(* . *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
assert (g <> R0).
apply Rgt_not_eq.
apply Rlt_le_trans with (2 := Hgx).
apply Rlt_le_trans with (2 := proj1 Hx).
apply epow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
610
destruct (ln_beta beta (Rabs g)) as (eg, Hg3).
611
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
612
specialize (Hg3 (Rabs_pos_lt g H0)).
613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634
apply Rnot_lt_le.
intros Hgp.
apply Rlt_not_le with (1 := Hgp).
rewrite <- (proj2 (proj2 (prop_exp ex) He) eg).
rewrite <- Hg2.
rewrite Hg1.
apply (epow_le_F2R _ (Float beta gm ge)).
rewrite <- Hg1.
apply Rlt_le_trans with (2 := Hgx).
apply Rlt_le_trans with (2 := proj1 Hx).
apply epow_gt_0.
apply epow_lt_epow with beta.
apply Rle_lt_trans with g.
rewrite <- (Rabs_right g).
apply Hg3.
apply Rle_ge.
apply Rle_trans with (2 := Hgx).
apply Rle_trans with (2 := proj1 Hx).
apply epow_ge_0.
exact Hgp.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
635
Theorem generic_UP_pt_large_pos_le_pow :
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666
  forall x xu ex,
  (bpow (ex - 1)%Z <= x < bpow ex)%R ->
  (fexp ex < ex)%Z ->
  Rnd_UP_pt generic_format x xu ->
  (xu <= bpow ex)%R.
Proof.
intros x xu ex Hx He (((dm, de), (Hu1, Hu2)), (Hu3, Hu4)).
apply Hu4 with (2 := (Rlt_le _ _ (proj2 Hx))).
exists (Float beta (Zpower (radix_val beta) (ex - fexp (ex + 1))) (fexp (ex + 1))).
unfold F2R. simpl.
split.
(* . *)
rewrite Z2R_Zpower.
rewrite <- epow_add.
apply f_equal.
ring.
generalize (proj1 (prop_exp _) He).
omega.
(* . *)
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
rewrite Rabs_pos_eq.
split.
ring_simplify (ex + 1 - 1)%Z.
apply Rle_refl.
apply -> epow_lt.
apply Zlt_succ.
apply epow_ge_0.
Qed.

667
End RND_generic.