Ftranslate_flocq2Pff.v 24.7 KB
Newer Older
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1 2 3 4
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Guillaume Melquiond's avatar
Guillaume Melquiond committed
5
Copyright (C) 2013-2018 Sylvie Boldo
BOLDO Sylvie's avatar
BOLDO Sylvie committed
6
#<br />#
Guillaume Melquiond's avatar
Guillaume Melquiond committed
7
Copyright (C) 2013-2018 Guillaume Melquiond
BOLDO Sylvie's avatar
BOLDO Sylvie committed
8 9 10 11 12 13 14 15 16 17 18 19 20

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** Translation from Flocq to Pff *)
21

BOLDO Sylvie's avatar
BOLDO Sylvie committed
22
From Flocq Require Import Pff Core Binary.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
23 24 25 26 27 28 29

Section RND_Closest_c.
(* extension of pff for rounding function with arbitrary tie *)
Variable b : Fbound.
Variable beta : radix.
Variable p : nat.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
30
Coercion FtoRradix := FtoR beta.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88
Hypothesis pGreaterThanOne : 1 < p.
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta p.

Variable choice: Z -> bool.


Definition RND_Closest (r : R) :=
   let ru := RND_Max b beta p r in
   let rd := RND_Min b beta p r in
  match Rle_dec (Rabs (ru - r)) (Rabs (rd - r)) with
  | left H =>
      match
        Rle_lt_or_eq_dec (Rabs (ru - r)) (Rabs (rd - r)) H
      with
      | left _ => ru
      | right _ =>
          match choice (Zfloor (scaled_mantissa beta (FLT_exp (- dExp b) p) r)) with
          | true => ru
          | false => rd
          end
      end
  | right _ => rd
  end.


Theorem RND_Closest_canonic :
 forall r : R, Fcanonic beta b (RND_Closest r).
intros r; unfold RND_Closest in |- *.
case (Rle_dec _ _ ); intros H1.
case (Rle_lt_or_eq_dec _ _ H1); intros H2.
apply RND_Max_canonic; try easy; apply radix_gt_1.
case (choice _).
now apply RND_Max_canonic; try easy; apply radix_gt_1.
now apply RND_Min_canonic; try easy; apply radix_gt_1.
now apply RND_Min_canonic; try easy; apply radix_gt_1.
Qed.

Theorem RND_Closest_correct :
 forall r : R, Closest b beta r (RND_Closest r).
intros r.
generalize (radix_gt_1 beta); intros M.
split.
apply FcanonicBound with beta; apply RND_Closest_canonic.
intros f H3; fold FtoRradix.
(* *)
cut (RND_Min b beta p r <= r)%R; [ intros V1 | idtac ].
2: apply (RND_Min_correct b beta p) with (r:=r); easy.
cut (r <= RND_Max b beta p r)%R; [ intros V2 | idtac ].
2: apply (RND_Max_correct b beta p) with (r:=r); easy.
cut (forall v w : R, (v <= w)%R -> (0 <= w - v)%R); [ intros V3 | idtac ].
2: intros v w H; apply Rplus_le_reg_l with v; ring_simplify; auto with real.
cut (forall v w : R, (v <= w)%R -> (v - w <= 0)%R); [ intros V4 | idtac ].
2: intros v w H; apply Rplus_le_reg_l with w; ring_simplify; auto with real.
(* *)
unfold RND_Closest; case (Rle_dec _ _); intros H1.
case (Rle_lt_or_eq_dec _ _ H1); intros H2.
(* . *)
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
89
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
90 91
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H4.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
92
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
93 94 95 96 97 98 99 100 101 102
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
 unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Max_correct b beta p) with (r:=r); try easy.
now apply Rlt_le.
(* . *)
case (choice _).
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
103
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
104 105
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H5.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
106
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
107 108 109 110 111 112 113 114 115
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
 unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Max_correct b beta p) with (r:=r); try easy.
now apply Rlt_le.
(* . *)
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
116
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
117 118 119
rewrite <- H2.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
case (Rle_or_lt f r); intros H5.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
120
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
121 122 123 124 125 126 127 128 129
apply Rle_trans with (1 := H1); apply Ropp_le_contravar;
 unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
