Flocq_rnd_generic.v 15.1 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 195 196 197 198 199 200
Proof.
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.
201
assert (Hbr : (F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex)) <= x)%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
202 203 204 205 206 207 208 209 210
(* - 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.
apply Rmult_le_compat_r.
apply epow_ge_0.
211
apply Zfloor_lb.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
212 213
destruct (Z_lt_le_dec (fexp ex) ex) as [He1|He1].
(* - negative big enough *)
214
assert (Hbl : (- bpow ex <= F2R (Float beta (Zfloor (x * bpow (- fexp ex)%Z)) (fexp ex)))%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
215 216 217 218 219 220 221
(* - . 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.
222 223 224
assert (Hp : (- bpow (ex - fexp ex)%Z = Z2R (- Zpower (radix_val beta) (ex - fexp ex)))%R).
rewrite <- Z2R_Zpower.
now rewrite opp_Z2R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
225
omega.
226 227 228
rewrite Hp.
apply Z2R_le.
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
229
rewrite <- Hp.
230 231 232 233 234
unfold Zminus.
rewrite epow_add.
rewrite <- Ropp_mult_distr_l_reverse.
apply Rmult_le_compat_r.
apply epow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
235 236
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
237 238 239 240 241
now apply Rlt_le.
split.
(* - . rounded *)
destruct (Rle_lt_or_eq_dec _ _ Hbl) as [Hbl2|Hbl2].
(* - . . not a radix power *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
242
eexists ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
243 244 245 246
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
247
rewrite Rabs_left.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
248
split.
249 250
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
251
apply Rle_trans with (1 := Hbr).
252 253 254 255
apply Ropp_le_cancel.
now rewrite Ropp_involutive.
apply Ropp_lt_cancel.
now rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
256 257 258 259
apply Rle_lt_trans with (1 := Hbr).
exact Hx.
(* - . . a radix power *)
rewrite <- Hbl2.
260
generalize (proj1 (prop_exp _) He1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
261 262 263 264 265 266 267 268 269 270 271
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)).
272 273 274
apply sym_eq.
apply Z2R_Zpower.
omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
275 276 277
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
278 279
rewrite Rabs_Ropp.
rewrite Rabs_right.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
280 281 282 283 284 285 286 287 288 289 290 291 292 293 294
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
295
destruct (ln_beta beta (Rabs g)) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
296
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
297
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
298 299 300 301 302 303 304 305
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).
306
rewrite Rabs_left with (1 := Hg4).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
307 308
now apply Ropp_le_contravar.
apply Ropp_lt_cancel.
309 310 311
rewrite Rabs_left with (1 := Hg4).
rewrite Ropp_involutive.
now apply Rle_lt_trans with (1 := Hbl).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
312 313 314 315
rewrite Hge'.
apply Rmult_le_compat_r.
apply epow_ge_0.
apply Z2R_le.
316
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
317 318 319 320 321 322 323 324 325 326 327
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 *)
328
replace (Zfloor (x * bpow (- fexp ex)%Z)) with (-1)%Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
329 330 331 332 333
unfold F2R. simpl.
rewrite Ropp_mult_distr_l_reverse.
rewrite Rmult_1_l.
(* - . rounded *)
split.
334
destruct (proj2 (prop_exp _) He1) as (He2, _).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
335 336 337 338 339 340 341 342
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)).
343 344 345
apply sym_eq.
apply Z2R_Zpower.
omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
346 347 348
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
349 350
rewrite Rabs_Ropp.
rewrite Rabs_pos_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
351 352 353 354 355
split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply Rle_refl.
apply -> epow_lt.
apply Zlt_succ.
356
apply epow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
357 358
split.
(* - . smaller *)
359 360
apply Ropp_le_cancel.
rewrite Ropp_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
361 362 363 364 365 366 367 368 369
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
370
destruct (ln_beta beta (Rabs g)) as (ge', Hge).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
371
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
372
specialize (Hge (Rabs_pos_lt g (Rlt_not_eq g 0 Hg4))).
373
rewrite (Rabs_left _ Hg4) in Hge.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
374 375 376 377 378 379
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.
380
rewrite (proj2 (proj2 (prop_exp _) He1) _ Hge') in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
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
399 400
change (0 < F2R (Float beta (-gm) ge))%R.
rewrite <- opp_F2R.
401 402 403
rewrite <- Hg1.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
404 405
apply Rle_trans with (1 * bpow (ge - ge')%Z)%R.
rewrite Rmult_1_l.
406 407
apply -> (epow_le beta 0).
omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
408 409 410 411 412
apply Rmult_le_compat_r.
apply epow_ge_0.
now apply (Z2R_le 1).
(* - . . *)
apply sym_eq.
413
apply Zfloor_imp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
414
simpl.
415 416 417 418 419 420 421
split.
apply Rle_trans with (- bpow ex * bpow (- fexp ex)%Z)%R.
rewrite Ropp_mult_distr_l_reverse.
rewrite <- epow_add.
apply Ropp_le_contravar.
apply (proj1 (epow_le beta _ 0)).
omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
422 423
apply Rmult_le_compat_r.
apply epow_ge_0.
424 425 426
apply Ropp_le_cancel.
rewrite Ropp_involutive.
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
427 428 429 430 431 432
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
433 434 435 436 437
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
438
exists (Float beta 0 _) ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
439 440 441
unfold F2R. simpl.
now rewrite Rmult_0_l.
intros x ((m,e),(H1,H2)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
442 443 444 445 446 447
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
448 449 450 451
(* rounding down *)
exists (fun x =>
  match total_order_T 0 x with
  | inleft (left Hx) =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
452
    let e := fexp (projT1 (ln_beta beta x)) in
453
    F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
454 455
  | inleft (right _) => R0
  | inright Hx =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
456
    let e := fexp (projT1 (ln_beta beta (-x))) in
457
    F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
458 459 460 461
  end).
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* positive *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
462
destruct (ln_beta beta x) as (ex, Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
463
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
464 465
apply generic_DN_pt_pos.
now apply Hx'.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
466 467
(* zero *)
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
468 469
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
470 471 472 473 474 475 476
now rewrite Rmult_0_l.
rewrite <- Hx.
split.
apply Rle_refl.
intros g _ H.
exact H.
(* negative *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
477
destruct (ln_beta beta (- x)) as (ex, Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
479 480 481 482
apply generic_DN_pt_neg.
apply Hx'.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
483 484 485
Qed.

Theorem generic_DN_pt_small_pos :
486 487 488 489 490 491 492
  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
493
exists (Float beta 0 _) ; repeat split.
494 495 496 497 498 499 500 501 502
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
503
destruct (ln_beta beta (Rabs g)) as (eg, Hg4).
504
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
505
specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))).
506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525
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
526
Theorem generic_UP_pt_small_pos :
527 528 529 530 531 532
  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
533
assert (bpow (fexp ex) = F2R (Float beta (Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1)))).
534
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
535 536 537 538
rewrite Z2R_Zpower.
rewrite <- epow_add.
apply f_equal.
ring.
539 540 541 542 543
generalize (proj1 (proj2 (prop_exp ex) He)).
omega.
split.
(* . *)
rewrite H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
544
eexists ; repeat split.
545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570
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
571
destruct (ln_beta beta (Rabs g)) as (eg, Hg3).
572
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
573
specialize (Hg3 (Rabs_pos_lt g H0)).
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
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
596
Theorem generic_UP_pt_large_pos_le_pow :
597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627
  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.

628
End RND_generic.