Ftranslate_flocq2Pff.v 10.6 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/

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

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 *)

Require Import Veltkamp.
Require Import Fcore.
Require Import Fappli_IEEE.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
27 28
Section Bounds.

29
Variable beta : radix.
30 31
Variable p E:Z.
Hypothesis precisionNotZero : (1 < p)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
32

33
Definition make_bound := Bound
34
      (Z.to_pos (Zpower beta p))
BOLDO Sylvie's avatar
BOLDO Sylvie committed
35
      (Z.abs_N E).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
36

37 38 39 40 41 42
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
43 44
Qed.

45
Lemma make_bound_p: 
46
        Zpos (vNum (make_bound))=(Zpower_nat beta (Zabs_nat p)).
47 48 49 50 51
Proof.
unfold make_bound, vNum; simpl.
rewrite Z2Pos.id.
apply Zpower_nat_Zpower.
omega.
52
generalize (Zpower_gt_0 beta); simpl.
53 54
intros T; apply T.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
55 56 57
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
58 59 60 61 62 63 64 65 66
Lemma FtoR_F2R: forall (f:Float.float) (g: float beta), Float.Fnum f = Fnum g -> Float.Fexp f = Fexp g -> 
  FtoR beta f = F2R g.
Proof.
intros f g H1 H2; unfold FtoR, F2R.
rewrite H1, H2, Z2R_IZR.
now rewrite bpow_powerRZ, Z2R_IZR.
Qed.


67 68 69
End Bounds.
Section b_Bounds.

70
Definition bsingle := make_bound radix2 24 (-149)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
71 72

Lemma psGivesBound: Zpos (vNum bsingle) = Zpower_nat 2 24.
73 74
unfold bsingle; apply make_bound_p.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
75 76
Qed.

77
Definition bdouble := make_bound radix2 53 1074.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
78 79

Lemma pdGivesBound: Zpos (vNum bdouble) = Zpower_nat 2 53.
80 81
unfold bdouble; apply make_bound_p.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
82 83
Qed.

84
End b_Bounds.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
85
Section Equiv.
86

87
Variable beta: radix.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
88
Variable b : Fbound.
89
Variable p : Z.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
90

91
Hypothesis pGivesBound : Zpos (vNum b) = Zpower_nat beta (Zabs_nat p).
92
Hypothesis precisionNotZero : (1 < p)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
93 94