unfold Rminus in |- *; apply Rplus_le_compat_r.
apply (RND_Max_correct b beta p) with (r:=r); try easy.
now apply Rlt_le.
(* . *)
apply Rnot_le_lt in H1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
130
rewrite Rabs_left1 in H1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
131
rewrite Rabs_right in H1; [ idtac | apply Rle_ge; apply V3; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
132
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133
case (Rle_or_lt f r); intros H4.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
134
rewrite Rabs_left1; [ idtac | apply V4; auto with real ].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
135 136 137 138 139 140 141 142 143 144
apply Ropp_le_contravar, Rplus_le_compat_r.
apply (RND_Min_correct b beta p) with (r:=r); easy.
rewrite Rabs_right; [ idtac | apply Rle_ge; apply V3; auto with real ].
left; apply Rlt_le_trans with (1:=H1).
apply Rplus_le_compat_r.
apply (RND_Max_correct b beta p) with (r:=r); try easy.
now left.
Qed.

End RND_Closest_c.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
145 146


BOLDO Sylvie's avatar
BOLDO Sylvie committed
147 148
Section Bounds.

149
Variable beta : radix.
150 151
Variable p E:Z.
Hypothesis precisionNotZero : (1 < p)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
152

153
Definition make_bound := Bound
154
      (Z.to_pos (Zpower beta p))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
155
      (Z.abs_N E).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
156

157 158 159 160 161 162
Lemma make_bound_Emin: (E <= 0)%Z ->
        ((Z_of_N (dExp (make_bound)))=-E)%Z.
Proof.
simpl.
rewrite Zabs2N.id_abs.
now apply Z.abs_neq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
163 164
Qed.

165
Lemma make_bound_p:
166
        Zpos (vNum (make_bound))=(Zpower_nat beta (Zabs_nat p)).
167 168 169 170 171
Proof.
unfold make_bound, vNum; simpl.
rewrite Z2Pos.id.
apply Zpower_nat_Zpower.
omega.
172
generalize (Zpower_gt_0 beta); simpl.
173 174
intros T; apply T.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
175 176 177
Qed.


178
Lemma FtoR_F2R: forall (f:Pff.float) (g: float beta), Pff.Fnum f = Fnum g -> Pff.Fexp f = Fexp g ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
179 180 181
  FtoR beta f = F2R g.
Proof.
intros f g H1 H2; unfold FtoR, F2R.
182 183
rewrite H1, H2.
now rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
184 185 186
Qed.


187 188 189
End Bounds.
Section b_Bounds.

190
Definition bsingle := make_bound radix2 24 (-149)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
191 192

Lemma psGivesBound: Zpos (vNum bsingle) = Zpower_nat 2 24.
193 194
unfold bsingle; apply make_bound_p.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
195 196
Qed.

197
Definition bdouble := make_bound radix2 53 1074.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
198 199

Lemma pdGivesBound: Zpos (vNum bdouble) = Zpower_nat 2 53.
200 201
unfold bdouble; apply make_bound_p.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
202 203
Qed.

204
End b_Bounds.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
205
Section Equiv.
206

207
Variable beta: radix.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
208
Variable b : Fbound.
209
Variable p : Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
210

211
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta (Zabs_nat p).
212
Hypothesis precisionNotZero : (1 < p)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
213 214


BOLDO Sylvie's avatar
BOLDO Sylvie committed
215
Lemma pff_format_is_format: forall f, Fbounded b f ->
216
  (generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
217 218
intros f Hf.
apply generic_format_FLT; auto with zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
219
exists (Float beta (Pff.Fnum f) (Pff.Fexp f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
220 221 222
unfold F2R, FtoR; simpl.
rewrite bpow_powerRZ.
reflexivity.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
223
destruct Hf.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
224 225 226
apply Zlt_le_trans with (1:=H).
rewrite pGivesBound.
rewrite Zpower_Zpower_nat; auto with zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
227
now destruct Hf.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
228 229 230
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
231 232
Lemma format_is_pff_format': forall r,
   (generic_format beta (FLT_exp (-dExp b) p) r) ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
233
    Fbounded b (Pff.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
234
                            (cexp beta (FLT_exp (-dExp b) p) r)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
235 236
Proof.
intros x; unfold generic_format.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
237
set (ex := cexp beta (FLT_exp (-dExp b) p) x).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
238 239
set (mx := Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) x)).
intros Hx; repeat split ; simpl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
240
apply lt_IZR.
241
rewrite pGivesBound, IZR_Zpower_nat.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
242 243 244 245 246 247 248 249 250 251
apply Rmult_lt_reg_r with (bpow beta ex).
apply bpow_gt_0.
rewrite <- bpow_plus.
rewrite inj_abs; try omega.
change (F2R (Float beta (Zabs mx) ex) < bpow beta (p + ex))%R.
rewrite F2R_Zabs.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
252
unfold cexp in ex.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
253
destruct (mag beta x) as (ex', He).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
254 255 256 257 258 259 260 261 262 263 264
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
apply bpow_le.
cut (ex' - p <= ex)%Z. omega.
unfold ex, FLT_exp.
apply Zle_max_l.
apply Zle_max_r.
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
265
Lemma format_is_pff_format: forall r,
266 267
  (generic_format beta (FLT_exp (-dExp b) p) r)
  -> exists f, FtoR beta f = r /\ Fbounded b f.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
268
intros r Hr.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
269 270 271
eexists; split.
2: apply (format_is_pff_format' _ Hr).
rewrite Hr at 3; unfold FtoR, F2R; simpl.
272
now rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
273 274 275
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
Lemma format_is_pff_format_can: forall r,
  (generic_format beta (FLT_exp (-dExp b) p) r)
  -> exists f, FtoR beta f = r /\ Fcanonic beta b f.
Proof.
intros r Hr.
destruct (format_is_pff_format r Hr) as (f,(Hf1,Hf2)).
exists (Fnormalize beta b (Zabs_nat p) f); split.
rewrite <- Hf1; apply FnormalizeCorrect.
apply radix_gt_1.
apply FnormalizeCanonic; try assumption.
apply radix_gt_1.
assert (0 < Z.abs_nat p); try omega.
apply absolu_lt_nz; omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
291

292 293
Lemma equiv_RNDs_aux: forall z, Z.even z = true -> Even z.
intros z; unfold Z.even, Even.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
294 295 296 297 298 299 300 301 302 303 304 305 306 307
case z.
intros; exists 0%Z; auto with zarith.
intros p0; case p0.
intros p1 H; contradict H; auto.
intros p1 _.
exists (Zpos p1); auto with zarith.
intros H; contradict H; auto.
intros p0; case p0.
intros p1 H; contradict H; auto.
intros p1 _.
exists (Zneg p1); auto with zarith.
intros H; contradict H; auto.
Qed.

308
Lemma pff_canonic_is_canonic: forall f, Fcanonic beta b f -> FtoR beta f <> 0 ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
309
  canonical beta (FLT_exp (- dExp b) p)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
310
    (Float beta (Pff.Fnum f) (Pff.Fexp f)).
311
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
312
intros f Hf1 Hf2; unfold canonical; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
313
assert (K:(F2R (Float beta (Pff.Fnum f) (Pff.Fexp f)) = FtoR beta f)).
314 315
  unfold FtoR, F2R; simpl.
  now rewrite bpow_powerRZ.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
316
unfold cexp, FLT_exp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
317
rewrite K.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
318
destruct (mag beta (FtoR beta f)) as (e, He).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
319 320 321
simpl; destruct Hf1.
(* . *)
destruct H as (H1,H2).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
322
cut (Pff.Fexp f = e-p)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
323 324 325
intros V; rewrite V.
apply sym_eq; apply Zmax_left.
rewrite <- V; destruct H1; auto with zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
326
assert (e = Pff.Fexp f + p)%Z;[idtac|omega].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
327 328
apply trans_eq with (mag beta (FtoR beta f)).
apply sym_eq; apply mag_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
329
apply He; assumption.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
330
apply mag_unique.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
331 332
rewrite <- K; unfold F2R; simpl.
rewrite Rabs_mult.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
333
rewrite (Rabs_right (bpow beta (Pff.Fexp f))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
334 335
2: apply Rle_ge; apply bpow_ge_0.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
336
replace (Pff.Fexp f + p - 1)%Z with ((p-1)+Pff.Fexp f)%Z by ring.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
337 338 339 340
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
(* .. *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
341 342
apply Rmult_le_reg_l with (IZR beta).
apply IZR_lt.
343
apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
344
rewrite <- bpow_plus_1.
345
replace (p-1+1)%Z with (Z_of_nat (Zabs_nat p)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
346
rewrite <- IZR_Zpower_nat.
347
simpl; rewrite <- pGivesBound.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
348 349 350
rewrite Rabs_Zabs.
rewrite <- mult_IZR.
apply IZR_le.
351
rewrite <- (Zabs_eq (beta)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
352 353
rewrite <- Zabs.Zabs_Zmult.
assumption.
354
apply Zlt_le_weak; apply radix_gt_0.
355 356
rewrite inj_abs; try ring.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
357 358 359 360
(* .. *)
rewrite Zplus_comm, bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
361
rewrite <- (inj_abs p);[idtac|omega].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
362
rewrite <- IZR_Zpower_nat.
363
simpl; rewrite <- pGivesBound.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
364 365 366 367 368 369 370 371
rewrite Rabs_Zabs.
apply IZR_lt.
destruct H1; assumption.
(* . *)
destruct H as (H1,(H2,H3)).
rewrite H2.
apply sym_eq; apply Zmax_right.
assert ((e-1) < p-dExp b)%Z;[idtac|omega].
372 373
apply lt_bpow with beta.
apply Rle_lt_trans with (Rabs (FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
374
apply He; auto.
375
apply Rlt_le_trans with (FtoR beta (firstNormalPos beta b (Zabs_nat p))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
376
rewrite <- Fabs_correct.
377
2: apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
378
apply FsubnormalLtFirstNormalPos; auto with zarith.
379
apply radix_gt_1.
380 381
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
382
apply FsubnormFabs; auto with zarith.
383
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
384 385
split; [idtac|split]; assumption.
rewrite Fabs_correct; auto with real zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
386
apply Rabs_pos.
387
apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
388 389
unfold firstNormalPos, FtoR, nNormMin.
simpl.
390 391
replace (IZR (Zpower_nat beta (Peano.pred (Zabs_nat p)))) with (bpow beta (p-1)).
rewrite <- (bpow_powerRZ _).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
392 393
rewrite <- bpow_plus.
apply bpow_le.
394 395
omega.
replace (p-1)%Z with (Z_of_nat (Peano.pred (Zabs_nat p))).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
396
rewrite <- IZR_Zpower_nat.
397
reflexivity.
398 399 400 401
rewrite inj_pred; try omega.
rewrite inj_abs; omega.
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
402 403 404
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
405
Lemma pff_round_NE_is_round: forall (r:R),
406 407 408
   (FtoR beta (RND_EvenClosest b beta (Zabs_nat p) r)
     =  round beta (FLT_exp (-dExp b) p) rndNE r).
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
409
intros.
410 411
assert (Rnd_NE_pt beta (FLT_exp (-dExp b) p) r
         (round beta (FLT_exp (-dExp b) p) rndNE r)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
412 413 414 415
apply round_NE_pt; auto with zarith.
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
apply exists_NE_FLT.
416
now right.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
417 418
unfold Rnd_NE_pt, Rnd_NG_pt, Rnd_N_pt, NE_prop in H.
destruct H as ((H1,H2),H3).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
419
destruct (format_is_pff_format _ H1) as (f,(Hf1,Hf2)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
420
rewrite <- Hf1.
421
generalize (EvenClosestUniqueP b beta (Zabs_nat p)); unfold UniqueP; intros T.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
422
apply sym_eq; apply T with r; auto with zarith; clear T.
423
apply radix_gt_1.
424 425
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
426 427 428 429 430
split.
(* *)
split; auto; intros g Hg.
rewrite Hf1.
apply H2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
431
apply pff_format_is_format; auto.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
432
(* *)
433
case (Req_dec (FtoR beta (Fnormalize beta b (Zabs_nat p) f))  0%R); intros L.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
434 435 436 437 438
left.
unfold FNeven, Feven, Even.
exists 0%Z.
rewrite Zmult_0_r.
apply eq_IZR.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
439
apply Rmult_eq_reg_l with (powerRZ beta (Pff.Fexp (Fnormalize beta b (Zabs_nat p) f)))%R.
440
rewrite Rmult_0_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
441 442
rewrite <- L; unfold FtoR; simpl; ring.
apply powerRZ_NOR; auto with zarith real.
443
apply Rgt_not_eq.
444
apply IZR_lt; apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
445 446 447 448 449
destruct H3.
(* . *)
destruct H as (g,(Hg1,(Hg2,Hg3))).
left.
unfold FNeven, Feven.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
450
apply equiv_RNDs_aux.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
451 452
replace (Pff.Fnum (Fnormalize beta b (Zabs_nat p) f)) with (Fnum g); try assumption.
replace g with (Float beta (Pff.Fnum (Fnormalize beta b (Zabs_nat p) f)) (Pff.Fexp (Fnormalize beta b (Zabs_nat p) f))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
453
easy.
454
apply canonical_unique with (FLT_exp (- dExp b) p).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
455
2: assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
456
apply pff_canonic_is_canonic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
457
apply FnormalizeCanonic; auto with zarith real.
458
apply radix_gt_1.
459 460
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
461 462
exact L.
rewrite <- Hg1, <- Hf1.
463
rewrite <- FnormalizeCorrect with beta b (Zabs_nat p) f; auto with zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
464
unfold F2R, FtoR; simpl.
465 466
rewrite bpow_powerRZ.
reflexivity.
467
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
468 469 470 471 472
(* . *)
right; intros q (Hq1,Hq2).
rewrite Hf1.
apply H.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
473
apply pff_format_is_format; auto.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
474
intros g Hg.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
475
destruct (format_is_pff_format _ Hg) as (v,(Hv1,Hv2)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
476 477 478
rewrite <- Hv1.
apply Hq2; auto.
apply RND_EvenClosest_correct; auto with zarith.
479
apply radix_gt_1.
480 481
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
482 483 484
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
485
Lemma round_NE_is_pff_round: forall (r:R),
BOLDO Sylvie's avatar
BOLDO Sylvie committed
486
   exists f:Pff.float, (Fcanonic beta b f /\ (EvenClosest b beta (Zabs_nat p) r f) /\
487
    FtoR beta f =  round beta (FLT_exp (-dExp b) p) rndNE r).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
488
intros r.
489
exists (RND_EvenClosest b beta (Zabs_nat p) r).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
490 491
split.
apply RND_EvenClosest_canonic; auto with zarith.
492
apply radix_gt_1.
493 494
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
495 496
split.
apply RND_EvenClosest_correct; auto with zarith.
497
apply radix_gt_1.
498 499
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
500
apply pff_round_NE_is_round.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
501 502
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
503
Lemma pff_round_UP_is_round: forall (r:R),
504
  FtoR beta (RND_Max b beta (Z.abs_nat p) r)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532
             = round beta (FLT_exp (- dExp b) p) Zceil r.
Proof with auto with typeclass_instances.
intros r.
generalize (radix_gt_1 beta); intros M.
assert (K:Valid_exp (FLT_exp (- dExp b) p)).
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
destruct (format_is_pff_format_can (round beta (FLT_exp (- dExp b) p) Zceil r)) as (fu,(Hfu1,Hfu2)).
apply generic_format_round...
rewrite <- Hfu1.
apply MaxUniqueP with b r.
apply RND_Max_correct; try assumption.
apply Nat2Z.inj_lt; rewrite inj_abs; simpl; omega.
split.
apply FcanonicBound with (1:=Hfu2).
assert (T:Rnd_UP_pt (generic_format beta (FLT_exp (- dExp b) p)) r
             (round beta (FLT_exp (- dExp b) p) Zceil r)).
apply round_UP_pt...
destruct T as (T1,(T2,T3)).
split.
rewrite Hfu1; apply T2.
intros g Hg1 Hg2.
rewrite Hfu1; apply T3; try assumption.
now apply pff_format_is_format.
Qed.


Lemma pff_round_DN_is_round: forall (r:R),
533
  FtoR beta (RND_Min b beta (Z.abs_nat p) r)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614
             = round beta (FLT_exp (- dExp b) p) Zfloor r.
Proof with auto with typeclass_instances.
intros r.
generalize (radix_gt_1 beta); intros M.
assert (K:Valid_exp (FLT_exp (- dExp b) p)).
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
destruct (format_is_pff_format_can (round beta (FLT_exp (- dExp b) p) Zfloor r)) as (fd,(Hfd1,Hfd2)).
apply generic_format_round...
rewrite <- Hfd1.
apply MinUniqueP with b r.
apply RND_Min_correct; try assumption.
apply Nat2Z.inj_lt; rewrite inj_abs; simpl; omega.
split.
apply FcanonicBound with (1:=Hfd2).
assert (T:Rnd_DN_pt (generic_format beta (FLT_exp (- dExp b) p)) r
             (round beta (FLT_exp (- dExp b) p) Zfloor r)).
apply round_DN_pt...
destruct T as (T1,(T2,T3)).
split.
rewrite Hfd1; apply T2.
intros g Hg1 Hg2.
rewrite Hfd1; apply T3; try assumption.
now apply pff_format_is_format.
Qed.




Lemma pff_round_N_is_round: forall choice, forall (r:R),
   (FtoR beta (RND_Closest b beta (Zabs_nat p) choice r)
     =  round beta (FLT_exp (-dExp b) p) (Znearest choice) r).
Proof with auto with typeclass_instances.
generalize (radix_gt_1 beta); intros M.
intros choice r; apply sym_eq.
assert (K:Valid_exp (FLT_exp (- dExp b) p)).
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
unfold RND_Closest, FtoRradix.
rewrite pff_round_DN_is_round.
rewrite pff_round_UP_is_round.
case (Rle_dec _ _); intros H1.
case (Rle_lt_or_eq_dec _ _ H1); intros H2.
(* *)
rewrite pff_round_UP_is_round.
apply round_N_eq_UP...
rewrite Rabs_right in H2;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy].
rewrite Rabs_left1 in H2;[idtac| apply Rle_minus, round_DN_pt; easy].
apply Rmult_lt_reg_r with 2%R; try apply Rlt_0_2.
unfold Rdiv; rewrite Rmult_assoc, Rinv_l.
2: apply Rgt_not_eq, Rlt_0_2.
apply Rplus_lt_reg_l with (-round beta (FLT_exp (- dExp b) p) Zfloor r - r)%R.
apply Rle_lt_trans with (round beta (FLT_exp (- dExp b) p) Zceil r - r)%R;[right;ring|idtac].
apply Rlt_le_trans with (1:=H2).
right; ring.
(* *)
rewrite round_N_middle.
rewrite inj_abs;[idtac|omega].
case (choice _).
apply sym_eq, pff_round_UP_is_round.
apply sym_eq, pff_round_DN_is_round.
rewrite Rabs_right in H2;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy].
rewrite Rabs_left1 in H2;[idtac| apply Rle_minus, round_DN_pt; easy].
rewrite H2; ring.
(* *)
rewrite pff_round_DN_is_round.
apply round_N_eq_DN...
apply Rnot_le_lt in H1.
rewrite Rabs_left1 in H1;[idtac| apply Rle_minus, round_DN_pt; easy].
rewrite Rabs_right in H1;[idtac| apply Rle_ge, Rle_0_minus, round_UP_pt; easy].
apply Rmult_lt_reg_r with 2%R; try apply Rlt_0_2.
unfold Rdiv; rewrite Rmult_assoc, Rinv_l.
2: apply Rgt_not_eq, Rlt_0_2.
apply Rplus_lt_reg_l with (-round beta (FLT_exp (- dExp b) p) Zfloor r - r)%R.
apply Rle_lt_trans with (-(round beta (FLT_exp (- dExp b) p) Zfloor r - r))%R;[right;ring|idtac].
apply Rlt_le_trans with (1:=H1).
right; ring.
Qed.


Lemma round_N_is_pff_round: forall choice, forall (r:R),
BOLDO Sylvie's avatar
BOLDO Sylvie committed
615
   exists f:Pff.float, (Fcanonic beta b f /\ (Closest b beta r f) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
616 617 618 619 620 621 622 623 624 625 626 627 628 629
    FtoR beta f =  round beta (FLT_exp (-dExp b) p) (Znearest choice) r).
Proof.
intros choice r.
assert (1 < Z.abs_nat p).
apply Nat2Z.inj_lt; simpl.
rewrite inj_abs; omega.
exists (RND_Closest b beta (Zabs_nat p) choice r); split.
apply RND_Closest_canonic; easy.
split.
apply RND_Closest_correct; easy.
apply pff_round_N_is_round.
Qed.

Lemma pff_round_is_round_N: forall r f, Closest b beta r f ->
630
    exists (choice:Z->bool),
BOLDO Sylvie's avatar
BOLDO Sylvie committed
631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
      FtoR beta f = round beta (FLT_exp (-dExp b) p) (Znearest choice) r.
Proof with auto with typeclass_instances.
intros r f Hf.
generalize (radix_gt_1 beta); intros M.
assert (M':1 < Z.abs_nat p).
apply Nat2Z.inj_lt; simpl.
rewrite inj_abs; omega.
pose (d := round beta (FLT_exp (-dExp b) p) Zfloor r).
pose (u := round beta (FLT_exp (-dExp b) p) Zceil r).
case (Rle_or_lt ((d+u)/2) r); intros L.
destruct L as [L|L].
(* rnd up *)
exists (fun _ => true).
rewrite <- pff_round_N_is_round.
apply trans_eq with (FtoR beta (RND_Max b beta (Z.abs_nat p) r)).
apply ClosestMaxEq with b r (RND_Min b beta (Z.abs_nat p) r); try assumption.
apply RND_Min_correct; assumption.
apply RND_Max_correct; assumption.
rewrite pff_round_DN_is_round; fold d.
rewrite pff_round_UP_is_round; fold u.
apply Rmult_lt_reg_r with (/2)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
652
apply pos_half_prf.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
apply Rlt_le_trans with (1:=L).
right; simpl; field.
rewrite pff_round_N_is_round.
rewrite pff_round_UP_is_round; fold u.
apply sym_eq, round_N_eq_UP...
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
(* middle *)
case (ClosestMinOrMax b beta r f); try assumption; intros LL.
exists (fun _ => false).
rewrite round_N_middle.
rewrite <- pff_round_DN_is_round.
apply (MinUniqueP b beta r); try assumption.
apply RND_Min_correct; assumption.
fold d; fold u; rewrite <- L; field.
exists (fun _ => true).
rewrite round_N_middle.
rewrite <- pff_round_UP_is_round.
apply (MaxUniqueP b beta r); try assumption.
apply RND_Max_correct; assumption.
fold d; fold u; rewrite <- L; field.
(* rnd down *)
exists (fun _ => true).
rewrite <- pff_round_N_is_round.
apply trans_eq with (FtoR beta (RND_Min b beta (Z.abs_nat p) r)).
apply ClosestMinEq with b r (RND_Max b beta (Z.abs_nat p) r); try assumption.
apply RND_Min_correct; assumption.
apply RND_Max_correct; assumption.
rewrite pff_round_DN_is_round; fold d.
rewrite pff_round_UP_is_round; fold u.
apply Rmult_lt_reg_r with (/2)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
684
apply pos_half_prf.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
685 686 687 688 689 690 691 692 693 694 695
apply Rle_lt_trans with (2:=L).
right; simpl; field.
rewrite pff_round_N_is_round.
rewrite pff_round_DN_is_round; fold d.
apply sym_eq, round_N_eq_DN...
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
Qed.



696 697
Lemma FloatFexp_gt:  forall e f, Fbounded b f ->
  (bpow beta (e+p) <= Rabs (FtoR beta f))%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
698
       (e < Pff.Fexp f)%Z.
699 700 701 702 703 704 705 706 707 708
Proof.
intros e f Ff H1.
apply lt_bpow with beta.
apply Rmult_lt_reg_r with (bpow beta p).
apply bpow_gt_0.
rewrite <- bpow_plus.
apply Rle_lt_trans with (1:=H1).
rewrite <- Fabs_correct.
2: apply radix_gt_0.
unfold Fabs, FtoR; simpl; rewrite Rmult_comm.
709
rewrite bpow_powerRZ.
710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732
apply Rmult_lt_compat_l.
apply powerRZ_lt.
apply IZR_lt, radix_gt_0.
destruct Ff as (T1,T2).
rewrite bpow_powerRZ.
replace p with (Z.of_nat (Zabs_nat p)).
rewrite <- Zpower_nat_Z_powerRZ.
apply IZR_lt.
now rewrite <- pGivesBound.
rewrite inj_abs; omega.
Qed.

Lemma CanonicGeNormal:  forall f, Fcanonic beta b f ->
  (bpow beta (-dExp b+p-1) <= Rabs (FtoR beta f))%R ->
       (Fnormal beta b f)%Z.
Proof.
intros f Cf H1.
case Cf; trivial.
intros (H2,(H3,H4)).
contradict H1; apply Rlt_not_le.
rewrite <- Fabs_correct.
2: apply radix_gt_0.
unfold FtoR, Fabs; simpl.
733
rewrite H3, <- bpow_powerRZ.
734 735 736 737 738
apply Rlt_le_trans with (bpow beta (p-1)*bpow beta (-dExp b))%R.
2: rewrite <- bpow_plus.
2: right; f_equal; ring.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
739
apply Rmult_lt_reg_l with (IZR beta).
740 741
apply IZR_lt, radix_gt_0.
rewrite <- mult_IZR.
742 743 744 745 746 747
apply Rlt_le_trans with (IZR (Z.pos (vNum b))).
apply IZR_lt.
rewrite <- (Zabs_eq beta).
now rewrite <- Zabs_Zmult.
apply Zlt_le_weak, radix_gt_0.
rewrite pGivesBound.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
748
rewrite IZR_Zpower_nat.
749
rewrite <- bpow_1.
750 751 752 753 754
rewrite <- bpow_plus.
apply bpow_le.
rewrite inj_abs; omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
755

BOLDO Sylvie's avatar
BOLDO Sylvie committed
756
Lemma Fulp_ulp_aux:  forall f, Fcanonic beta b f ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
757 758 759
   Fulp b beta (Z.abs_nat p) f
    = ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
760 761 762 763 764 765 766 767 768 769 770 771
intros f H.
case (Req_dec (FtoR beta f) 0); intros Zf.
(* f = 0 *)
rewrite Zf, ulp_FLT_small.
2: unfold Prec_gt_0; omega.
2: rewrite Rabs_R0; apply bpow_gt_0.
rewrite Fulp_zero.
apply sym_eq, bpow_powerRZ.
apply is_Fzero_rep2 with beta; try assumption.
apply radix_gt_1.
(* f <> 0 *)
rewrite ulp_neq_0; try assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
772
replace (FtoR beta f) with (F2R (Float beta (Pff.Fnum f) (Pff.Fexp f))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
773 774 775 776 777 778 779 780 781
rewrite <- pff_canonic_is_canonic; try assumption.
simpl; rewrite CanonicFulp; try assumption.
unfold FtoR; simpl; rewrite bpow_powerRZ; ring.
apply radix_gt_1.
replace 1 with (Z.abs_nat 1) by easy.
apply Zabs_nat_lt; omega.
unfold F2R, FtoR; simpl.
rewrite bpow_powerRZ; easy.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
782 783


BOLDO Sylvie's avatar
BOLDO Sylvie committed
784 785 786 787 788 789
Lemma Fulp_ulp:  forall f, Fbounded b f ->
   Fulp b beta (Z.abs_nat p) f
    = ulp beta (FLT_exp (-dExp b) p) (FtoR beta f).
intros f H.
assert (Y1: (1 < beta)%Z) by apply radix_gt_1.
assert (Y2:Z.abs_nat p <> 0).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
790
apply sym_not_eq, Nat.lt_neq.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
791 792 793 794 795 796 797 798 799 800 801
replace 0 with (Z.abs_nat 0) by easy.
apply Zabs_nat_lt; omega.
rewrite FulpComp with (q:=Fnormalize beta b (Z.abs_nat p) f); try assumption.
rewrite <- FnormalizeCorrect with beta b (Z.abs_nat p) f; try assumption.
apply Fulp_ulp_aux.
apply FnormalizeCanonic; try assumption.
replace 1 with (Z.abs_nat 1) by easy.
apply Zabs_nat_lt; omega.
apply FnormalizeBounded; try assumption.
apply sym_eq, FnormalizeCorrect; try assumption.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
802 803


BOLDO Sylvie's avatar
BOLDO Sylvie committed
804
End Equiv.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
805 806 807

Section Equiv_instanc.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
808
Lemma round_NE_is_pff_round_b32: forall (r:R),
BOLDO Sylvie's avatar
BOLDO Sylvie committed
809
   exists f:Pff.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
810
    FtoR 2 f =  round radix2 (FLT_exp (-149) 24) rndNE r).
811
Proof.
812
apply (round_NE_is_pff_round radix2 bsingle 24).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
813
apply psGivesBound.
814
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
815 816 817
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
818
Lemma round_NE_is_pff_round_b64: forall (r:R),
BOLDO Sylvie's avatar
BOLDO Sylvie committed
819
   exists f:Pff.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
820
    FtoR 2 f =  round radix2 (FLT_exp (-1074) 53) rndNE r).
821
apply (round_NE_is_pff_round radix2 bdouble 53).
822
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
823
apply pdGivesBound.
824
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
825 826 827 828 829
Qed.



End Equiv_instanc.