Fcore_FLT.v 8.19 KB
Newer Older
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
6
#<br />#
7
Copyright (C) 2010-2013 Guillaume Melquiond
8 9 10 11 12 13 14 15 16 17 18 19

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

20
(** * Floating-point format with gradual underflow *)
21 22 23 24 25 26 27
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
Require Import Fcore_FLX.
Require Import Fcore_FIX.
28
Require Import Fcore_ulp.
29
Require Import Fcore_rnd_ne.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
30 31 32 33 34

Section RND_FLT.

Variable beta : radix.

35
Notation bpow e := (bpow beta e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
36 37

Variable emin prec : Z.
38 39

Context { prec_gt_0_ : Prec_gt_0 prec }.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
40

41 42 43
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
  exists f : float beta,
44
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
45

46 47
Definition FLT_exp e := Zmax (e - prec) emin.

48
(** Properties of the FLT format *)
49
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
50 51 52
Proof.
intros k.
unfold FLT_exp.
53 54 55
generalize (prec_gt_0 prec).
repeat split ;
  intros ; zify ; omega.
56 57
Qed.

58 59
Theorem generic_format_FLT :
  forall x, FLT_format x -> generic_format beta FLT_exp x.
60
Proof.
61
clear prec_gt_0_.
62 63 64
intros x ((mx, ex), (H1, (H2, H3))).
simpl in H2, H3.
rewrite H1.
65 66
apply generic_format_F2R.
intros Zmx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
67
unfold canonic_exp, FLT_exp.
68 69 70 71
rewrite ln_beta_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
72
now apply ln_beta_le_Zpower.
73 74 75 76 77 78
Qed.

Theorem FLT_format_generic :
  forall x, generic_format beta FLT_exp x -> FLT_format x.
Proof.
intros x.
79
unfold generic_format.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
80
set (ex := canonic_exp beta FLT_exp x).
81
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
82 83 84
intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
85
apply lt_Z2R.
86 87
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
88
apply bpow_gt_0.
89
rewrite <- bpow_plus.
90
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
91
rewrite F2R_Zabs.
92 93 94 95
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
96
unfold canonic_exp in ex.
97 98 99 100
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
101
apply bpow_le.
102 103
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
104 105
apply Zle_max_l.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
106 107
Qed.

108 109 110 111 112 113 114 115 116 117 118 119 120

Theorem FLT_format_bpow :
  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
Proof.
intros e He.
apply generic_format_bpow; unfold FLT_exp.
apply Z.max_case; try assumption.
unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.




121 122 123
Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
124
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
125
intros x.
126
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
127
apply FLT_format_generic.
128
apply generic_format_FLT.
129
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
130

131
Theorem canonic_exp_FLT_FLX :
Sylvie Boldo's avatar
Sylvie Boldo committed
132
  forall x,
133
  (bpow (emin + prec - 1) <= Rabs x)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
134
  canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
135
Proof.
Sylvie Boldo's avatar
Sylvie Boldo committed
136 137 138 139
intros x Hx.
assert (Hx0: x <> 0%R).
intros H1; rewrite H1, Rabs_R0 in Hx.
contradict Hx; apply Rlt_not_le, bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
140
unfold canonic_exp.
141 142
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
143 144 145
unfold FLX_exp. simpl.
specialize (He Hx0).
cut (emin + prec - 1 < ex)%Z. omega.
146
apply (lt_bpow beta).
147 148 149 150
apply Rle_lt_trans with (1 := Hx).
apply He.
Qed.

151
(** Links between FLT and FLX *)
152
Theorem generic_format_FLT_FLX :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
153 154
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
155 156
  generic_format beta (FLX_exp prec) x ->
  generic_format beta FLT_exp x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
157
Proof.
158
intros x Hx H.
159 160
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
161
apply generic_format_0.
162
unfold generic_format, scaled_mantissa.
163
now rewrite canonic_exp_FLT_FLX.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
164 165
Qed.

166
Theorem generic_format_FLX_FLT :
167 168 169
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.
170
clear prec_gt_0_.
171 172
intros x Hx.
unfold generic_format in Hx; rewrite Hx.
173 174
apply generic_format_F2R.
intros _.
175
rewrite <- Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
176
unfold canonic_exp, FLX_exp, FLT_exp.
177 178 179
apply Zle_max_l.
Qed.

180
Theorem round_FLT_FLX : forall rnd x,
181
  (bpow (emin + prec - 1) <= Rabs x)%R ->
182
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
183
intros rnd x Hx.
184
unfold round, scaled_mantissa.
185
rewrite canonic_exp_FLT_FLX ; trivial.
186 187
Qed.

188
(** Links between FLT and FIX (underflow) *)
189
Theorem canonic_exp_FLT_FIX :
190 191
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
192
  canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
193 194
Proof.
intros x Hx0 Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
195
unfold canonic_exp.
196 197
apply Zmax_right.
unfold FIX_exp.
198 199 200
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
201
apply (lt_bpow beta).
202 203 204 205
apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.

206
Theorem generic_format_FIX_FLT :
207 208 209 210
  forall x : R,
  generic_format beta FLT_exp x ->
  generic_format beta (FIX_exp emin) x.
Proof.
211
clear prec_gt_0_.
212 213
intros x Hx.
rewrite Hx.
214 215
apply generic_format_F2R.
intros _.
216 217 218 219
rewrite <- Hx.
apply Zle_max_r.
Qed.

220
Theorem generic_format_FLT_FIX :
221 222
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
223 224
  generic_format beta (FIX_exp emin) x ->
  generic_format beta FLT_exp x.
225 226 227
Proof with auto with typeclass_instances.
apply generic_inclusion_le...
intros e He.
228
unfold FIX_exp.
229 230 231
apply Zmax_lub.
omega.
apply Zle_refl.
232 233
Qed.

234 235 236 237 238 239 240
Theorem ulp_FLT_small: forall x, (Rabs x < bpow (emin+prec))%R ->
    ulp beta FLT_exp x = bpow emin.
Proof with auto with typeclass_instances.
intros x Hx.
unfold ulp; case Req_bool_spec; intros Hx2.
(* x = 0 *)
case (negligible_exp_spec FLT_exp).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
241
intros T; specialize (T (emin-1)%Z); contradict T.
242 243 244 245 246
apply Zle_not_lt; unfold FLT_exp.
apply Zle_trans with (2:=Z.le_max_r _ _); omega.
assert (V:FLT_exp emin = emin).
unfold FLT_exp; apply Z.max_r.
unfold Prec_gt_0 in prec_gt_0_; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
247
intros n H2; rewrite <-V.
248 249 250 251 252 253 254 255 256 257 258 259
apply f_equal, fexp_negligible_exp_eq...
omega.
(* x <> 0 *)
apply f_equal; unfold canonic_exp, FLT_exp.
apply Z.max_r.
assert (ln_beta beta x-1 < emin+prec)%Z;[idtac|omega].
destruct (ln_beta beta x) as (e,He); simpl.
apply lt_bpow with beta.
apply Rle_lt_trans with (2:=Hx).
now apply He.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301
Theorem ulp_FLT_le: forall x, (bpow (emin+prec) <= Rabs x)%R ->
  (ulp beta FLT_exp x <= Rabs x * bpow (1-prec))%R.
Proof.
intros x Hx.
assert (x <> 0)%R.
intros Z; contradict Hx; apply Rgt_not_le, Rlt_gt.
rewrite Z, Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0; try assumption.
unfold canonic_exp, FLT_exp.
destruct (ln_beta beta x) as (e,He).
apply Rle_trans with (bpow (e-1)*bpow (1-prec))%R.
rewrite <- bpow_plus.
right; apply f_equal.
apply trans_eq with (e-prec)%Z;[idtac|ring].
simpl; apply Z.max_l.
assert (emin+prec <= e)%Z; try omega.
apply le_bpow with beta.
apply Rle_trans with (1:=Hx).
left; now apply He.
apply Rmult_le_compat_r.
apply bpow_ge_0.
now apply He.
Qed.


Theorem ulp_FLT_ge: forall x, (Rabs x * bpow (-prec) < ulp beta FLT_exp x)%R.
Proof.
intros x; case (Req_dec x 0); intros Hx.
rewrite Hx, ulp_FLT_small, Rabs_R0, Rmult_0_l; try apply bpow_gt_0.
rewrite Rabs_R0; apply bpow_gt_0.
rewrite ulp_neq_0; try exact Hx.
unfold canonic_exp, FLT_exp.
apply Rlt_le_trans with (bpow (ln_beta beta x)*bpow (-prec))%R.
apply Rmult_lt_compat_r.
apply bpow_gt_0.
now apply bpow_ln_beta_gt.
rewrite <- bpow_plus.
apply bpow_le.
apply Z.le_max_l.
Qed.


302

303
(** FLT is a nice format: it has a monotone exponent... *)
304
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
305
Proof.
306
intros ex ey.
307
unfold FLT_exp.
308
zify ; omega.
309 310
Qed.

311
(** and it allows a rounding to nearest, ties to even. *)
312
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
313

314
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
315
Proof.
316
destruct NE_prop as [H|H].
317 318 319 320
now left.
right.
intros e.
unfold FLT_exp.
321 322
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
323 324 325 326 327 328 329 330
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
331
End RND_FLT.