BOLDO Sylvie's avatar
BOLDO Sylvie committed
95
Lemma pff_format_is_format: forall f, Fbounded b f ->
96
  (generic_format beta (FLT_exp (-dExp b) p) (FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
97 98
intros f Hf.
apply generic_format_FLT; auto with zarith.
99
exists (Float beta (Float.Fnum f) (Float.Fexp f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
100 101
simpl; split.
unfold F2R, FtoR; simpl.
102
rewrite <- 2!Z2R_IZR.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
103 104 105 106 107 108 109 110 111 112
rewrite bpow_powerRZ.
reflexivity.
split; destruct Hf.
apply Zlt_le_trans with (1:=H).
rewrite pGivesBound.
rewrite Zpower_Zpower_nat; auto with zarith.
exact H0.
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146
Lemma format_is_pff_format': forall r,
   (generic_format beta (FLT_exp (-dExp b) p) r) ->
    Fbounded b (Float.Float (Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) r))
                            (canonic_exp beta (FLT_exp (-dExp b) p) r)).
Proof.
intros x; unfold generic_format.
set (ex := canonic_exp beta (FLT_exp (-dExp b) p) x).
set (mx := Ztrunc (scaled_mantissa beta (FLT_exp (-dExp b) p) x)).
intros Hx; repeat split ; simpl.
apply lt_Z2R.
rewrite pGivesBound, Z2R_Zpower_nat. 
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.
unfold canonic_exp in ex.
destruct (ln_beta beta x) as (ex', He).
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
147
Lemma format_is_pff_format: forall r,
148 149
  (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
150
intros r Hr.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
151 152 153 154
eexists; split.
2: apply (format_is_pff_format' _ Hr).
rewrite Hr at 3; unfold FtoR, F2R; simpl.
now rewrite Z2R_IZR, bpow_powerRZ, Z2R_IZR.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
155 156 157
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
158

BOLDO Sylvie's avatar
BOLDO Sylvie committed
159
Lemma equiv_RNDs_aux: forall z, Zeven z = true -> Even z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
160 161 162 163 164 165 166 167 168 169 170 171 172 173 174
intros z; unfold Zeven, Even.
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.

175 176 177
Lemma pff_canonic_is_canonic: forall f, Fcanonic beta b f -> FtoR beta f <> 0 ->
  canonic beta (FLT_exp (- dExp b) p)
    (Float beta (Float.Fnum f) (Float.Fexp f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
178
intros f Hf1 Hf2; unfold canonic; simpl.
179
assert (K:(F2R (Float beta (Float.Fnum f) (Float.Fexp f)) = FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
180
unfold FtoR, F2R; simpl.
181
rewrite bpow_powerRZ; rewrite <- 2!Z2R_IZR; reflexivity.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
182 183
unfold canonic_exp, FLT_exp.
rewrite K.
184
destruct (ln_beta beta (FtoR beta f)) as (e, He).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
185 186 187 188 189 190 191 192
simpl; destruct Hf1.
(* . *)
destruct H as (H1,H2).
cut (Float.Fexp f = e-p)%Z.
intros V; rewrite V.
apply sym_eq; apply Zmax_left.
rewrite <- V; destruct H1; auto with zarith.
assert (e = Float.Fexp f + p)%Z;[idtac|omega].
193
apply trans_eq with (ln_beta beta (FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
194 195 196 197 198
apply sym_eq; apply ln_beta_unique.
apply He; assumption.
apply ln_beta_unique.
rewrite <- K; unfold F2R; simpl.
rewrite Rabs_mult.
199
rewrite (Rabs_right (bpow beta (Float.Fexp f))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
200 201 202 203 204 205 206
2: apply Rle_ge; apply bpow_ge_0.
split.
replace (Float.Fexp f + p - 1)%Z with ((p-1)+Float.Fexp f)%Z by ring.
rewrite bpow_plus.
apply Rmult_le_compat_r.
apply bpow_ge_0.
(* .. *)
207 208 209 210
apply Rmult_le_reg_l with (Z2R beta).
replace 0%R with (Z2R 0) by reflexivity.
apply Z2R_lt.
apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
211
rewrite <- bpow_plus1.
212
replace (p-1+1)%Z with (Z_of_nat (Zabs_nat p)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
213
rewrite <- Z2R_Zpower_nat.
214
simpl; rewrite <- pGivesBound, 3!Z2R_IZR.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
215 216 217
rewrite Rabs_Zabs.
rewrite <- mult_IZR.
apply IZR_le.
218
rewrite <- (Zabs_eq (beta)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
219 220
rewrite <- Zabs.Zabs_Zmult.
assumption.
221
apply Zlt_le_weak; apply radix_gt_0.
222 223
rewrite inj_abs; try ring.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
224 225 226 227
(* .. *)
rewrite Zplus_comm, bpow_plus.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
228
rewrite <- (inj_abs p);[idtac|omega].
BOLDO Sylvie's avatar
BOLDO Sylvie committed
229 230 231 232 233 234 235 236 237 238
rewrite <- Z2R_Zpower_nat.
simpl; rewrite <- pGivesBound, 2!Z2R_IZR.
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].
239 240
apply lt_bpow with beta.
apply Rle_lt_trans with (Rabs (FtoR beta f)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
241
apply He; auto.
242
apply Rlt_le_trans with (FtoR beta (firstNormalPos beta b (Zabs_nat p))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
243
rewrite <- Fabs_correct.
244
2: apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
245
apply FsubnormalLtFirstNormalPos; auto with zarith.
246
apply radix_gt_1.
247 248
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
249
apply FsubnormFabs; auto with zarith.
250
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
251 252
split; [idtac|split]; assumption.
rewrite Fabs_correct; auto with real zarith.
253
apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
254 255
unfold firstNormalPos, FtoR, nNormMin.
simpl.
256 257 258
replace (IZR (Zpower_nat beta (Peano.pred (Zabs_nat p)))) with (bpow beta (p-1)).
rewrite <- Z2R_IZR.
rewrite <- (bpow_powerRZ _).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
259 260
rewrite <- bpow_plus.
apply bpow_le.
261 262
omega.
replace (p-1)%Z with (Z_of_nat (Peano.pred (Zabs_nat p))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
263 264
rewrite <- Z2R_Zpower_nat.
rewrite Z2R_IZR; reflexivity.
265 266 267 268
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
269 270 271
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
272
Lemma pff_round_NE_is_round: forall (r:R),
273 274 275
   (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
276
intros.
277 278
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
279 280 281 282
apply round_NE_pt; auto with zarith.
apply FLT_exp_valid.
unfold Prec_gt_0; auto with zarith.
apply exists_NE_FLT.
283
now right.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
284 285
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
286
destruct (format_is_pff_format _ H1) as (f,(Hf1,Hf2)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
287
rewrite <- Hf1.
288
generalize (EvenClosestUniqueP b beta (Zabs_nat p)); unfold UniqueP; intros T.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
289
apply sym_eq; apply T with r; auto with zarith; clear T.
290
apply radix_gt_1.
291 292
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
293 294 295 296 297
split.
(* *)
split; auto; intros g Hg.
rewrite Hf1.
apply H2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
298
apply pff_format_is_format; auto.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
299
(* *)
300
case (Req_dec (FtoR beta (Fnormalize beta b (Zabs_nat p) f))  0%R); intros L.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
301 302 303 304 305
left.
unfold FNeven, Feven, Even.
exists 0%Z.
rewrite Zmult_0_r.
apply eq_IZR.
306
apply Rmult_eq_reg_l with (powerRZ beta (Float.Fexp (Fnormalize beta b (Zabs_nat p) f)))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
307 308 309
simpl (IZR 0); rewrite Rmult_0_r.
rewrite <- L; unfold FtoR; simpl; ring.
apply powerRZ_NOR; auto with zarith real.
310 311
apply Rgt_not_eq; replace 0%R with (IZR 0) by reflexivity.
apply IZR_lt; apply radix_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
312 313 314 315 316
destruct H3.
(* . *)
destruct H as (g,(Hg1,(Hg2,Hg3))).
left.
unfold FNeven, Feven.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
317
apply equiv_RNDs_aux.
318 319
replace (Float.Fnum (Fnormalize beta b (Zabs_nat p) f)) with (Fnum g); try assumption.
replace g with (Float beta (Float.Fnum (Fnormalize beta b (Zabs_nat p) f)) (Float.Fexp (Fnormalize beta b (Zabs_nat p) f))).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
320 321 322
easy.
apply canonic_unicity with (FLT_exp (- dExp b) p).
2: assumption.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
323
apply pff_canonic_is_canonic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
324
apply FnormalizeCanonic; auto with zarith real.
325
apply radix_gt_1.
326 327
intros KK; absurd (1 < p)%Z; try assumption.
apply Zle_not_lt; rewrite <- (inj_abs p); omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
328 329
exact L.
rewrite <- Hg1, <- Hf1.
330
rewrite <- FnormalizeCorrect with beta b (Zabs_nat p) f; auto with zarith.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
331 332
unfold F2R, FtoR; simpl.
rewrite Z2R_IZR, bpow_powerRZ.
333 334
rewrite Z2R_IZR; reflexivity.
apply radix_gt_1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
335 336 337 338 339
(* . *)
right; intros q (Hq1,Hq2).
rewrite Hf1.
apply H.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
340
apply pff_format_is_format; auto.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
341
intros g Hg.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
342
destruct (format_is_pff_format _ Hg) as (v,(Hv1,Hv2)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
343 344 345
rewrite <- Hv1.
apply Hq2; auto.
apply RND_EvenClosest_correct; auto with zarith.
346
apply radix_gt_1.
347 348
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
349 350 351
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
352
Lemma round_NE_is_pff_round: forall (r:R),
353 354
   exists f:Float.float, (Fcanonic beta b f /\ (EvenClosest b beta (Zabs_nat p) r f) /\
    FtoR beta f =  round beta (FLT_exp (-dExp b) p) rndNE r).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
355
intros r.
356
exists (RND_EvenClosest b beta (Zabs_nat p) r).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
357 358
split.
apply RND_EvenClosest_canonic; auto with zarith.
359
apply radix_gt_1.
360 361
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
362 363
split.
apply RND_EvenClosest_correct; auto with zarith.
364
apply radix_gt_1.
365 366
apply Nat2Z.inj_lt.
rewrite inj_abs; simpl; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
367
apply pff_round_NE_is_round.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
368 369 370
Qed.

End Equiv.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
371 372 373

Section Equiv_instanc.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
374
Lemma round_NE_is_pff_round_b32: forall (r:R),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
375
   exists f:Float.float, (Fcanonic 2 bsingle f /\ (EvenClosest bsingle 2 24 r f) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
376
    FtoR 2 f =  round radix2 (FLT_exp (-149) 24) rndNE r).
377
apply (round_NE_is_pff_round radix2 bsingle 24).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
378
apply psGivesBound.
379
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
380 381 382
Qed.


BOLDO Sylvie's avatar
BOLDO Sylvie committed
383
Lemma round_NE_is_pff_round_b64: forall (r:R),
Guillaume Melquiond's avatar
Guillaume Melquiond committed
384
   exists f:Float.float, (Fcanonic 2 bdouble f /\ (EvenClosest bdouble 2 53 r f) /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
385
    FtoR 2 f =  round radix2 (FLT_exp (-1074) 53) rndNE r).
386
apply (round_NE_is_pff_round radix2 bdouble 53).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
387
apply pdGivesBound.
388
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
389 390 391 392 393
Qed.



End Equiv_instanc.