Fcore_generic_fmt.v 19.1 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
Definition canonic x (f : float beta) :=
24
  x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta x)).
25

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

Guillaume Melquiond's avatar
Guillaume Melquiond committed
30 31 32 33 34 35 36
Theorem generic_format_0 :
  generic_format 0.
Proof.
exists (Float beta 0 _) ; repeat split.
now rewrite F2R_0.
Qed.

37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53
Theorem generic_format_bpow :
  forall e, (fexp (e + 1) <= e)%Z ->
  generic_format (bpow e).
Proof.
intros e H.
exists (Float beta (1 * Zpower (radix_val beta) (e - fexp (e + 1))) (fexp (e + 1))).
split.
rewrite <- F2R_change_exp.
apply sym_eq.
apply F2R_bpow.
exact H.
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_bpow.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
54
Theorem generic_DN_pt_large_pos_ge_pow_aux :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
55 56
  forall x ex,
  (fexp ex < ex)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
57 58
  (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
59
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
60
intros x ex He1 Hx1.
61
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
62
replace (ex - 1)%Z with ((ex - 1 - fexp ex) + fexp ex)%Z by ring.
63
rewrite bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
64
apply Rmult_le_compat_r.
65
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
66
assert (Hx2 : bpow (ex - 1 - fexp ex) = Z2R (Zpower (radix_val beta) (ex - 1 - fexp ex))).
67 68 69 70 71 72 73 74
apply sym_eq.
apply Z2R_Zpower.
omega.
rewrite Hx2.
apply Z2R_le.
apply Zfloor_lub.
rewrite <- Hx2.
unfold Zminus at 1.
75
rewrite bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
76
apply Rmult_le_compat_r.
77
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
78
exact Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
79 80 81 82
Qed.

Theorem generic_DN_pt_pos :
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
83 84
  (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
85 86 87 88
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
89
assert (Hbl : (bpow (ex - 1) <= F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)))%R).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90
now apply generic_DN_pt_large_pos_ge_pow_aux.
91
(* - . smaller *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
92
assert (Hrx : (F2R (Float beta (Zfloor (x * bpow (- fexp ex))) (fexp ex)) <= x)%R).
93
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
94
pattern x at 2 ; replace x with ((x * bpow (- fexp ex)) * bpow (fexp ex))%R.
95
apply Rmult_le_compat_r.
96
apply bpow_ge_0.
97 98
apply Zfloor_lb.
rewrite Rmult_assoc.
99
rewrite <- bpow_add.
100 101
rewrite Zplus_opp_l.
apply Rmult_1_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
102 103
split.
(* - . rounded *)
104
eexists ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
105 106 107 108
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
109
rewrite Rabs_pos_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
110 111
split.
exact Hbl.
112
now apply Rle_lt_trans with (2 := Hx2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
113
apply Rle_trans with (2 := Hbl).
114
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
115
split.
116
exact Hrx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
117 118 119 120 121
(* - . 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).
122
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
123 124
apply Rnot_lt_le.
intros Hrg.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
125
assert (bpow (ex - 1) <= g < bpow ex)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126 127 128 129
split.
apply Rle_trans with (1 := Hbl).
now apply Rlt_le.
now apply Rle_lt_trans with (1 := Hgx).
130
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
131 132 133 134
rewrite ln_beta_unique with (1 := H) in Hg2.
simpl in Hg2.
apply Rlt_not_le with (1 := Hrg).
rewrite Hg1, Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
135
apply F2R_le_compat.
136
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
137
apply Rmult_le_reg_r with (bpow (fexp ex)).
138
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139
rewrite Rmult_assoc.
140
rewrite <- bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
141 142 143 144
rewrite Zplus_opp_l.
rewrite Rmult_1_r.
unfold F2R in Hg1.
simpl in Hg1.
145
rewrite <- Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
146 147
now rewrite <- Hg1.
(* - positive too small *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
148
replace (Zfloor (x * bpow (- fexp ex))) with Z0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
149
(* - . rounded *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
150
rewrite F2R_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
152
exact generic_format_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
153
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
154
apply Rle_trans with (2 := Hx1).
155
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
156 157 158 159
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
160
destruct (ln_beta beta g) as (ge', Hg4).
161 162 163
simpl in Hg2.
specialize (Hg4 (Rgt_not_eq _ _ Hg3)).
rewrite Rabs_pos_eq in Hg4.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
164 165
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)).
apply Rle_trans with (bpow ge).
166
apply -> bpow_le.
167
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
168
rewrite Hg2.
169
rewrite (proj2 (proj2 (prop_exp ex) He1) ge').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
170 171
exact He1.
apply Zle_trans with (2 := He1).
172
cut (ge' - 1 < ex)%Z. omega.
173
apply <- bpow_lt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
174 175 176 177
apply Rle_lt_trans with (2 := Hx2).
apply Rle_trans with (2 := Hgx).
exact (proj1 Hg4).
rewrite Hg1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
178 179
rewrite <- F2R_bpow.
apply F2R_le_compat.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
180
apply (Zlt_le_succ 0).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
181 182
apply F2R_lt_reg with beta ge.
now rewrite F2R_0, <- Hg1.
183
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
184 185
(* - . . *)
apply sym_eq.
186 187 188 189 190
apply Zfloor_imp.
simpl.
split.
apply Rmult_le_pos.
apply Rle_trans with (2 := Hx1).
191 192
apply bpow_ge_0.
apply bpow_ge_0.
193
apply Rmult_lt_reg_r with (bpow (fexp ex)).
194
apply bpow_gt_0.
195
rewrite Rmult_assoc.
196
rewrite <- bpow_add.
197 198
rewrite Zplus_opp_l.
rewrite Rmult_1_r, Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
199
apply Rlt_le_trans with (1 := Hx2).
200
now apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
201 202 203 204
Qed.

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

446 447 448 449 450 451 452 453 454 455 456 457 458 459 460
Theorem canonic_unicity :
  forall x f1 f2,
  canonic x f1 ->
  canonic x f2 ->
  f1 = f2.
Proof.
intros x (m1,e1) (m2,e2) (H1a,H1b) (H2a,H2b).
simpl in H1b, H2b.
rewrite H1b, <- H2b.
apply (f_equal (fun m => Float beta m e2)).
apply eq_Z2R.
apply Rmult_eq_reg_r with (bpow e1).
change (F2R (Float beta m1 e1) = F2R (Float beta m2 e1)).
now rewrite <- H1a, H1b, <- H2b.
apply Rgt_not_eq.
461
apply bpow_gt_0.
462 463
Qed.

464 465 466 467 468
Theorem canonic_sym :
  forall x m e,
  canonic x (Float beta m e) ->
  canonic (-x) (Float beta (-m) e).
Proof.
469 470 471 472 473 474 475 476 477 478
intros x m e.
destruct (Req_dec x 0) as [Hx|Hx].
(* . *)
rewrite Hx, Ropp_0.
intros (H1,H2).
split.
now rewrite <- opp_F2R, <- H1, Ropp_0.
exact H2.
(* . *)
intros (H1,H2).
479 480 481
split.
rewrite H1.
apply opp_F2R.
482
now rewrite ln_beta_opp.
483 484
Qed.

485 486
Theorem generic_format_sym :
  forall x, generic_format x -> generic_format (-x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
487
Proof.
488 489 490
intros x ((m,e),H).
exists (Float beta (-m) e).
now apply canonic_sym.
491 492 493 494 495
Qed.

Theorem generic_format_satisfies_any :
  satisfies_any generic_format.
Proof.
496
split.
497
(* symmetric set *)
498
exact generic_format_0.
499
exact generic_format_sym.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
500
(* rounding down *)
501 502
intros x.
exists (match Req_EM_T x 0 with
503 504
  | left Hx => R0
  | right Hx =>
Guillaume Melquiond's avatar
Guillaume Melquiond committed
505
    let e := fexp (projT1 (ln_beta beta x)) in
506
    F2R (Float beta (Zfloor (x * bpow (Zopp e))) e)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
507
  end).
508 509
destruct (Req_EM_T x 0) as [Hx|Hx].
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
510
split.
511 512
apply generic_format_0.
rewrite Hx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
513 514
split.
apply Rle_refl.
515 516 517
now intros g _ H.
(* . *)
destruct (ln_beta beta x) as (ex, H1).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
518
simpl.
519 520
specialize (H1 Hx).
destruct (Rdichotomy _ _ Hx) as [H2|H2].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
521
apply generic_DN_pt_neg.
522 523 524 525 526
now rewrite <- Rabs_left.
apply generic_DN_pt_pos.
rewrite Rabs_right in H1.
exact H1.
now apply Rgt_ge.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
527 528 529
Qed.

Theorem generic_DN_pt_small_pos :
530
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
531
  (bpow (ex - 1) <= x < bpow ex)%R ->
532 533 534 535 536
  (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
537
exact generic_format_0.
538 539
split.
apply Rle_trans with (2 := proj1 Hx).
540
apply bpow_ge_0.
541 542 543 544
(* . *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
545
destruct (ln_beta beta g) as (eg, Hg4).
546
simpl in Hg2.
547
specialize (Hg4 (Rgt_not_eq g 0 Hg3)).
548 549 550 551 552 553 554
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)).
555
now apply -> bpow_le.
556 557
rewrite <- Hg2.
rewrite Hg1 in Hg3.
558
apply bpow_le_F2R.
559
apply F2R_gt_0_reg with (1 := Hg3).
560
apply bpow_lt_bpow with beta.
561 562 563
apply Rlt_le_trans with (bpow ex).
apply Rle_lt_trans with (2 := proj2 Hx).
now apply Rle_trans with g.
564
now apply -> bpow_le.
565 566 567 568
apply Rle_ge.
now apply Rlt_le.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
569
Theorem generic_UP_pt_small_pos :
570
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
571
  (bpow (ex - 1) <= x < bpow ex)%R ->
572 573 574 575
  (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
576
assert (bpow (fexp ex) = F2R (Float beta (Zpower (radix_val beta) (fexp ex - fexp (fexp ex + 1))) (fexp (fexp ex + 1)))).
577
unfold F2R. simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
578
rewrite Z2R_Zpower.
579
rewrite <- bpow_add.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
580 581
apply f_equal.
ring.
582 583 584 585 586
generalize (proj1 (proj2 (prop_exp ex) He)).
omega.
split.
(* . *)
rewrite H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
587
eexists ; repeat split.
588 589 590 591
simpl.
apply f_equal.
apply sym_eq.
rewrite <- H.
592
apply ln_beta_unique.
593 594 595
split.
replace (fexp ex + 1 - 1)%Z with (fexp ex) by ring.
apply RRle_abs.
596
rewrite Rabs_pos_eq.
597
apply -> bpow_lt.
598 599
apply Zle_lt_succ.
apply Zle_refl.
600
apply bpow_ge_0.
601 602 603 604
split.
(* . *)
apply Rlt_le.
apply Rlt_le_trans with (1 := proj2 Hx).
605
now apply -> bpow_le.
606 607 608 609 610 611
(* . *)
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).
612
apply bpow_gt_0.
613
destruct (ln_beta beta g) as (eg, Hg3).
614
simpl in Hg2.
615
specialize (Hg3 H0).
616 617 618 619 620 621
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.
622
apply bpow_le_F2R.
623
apply F2R_gt_0_reg with beta ge.
624 625 626
rewrite <- Hg1.
apply Rlt_le_trans with (2 := Hgx).
apply Rlt_le_trans with (2 := proj1 Hx).
627 628
apply bpow_gt_0.
apply bpow_lt_bpow with beta.
629 630 631 632 633 634
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).
635
apply bpow_ge_0.
636 637 638
exact Hgp.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
639
Theorem generic_UP_pt_large_pos_le_pow :
640
  forall x xu ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
641
  (bpow (ex - 1) <= x < bpow ex)%R ->
642 643 644 645 646 647 648
  (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))).
649
unfold canonic, F2R. simpl.
650 651 652
split.
(* . *)
rewrite Z2R_Zpower.
653
rewrite <- bpow_add.
654 655 656 657 658 659 660 661 662 663 664 665
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.
666
apply -> bpow_lt.
667
apply Zlt_succ.
668
apply bpow_ge_0.
669 670
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
671 672
Theorem generic_UP_pt_pos :
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
673
  (bpow (ex - 1) <= x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
  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
689
  (bpow (ex - 1) <= - x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
690 691 692 693 694 695 696 697 698 699 700 701
  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.

702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764
Theorem generic_DN_pt :
  forall x,
  Rnd_DN_pt generic_format x (F2R (Float beta (Zfloor (x * bpow (Zopp (fexp (projT1 (ln_beta beta x)))))) (fexp (projT1 (ln_beta beta x))))).
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
(* x = 0 *)
rewrite Hx, Rmult_0_l.
fold (Z2R 0).
rewrite Zfloor_Z, F2R_0.
apply Rnd_DN_pt_refl.
apply generic_format_0.
(* x <> 0 *)
destruct (ln_beta beta x) as (ex, Hex).
simpl.
specialize (Hex Hx).
unfold Rabs in Hex.
destruct (Rcase_abs x) as [Hx'|Hx'].
now apply generic_DN_pt_neg.
now apply generic_DN_pt_pos.
Qed.

Theorem generic_UP_pt :
  forall x,
  Rnd_UP_pt generic_format x (F2R (Float beta (Zceil (x * bpow (Zopp (fexp (projT1 (ln_beta beta x)))))) (fexp (projT1 (ln_beta beta x))))).
Proof.
intros x.
destruct (Req_dec x 0) as [Hx|Hx].
(* x = 0 *)
rewrite Hx, Rmult_0_l.
fold (Z2R 0).
rewrite Zceil_Z, F2R_0.
apply Rnd_UP_pt_refl.
apply generic_format_0.
(* x <> 0 *)
destruct (ln_beta beta x) as (ex, Hex).
simpl.
specialize (Hex Hx).
unfold Rabs in Hex.
destruct (Rcase_abs x) as [Hx'|Hx'].
now apply generic_UP_pt_neg.
now apply generic_UP_pt_pos.
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
765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793
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.

794
End RND_generic.
795

796 797
Theorem canonic_fun_eq :
  forall beta : radix, forall f1 f2 : Z -> Z, forall x f,
798
  f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) ->
799 800 801 802 803 804 805 806
  canonic beta f1 x f -> canonic beta f2 x f.
Proof.
intros beta f1 f2 x f Hf (Hx1,Hx2).
split.
exact Hx1.
now rewrite <- Hf.
Qed.

807 808
Theorem generic_format_fun_eq :
  forall beta : radix, forall f1 f2 : Z -> Z, forall x,
809
  f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) ->
810 811
  generic_format beta f1 x -> generic_format beta f2 x.
Proof.
812
intros beta f1 f2 x Hf (f,Hx).
813
exists f.
814
now apply canonic_fun_eq with (1 := Hf).
815
Qed.