Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Flocq_rnd_generic.v 17 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
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
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
simpl.
apply f_equal.
apply sym_eq.
apply ln_beta_unique.
86
rewrite Rabs_pos_eq.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
87 88
split.
exact Hbl.
89
now apply Rle_lt_trans with (2 := Hx2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90 91 92
apply Rle_trans with (2 := Hbl).
apply epow_ge_0.
split.
93
exact Hrx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
94 95 96 97 98 99 100 101
(* - . 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
102
assert (bpow (ex - 1) <= g < bpow ex)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
103 104 105 106
split.
apply Rle_trans with (1 := Hbl).
now apply Rlt_le.
now apply Rle_lt_trans with (1 := Hgx).
107
rewrite <- (Rabs_pos_eq g (Rlt_le _ _ Hg3)) in H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
108 109 110 111 112 113 114 115
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.
116
apply Zfloor_lub.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
117 118 119 120 121 122 123 124
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.
125
rewrite <- Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126 127
now rewrite <- Hg1.
(* - positive too small *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
128
replace (Zfloor (x * bpow (- fexp ex))) with Z0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
129 130 131 132
(* - . rounded *)
unfold F2R. simpl.
rewrite Rmult_0_l.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
133
exists (Float beta Z0 _) ; repeat split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
134 135 136
unfold F2R. simpl.
now rewrite Rmult_0_l.
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
137 138
apply Rle_trans with (2 := Hx1).
apply epow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
139 140 141 142
(* - . biggest *)
intros g ((gm, ge), (Hg1, Hg2)) Hgx.
apply Rnot_lt_le.
intros Hg3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
143
destruct (ln_beta beta g) as (ge', Hg4).
144 145 146
simpl in Hg2.
specialize (Hg4 (Rgt_not_eq _ _ Hg3)).
rewrite Rabs_pos_eq in Hg4.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
147 148 149
apply (Rlt_not_le _ _ (Rle_lt_trans _ _ _ Hgx Hx2)).
apply Rle_trans with (bpow ge).
apply -> epow_le.
150
simpl in Hg2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151
rewrite Hg2.
152
rewrite (proj2 (proj2 (prop_exp ex) He1) ge').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
153 154
exact He1.
apply Zle_trans with (2 := He1).
155
cut (ge' - 1 < ex)%Z. omega.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
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.
173
now apply Rlt_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
174 175
(* - . . *)
apply sym_eq.
176 177 178 179 180 181 182 183
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
184
apply epow_gt_0.
185 186 187 188
rewrite Rmult_assoc.
rewrite <- epow_add.
rewrite Zplus_opp_l.
rewrite Rmult_1_r, Rmult_1_l.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
189 190
apply Rlt_le_trans with (1 := Hx2).
now apply -> epow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
191 192 193 194
Qed.

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

436 437 438 439 440 441 442 443
Theorem generic_format_0 :
  generic_format 0.
Proof.
exists (Float beta 0 _) ; repeat split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
Qed.

444 445 446 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.
apply epow_gt_0.
Qed.

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

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

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

Theorem generic_DN_pt_small_pos :
529
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
530
  (bpow (ex - 1) <= x < bpow ex)%R ->
531 532 533 534 535
  (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
536
exists (Float beta 0 _) ; repeat split.
537 538 539 540 541 542 543 544 545
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.
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 556 557 558 559 560 561 562 563 564 565 566 567 568
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
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 579 580 581
rewrite Z2R_Zpower.
rewrite <- epow_add.
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 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612
apply -> epow_lt.
apply Zle_lt_succ.
apply Zle_refl.
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.
613
destruct (ln_beta beta g) as (eg, Hg3).
614
simpl in Hg2.
615
specialize (Hg3 H0).
616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637
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
638
Theorem generic_UP_pt_large_pos_le_pow :
639
  forall x xu ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
640
  (bpow (ex - 1) <= x < bpow ex)%R ->
641 642 643 644 645 646 647
  (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))).
648
unfold canonic, F2R. simpl.
649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669
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
670 671
Theorem generic_UP_pt_pos :
  forall x ex,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
672
  (bpow (ex - 1) <= x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
673 674 675 676 677 678 679 680 681 682 683 684 685 686 687
  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
688
  (bpow (ex - 1) <= - x < bpow ex)%R ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
689 690 691 692 693 694 695 696 697 698 699 700
  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.

701
End RND_generic.
702

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

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