Flocq_rnd_generic.v 16.5 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_rnd_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
5
Require Import Flocq_float_prop.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
6 7 8 9 10

Section RND_generic.

Variable beta : radix.

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

Variable fexp : Z -> Z.

15 16 17 18 19 20 21 22
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
23

24 25 26
Definition canonic x (f : float beta) :=
  x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta (Rabs x))).

Guillaume Melquiond's avatar
Guillaume Melquiond committed
27 28
Definition generic_format (x : R) :=
  exists f : float beta,
29
  canonic x f.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
30

Guillaume Melquiond's avatar
Guillaume Melquiond committed
31 32 33
Theorem generic_DN_pt_large_pos_ge_pow :
  forall x ex,
  (fexp ex < ex)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
34 35
  (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
36
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
37
intros x ex He1 Hx1.
38
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
39 40 41 42
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.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
43
assert (Hx2 : bpow (ex - 1 - fexp ex) = Z2R (Zpower (radix_val beta) (ex - 1 - fexp ex))).
44 45 46 47 48 49 50 51
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
52 53 54 55
rewrite epow_add.
apply Rmult_le_compat_r.
apply epow_ge_0.
exact Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
56 57 58 59
Qed.

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

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

437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456
Theorem generic_format_0 :
  generic_format 0.
Proof.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
Qed.

Theorem canonic_sym :
  forall x m e,
  canonic x (Float beta m e) ->
  canonic (-x) (Float beta (-m) e).
Proof.
intros x m e (H1,H2).
split.
rewrite H1.
apply opp_F2R.
now rewrite Rabs_Ropp.
Qed.

457 458
Theorem generic_format_sym :
  forall x, generic_format x -> generic_format (-x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
459
Proof.
460 461 462
intros x ((m,e),H).
exists (Float beta (-m) e).
now apply canonic_sym.
463 464 465 466 467 468 469
Qed.

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.
Proof.
refine ((fun D => Satisfies_any _ _ _ (projT1 D) (projT2 D)) _).
(* symmetric set *)
470
exact generic_format_0.
471
exact generic_format_sym.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
472 473 474 475
(* rounding down *)
exists (fun x =>
  match total_order_T 0 x with
  | inleft (left Hx) =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
476
    let e := fexp (projT1 (ln_beta beta x)) in
477
    F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
478 479
  | inleft (right _) => R0
  | inright Hx =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
480
    let e := fexp (projT1 (ln_beta beta (-x))) in
481
    F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
482 483 484 485
  end).
intros x.
destruct (total_order_T 0 x) as [[Hx|Hx]|Hx].
(* positive *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
486
destruct (ln_beta beta x) as (ex, Hx').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
487
simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
488 489
apply generic_DN_pt_pos.
now apply Hx'.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
490 491
(* zero *)
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
492 493
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
494 495 496 497 498 499 500
now rewrite Rmult_0_l.
rewrite <- Hx.
split.
apply Rle_refl.
intros g _ H.
exact H.
(* negative *)
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 505 506
apply generic_DN_pt_neg.
apply Hx'.
rewrite <- Ropp_0.
now apply Ropp_lt_contravar.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
507 508 509
Qed.

Theorem generic_DN_pt_small_pos :
510
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
511
  (bpow (ex - 1) <= x < bpow ex)%R ->
512 513 514 515 516
  (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
517
exists (Float beta 0 _) ; repeat split.
518 519 520 521 522 523 524 525 526
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
527
destruct (ln_beta beta (Rabs g)) as (eg, Hg4).
528
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
529
specialize (Hg4 (Rabs_pos_lt g (Rgt_not_eq g 0 Hg3))).
530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549
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
550
Theorem generic_UP_pt_small_pos :
551
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
552
  (bpow (ex - 1) <= x < bpow ex)%R ->
553 554 555 556
  (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
557
assert (bpow (fexp ex) = F2R (Float beta (Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1)))).
558
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
559 560 561 562
rewrite Z2R_Zpower.
rewrite <- epow_add.
apply f_equal.
ring.
563 564 565 566 567
generalize (proj1 (proj2 (prop_exp ex) He)).
omega.
split.
(* . *)
rewrite H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
568
eexists ; repeat split.
569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594
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
595
destruct (ln_beta beta (Rabs g)) as (eg, Hg3).
596
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
597
specialize (Hg3 (Rabs_pos_lt g H0)).
598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619
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
620
Theorem generic_UP_pt_large_pos_le_pow :
621
  forall x xu ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
622
  (bpow (ex - 1) <= x < bpow ex)%R ->
623 624 625 626 627 628 629
  (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))).
630
unfold canonic, F2R. simpl.
631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
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.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
652 653
Theorem generic_UP_pt_pos :
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
654
  (bpow (ex - 1) <= x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
655 656 657 658 659 660 661 662 663 664 665 666 667 668 669
  Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (Zopp (fexp ex)))) (fexp ex))).
Proof.
intros x ex Hx1.
apply Rnd_DN_UP_pt_sym.
apply generic_format_satisfies_any.
unfold Zceil.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite opp_F2R.
rewrite Zopp_involutive.
apply generic_DN_pt_neg.
now rewrite Ropp_involutive.
Qed.

Theorem generic_UP_pt_neg :
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
670
  (bpow (ex - 1) <= - x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
671 672 673 674 675 676 677 678 679 680 681 682
  Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (Zopp (fexp ex)))) (fexp ex))).
Proof.
intros x ex Hx1.
apply Rnd_DN_UP_pt_sym.
apply generic_format_satisfies_any.
unfold Zceil.
rewrite <- Ropp_mult_distr_l_reverse.
rewrite opp_F2R.
rewrite Zopp_involutive.
now apply generic_DN_pt_pos.
Qed.

683
End RND_generic.
684 685 686 687 688 689 690 691 692 693 694 695

Theorem generic_format_fun_eq :
  forall beta : radix, forall f1 f2 : Z -> Z, forall x,
  f1 (projT1 (ln_beta beta (Rabs x))) = f2 (projT1 (ln_beta beta (Rabs x))) ->
  generic_format beta f1 x -> generic_format beta f2 x.
Proof.
intros beta f1 f2 x Hf (f,(Hx1,Hx2)).
exists f.
split.
exact Hx1.
now rewrite <- Hf.
Qed.