Fcore_FTZ.v 8.67 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 abrupt underflow *)
21 22 23 24 25
Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_float_prop.
26
Require Import Fcore_ulp.
27
Require Import Fcore_FLX.
28 29 30 31 32

Section RND_FTZ.

Variable beta : radix.

33
Notation bpow e := (bpow beta e).
34 35

Variable emin prec : Z.
36 37

Context { prec_gt_0_ : Prec_gt_0 prec }.
38 39 40 41

(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
  exists f : float beta,
42
  x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
43 44 45 46
  (emin <= Fexp f)%Z.

Definition FTZ_exp e := if Zlt_bool (e - prec) emin then (emin + prec - 1)%Z else (e - prec)%Z.

47
(** Properties of the FTZ format *)
48
Global Instance FTZ_exp_valid : Valid_exp FTZ_exp.
49 50 51 52 53 54 55 56 57 58 59 60
Proof.
intros k.
unfold FTZ_exp.
generalize (Zlt_cases (k - prec) emin).
case (Zlt_bool (k - prec) emin) ; intros H1.
split ; intros H2.
omega.
split.
generalize (Zlt_cases (emin + prec + 1 - prec) emin).
case (Zlt_bool (emin + prec + 1 - prec) emin) ; intros H3.
omega.
generalize (Zlt_cases (emin + prec - 1 + 1 - prec) emin).
61
generalize (prec_gt_0 prec).
62 63 64 65 66 67 68
case (Zlt_bool (emin + prec - 1 + 1 - prec) emin) ; omega.
intros l H3.
generalize (Zlt_cases (l - prec) emin).
case (Zlt_bool (l - prec) emin) ; omega.
split ; intros H2.
generalize (Zlt_cases (k + 1 - prec) emin).
case (Zlt_bool (k + 1 - prec) emin) ; omega.
69
generalize (prec_gt_0 prec).
70 71 72
split ; intros ; omega.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
73 74 75 76 77 78 79 80
Theorem FLXN_format_FTZ :
  forall x, FTZ_format x -> FLXN_format beta prec x.
Proof.
intros x ((xm, xe), (Hx1, (Hx2, Hx3))).
eexists.
apply (conj Hx1 Hx2).
Qed.

81 82
Theorem generic_format_FTZ :
  forall x, FTZ_format x -> generic_format beta FTZ_exp x.
83
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
intros x Hx.
cut (generic_format beta (FLX_exp prec) x).
apply generic_inclusion_ln_beta.
intros Zx.
destruct Hx as ((xm, xe), (Hx1, (Hx2, Hx3))).
simpl in Hx2, Hx3.
specialize (Hx2 Zx).
assert (Zxm: xm <> Z0).
contradict Zx.
rewrite Hx1, Zx.
apply F2R_0.
unfold FTZ_exp, FLX_exp.
rewrite Zlt_bool_false.
apply Zle_refl.
rewrite Hx1, ln_beta_F2R with (1 := Zxm).
cut (prec - 1 < ln_beta beta (Z2R xm))%Z.
clear -Hx3 ; omega.
101
apply ln_beta_gt_Zpower with (1 := Zxm).
102
apply Hx2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
103 104
apply generic_format_FLXN.
now apply FLXN_format_FTZ.
105 106 107 108 109 110
Qed.

Theorem FTZ_format_generic :
  forall x, generic_format beta FTZ_exp x -> FTZ_format x.
Proof.
intros x Hx.
111 112 113 114 115 116 117 118 119
destruct (Req_dec x 0) as [Hx3|Hx3].
exists (Float beta 0 emin).
split.
unfold F2R. simpl.
now rewrite Rmult_0_l.
split.
intros H.
now elim H.
apply Zle_refl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
120
unfold generic_format, scaled_mantissa, canonic_exp, FTZ_exp in Hx.
121
destruct (ln_beta beta x) as (ex, Hx4).
122
simpl in Hx.
123
specialize (Hx4 Hx3).
124
generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
125 126 127
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
128
rewrite Hx2, <- F2R_Zabs.
129 130 131 132
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
now apply (Z2R_le 0 1).
133
apply bpow_ge_0.
134 135 136
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
137
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
138
apply bpow_gt_0.
139
rewrite Rmult_0_l.
140
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
141
rewrite F2R_Zabs, <- Hx2.
142
now apply Rabs_pos_lt.
143
apply bpow_le.
144
omega.
145 146
rewrite Hx2.
eexists ; repeat split ; simpl.
147 148 149
apply le_Z2R.
rewrite Z2R_Zpower.
apply Rmult_le_reg_r with (bpow (ex - prec)).
150
apply bpow_gt_0.
151
rewrite <- bpow_plus.
152
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
153
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
154
rewrite F2R_Zabs, <- Hx2.
155 156 157 158 159 160
apply Hx4.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow (ex - prec)).
161
apply bpow_gt_0.
162
rewrite <- bpow_plus.
163
replace (prec + (ex - prec))%Z with ex by ring.
164
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
165
rewrite F2R_Zabs, <- Hx2.
166 167 168 169 170
apply Hx4.
now apply Zlt_le_weak.
now apply Zge_le.
Qed.

171 172 173
Theorem FTZ_format_satisfies_any :
  satisfies_any FTZ_format.
Proof.
174
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
175
intros x.
176
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
177
apply FTZ_format_generic.
178
apply generic_format_FTZ.
179 180 181 182 183
Qed.

Theorem FTZ_format_FLXN :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
184 185 186 187 188 189 190 191 192 193 194 195
  FLXN_format beta prec x -> FTZ_format x.
