Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Flocq_rnd_generic.v 16.9 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.

11
Notation bpow e := (bpow 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
Definition canonic x (f : float beta) :=
25
  x = F2R f /\ Fexp f = fexp (projT1 (ln_beta beta x)).
26

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 34 35 36 37
Theorem generic_format_0 :
  generic_format 0.
Proof.
exists (Float beta 0 _) ; repeat split.
now rewrite F2R_0.
Qed.

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

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

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

447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
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.
462
apply bpow_gt_0.
463 464
Qed.

465 466 467 468 469
Theorem canonic_sym :
  forall x m e,
  canonic x (Float beta m e) ->
  canonic (-x) (Float beta (-m) e).
Proof.
470 471 472 473 474 475 476 477 478 479
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).
480 481 482
split.
rewrite H1.
apply opp_F2R.
483
now rewrite ln_beta_opp.
484 485
Qed.

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

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

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

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

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

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

703
End RND_generic.
704

705 706
Theorem canonic_fun_eq :
  forall beta : radix, forall f1 f2 : Z -> Z, forall x f,
707
  f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) ->
708 709 710 711 712 713 714 715
  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.

716 717
Theorem generic_format_fun_eq :
  forall beta : radix, forall f1 f2 : Z -> Z, forall x,
718
  f1 (projT1 (ln_beta beta x)) = f2 (projT1 (ln_beta beta x)) ->
719 720
  generic_format beta f1 x -> generic_format beta f2 x.
Proof.
721
intros beta f1 f2 x Hf (f,Hx).
722
exists f.
723
now apply canonic_fun_eq with (1 := Hf).
724
Qed.