Proof.
intros x Hx Fx.
apply FTZ_format_generic.
apply generic_format_FLXN in Fx.
revert Hx Fx.
apply generic_inclusion_ge.
intros e He.
unfold FTZ_exp.
rewrite Zlt_bool_false.
apply Zle_refl.
omega.
196 197
Qed.

198 199 200 201
Theorem ulp_FTZ_0: ulp beta FTZ_exp 0 = bpow (emin+prec-1).
Proof with auto with typeclass_instances.
unfold ulp; rewrite Req_bool_true; trivial.
case (negligible_exp_spec FTZ_exp).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
202
intros T; specialize (T (emin-1)%Z); contradict T.
203 204 205 206
apply Zle_not_lt; unfold FTZ_exp; unfold Prec_gt_0 in prec_gt_0_.
rewrite Zlt_bool_true; omega.
assert (V:(FTZ_exp (emin+prec-1) = emin+prec-1)%Z).
unfold FTZ_exp; rewrite Zlt_bool_true; omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
207
intros n H2; rewrite <-V.
208 209 210 211 212
apply f_equal, fexp_negligible_exp_eq...
omega.
Qed.


213
Section FTZ_round.
214

215
(** Rounding with FTZ *)
216 217
Variable rnd : R -> Z.
Context { valid_rnd : Valid_rnd rnd }.
218

219
Definition Zrnd_FTZ x :=
220
  if Rle_bool R1 (Rabs x) then rnd x else Z0.
221

222 223 224 225
Global Instance valid_rnd_FTZ : Valid_rnd Zrnd_FTZ.
Proof with auto with typeclass_instances.
split.
(* *)
226
intros x y Hxy.
227 228 229 230 231
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
  case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
232
now apply Zrnd_le.
233
rewrite <- (Zrnd_Z2R rnd 0).
234
apply Zrnd_le...
235
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
236
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
237 238 239 240 241 242
exact Hx1.
elim Rle_not_lt with (1 := Hx1).
apply Rle_lt_trans with (2 := Hy).
apply Rle_trans with (1 := Hxy).
apply RRle_abs.
(* |x| < 1 *)
243
rewrite <- (Zrnd_Z2R rnd 0).
244
apply Zrnd_le...
245 246
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
247
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
248 249 250 251
elim Rle_not_lt with (1 := Hy1).
apply Rlt_le_trans with (2 := Hxy).
apply (Rabs_def2 _ _ Hx).
exact Hy1.
252 253 254 255 256 257 258 259 260 261 262
(* *)
intros n.
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R...
case Rle_bool_spec.
easy.
rewrite <- Z2R_abs.
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
263 264
Qed.

265
Theorem round_FTZ_FLX :
266 267
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
268
  round beta FTZ_exp Zrnd_FTZ x = round beta (FLX_exp prec) rnd x.
269 270
Proof.
intros x Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
271
unfold round, scaled_mantissa, canonic_exp.
272 273 274 275 276 277 278 279 280 281 282 283
destruct (ln_beta beta x) as (ex, He). simpl.
assert (Hx0: x <> R0).
intros Hx0.
apply Rle_not_lt with (1 := Hx).
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
specialize (He Hx0).
assert (He': (emin + prec <= ex)%Z).
apply (bpow_lt_bpow beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
replace (FTZ_exp ex) with (FLX_exp prec ex).
284
unfold Zrnd_FTZ.
285 286 287 288 289 290
rewrite Rle_bool_true.
apply refl_equal.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FLX_exp prec ex))).
change R1 with (bpow 0).
rewrite <- (Zplus_opp_r (FLX_exp prec ex)).
291
rewrite bpow_plus.
292 293 294
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rle_trans with (2 := proj1 He).
295
apply bpow_le.
296
unfold FLX_exp.
297 298
generalize (prec_gt_0 prec).
clear -He' ; omega.
299 300
apply bpow_ge_0.
unfold FLX_exp, FTZ_exp.
301 302 303
rewrite Zlt_bool_false.
apply refl_equal.
clear -He' ; omega.
304 305
Qed.

306
Theorem round_FTZ_small :
307 308
  forall x : R,
  (Rabs x < bpow (emin + prec - 1))%R ->
309 310
  round beta FTZ_exp Zrnd_FTZ x = R0.
Proof with auto with typeclass_instances.
311 312 313
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
314
apply round_0...
BOLDO Sylvie's avatar
BOLDO Sylvie committed
315
unfold round, scaled_mantissa, canonic_exp.
316 317 318 319 320 321 322 323 324
destruct (ln_beta beta x) as (ex, He). simpl.
specialize (He Hx0).
unfold Zrnd_FTZ.
rewrite Rle_bool_false.
apply F2R_0.
rewrite Rabs_mult.
rewrite (Rabs_pos_eq (bpow (- FTZ_exp ex))).
change R1 with (bpow 0).
rewrite <- (Zplus_opp_r (FTZ_exp ex)).
325
rewrite bpow_plus.
326 327 328
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Rlt_le_trans with (1 := Hx).
329
apply bpow_le.
330 331 332 333 334 335 336 337
unfold FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
case Zlt_bool.
intros _.
apply Zle_refl.
intros He'.
elim Rlt_not_le with (1 := Hx).
apply Rle_trans with (2 := proj1 He).
338
apply bpow_le.
339 340 341 342
omega.
apply bpow_ge_0.
Qed.

343
End FTZ_round.
344

345
End RND_FTZ.