Fcore_FTZ.v 9.04 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(*
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010 Sylvie Boldo
Copyright (C) 2010 Guillaume Melquiond

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

19 20 21 22 23 24
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.
25 26 27 28 29

Section RND_FTZ.

Variable beta : radix.

30
Notation bpow e := (bpow beta e).
31 32 33 34 35 36 37

Variable emin prec : Z.
Variable Hp : Zlt 0 prec.

(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
  exists f : float beta,
38
  x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
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
  (emin <= Fexp f)%Z.

Definition FTZ_RoundingModeP (rnd : R -> R):=
  Rounding_for_Format FTZ_format rnd.

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

Theorem FTZ_exp_correct : valid_exp FTZ_exp.
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).
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.
split ; intros ; omega.
Qed.

Theorem FTZ_format_generic :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
70
  forall x : R, FTZ_format x <-> generic_format beta FTZ_exp x.
71 72 73
Proof.
split.
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
74 75 76 77 78
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
79 80 81 82
rewrite Hx1.
apply generic_format_canonic_exponent.
unfold canonic_exponent, FTZ_exp.
rewrite <- Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
83 84 85 86 87
destruct (ln_beta beta x) as (ex, Hx6).
simpl.
specialize (Hx6 Hx4).
generalize (Zlt_cases (ex - prec) emin).
case (Zlt_bool (ex - prec) emin) ; intros H1.
88
elim (Rlt_not_le _ _ (proj2 Hx6)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
89
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
90
rewrite <- bpow_plus.
91
apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
92
omega.
93
rewrite Hx1, abs_F2R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
94 95
unfold F2R. simpl.
apply Rmult_le_compat.
96 97
apply bpow_ge_0.
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
98 99 100 101
rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
102
now apply -> bpow_le.
103 104 105 106 107 108 109 110
cut (ex - 1 < prec + xe)%Z. omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := proj1 Hx6).
rewrite Hx1.
apply F2R_lt_bpow.
simpl.
ring_simplify (prec + xe - xe)%Z.
apply Hx2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
111
(* . *)
112
intros Hx.
113 114 115 116 117 118 119 120 121
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.
122
unfold generic_format, scaled_mantissa, canonic_exponent, FTZ_exp in Hx.
123
destruct (ln_beta beta x) as (ex, Hx4).
124
simpl in Hx.
125
specialize (Hx4 Hx3).
126
generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
127 128 129
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
130
rewrite Hx2, abs_F2R.
131 132 133 134
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
now apply (Z2R_le 0 1).
135
apply bpow_ge_0.
136 137 138
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
139
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
140
apply bpow_gt_0.
141
rewrite Rmult_0_l.
142 143
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite <- abs_F2R, <- Hx2.
144
now apply Rabs_pos_lt.
145
apply -> bpow_le.
146
omega.
147 148
rewrite Hx2.
eexists ; repeat split ; simpl.
149 150 151
apply le_Z2R.
rewrite Z2R_Zpower.
apply Rmult_le_reg_r with (bpow (ex - prec)).
152
apply bpow_gt_0.
153
rewrite <- bpow_plus.
154
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
155 156
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
rewrite <- abs_F2R, <- Hx2.
157 158 159 160 161 162
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)).
163
apply bpow_gt_0.
164
rewrite <- bpow_plus.
165
replace (prec + (ex - prec))%Z with ex by ring.
166 167
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx2.
168 169 170 171 172
apply Hx4.
now apply Zlt_le_weak.
now apply Zge_le.
Qed.

173 174 175 176
Theorem FTZ_format_satisfies_any :
  satisfies_any FTZ_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FTZ_exp _)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
177 178 179
intros x.
apply iff_sym.
apply FTZ_format_generic.
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
exact FTZ_exp_correct.
Qed.

Theorem FTZ_format_FLXN :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  ( FTZ_format x <-> FLXN_format beta prec x ).
Proof.
intros x Hx.
split.
(* . *)
destruct (Req_dec x 0) as [H4|H4].
intros _.
rewrite H4.
apply -> FLX_format_FLXN.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
195
apply <- FLX_format_generic.
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
apply generic_format_0.
exact Hp.
exact Hp.
intros ((xm,xe),(H1,(H2,H3))).
specialize (H2 H4).
rewrite H1.
eexists. split. split.
now intros _.
(* . *)
intros ((xm,xe),(H1,H2)).
rewrite H1.
eexists. split. split. split.
now rewrite <- H1 at 1.
rewrite (Zsucc_pred emin).
apply Zlt_le_succ.
211
apply <- (bpow_lt beta).
212 213
apply Rmult_lt_reg_l with (Z2R (Zabs xm)).
apply Rmult_lt_reg_r with (bpow xe).
214
apply bpow_gt_0.
215 216 217
rewrite Rmult_0_l.
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (2 := Hx).
218
apply bpow_gt_0.
219 220 221
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (2 := Hx).
replace (emin + prec - 1)%Z with (prec + (emin - 1))%Z by ring.
222
rewrite bpow_plus.
223
apply Rmult_lt_compat_r.
224
apply bpow_gt_0.
225 226 227 228 229 230
rewrite <- Z2R_Zpower.
apply Z2R_lt.
apply H2.
intros H.
rewrite <- abs_F2R, <- H1, H, Rabs_right in Hx.
apply Rle_not_lt with (1 := Hx).
231
apply bpow_gt_0.
232 233 234 235
apply Rle_refl.
now apply Zlt_le_weak.
Qed.

236
Section FTZ_round.
237

238
Hypothesis rnd : Zround.
239

240 241
Definition Zrnd_FTZ x :=
  if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0.
242 243

Theorem Z_FTZ_Z2R :
244
  forall n, Zrnd_FTZ (Z2R n) = n.
245
Proof.
246
intros n.
247 248 249 250
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R.
case Rle_bool_spec.
easy.
251
rewrite <- Z2R_abs.
252 253 254 255 256 257 258
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.

Theorem Z_FTZ_monotone :
259 260
  forall x y, (x <= y)%R ->
  (Zrnd_FTZ x <= Zrnd_FTZ y)%Z.
261
Proof.
262
intros x y Hxy.
263 264 265 266 267 268
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
  case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
now apply Zrnd_monotone.
269
rewrite <- (Zrnd_Z2R rnd 0).
270 271
apply Zrnd_monotone.
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
272
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
273 274 275 276 277 278
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 *)
279
rewrite <- (Zrnd_Z2R rnd 0).
280 281 282
apply Zrnd_monotone.
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
283
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
284 285 286 287 288 289
elim Rle_not_lt with (1 := Hy1).
apply Rlt_le_trans with (2 := Hxy).
apply (Rabs_def2 _ _ Hx).
exact Hy1.
Qed.

290
Definition ZrFTZ := mkZround Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R.
291

292
Theorem FTZ_round :
293 294
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
295
  round beta FTZ_exp ZrFTZ x = round beta (FLX_exp prec) rnd x.
296 297
Proof.
intros x Hx.
298
unfold round, scaled_mantissa, canonic_exponent.
299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317
destruct (ln_beta beta x) as (ex, He). simpl.
unfold Zrnd_FTZ.
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).
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)).
318
rewrite bpow_plus.
319 320 321 322 323 324 325 326 327 328 329 330 331 332
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rle_trans with (2 := proj1 He).
apply -> bpow_le.
unfold FLX_exp.
omega.
apply bpow_ge_0.
unfold FLX_exp, FTZ_exp.
generalize (Zlt_cases (ex - prec) emin).
case Zlt_bool.
omega.
easy.
Qed.

333
Theorem FTZ_round_small :
334 335
  forall x : R,
  (Rabs x < bpow (emin + prec - 1))%R ->
336
  round beta FTZ_exp ZrFTZ x = R0.
337 338 339 340
Proof.
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
341 342
apply round_0.
unfold round, scaled_mantissa, canonic_exponent.
343 344 345 346 347 348 349 350 351
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)).
352
rewrite bpow_plus.
353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
apply Rmult_lt_compat_r.
apply bpow_gt_0.
apply Rlt_le_trans with (1 := Hx).
apply -> bpow_le.
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).
apply -> bpow_le.
omega.
apply bpow_ge_0.
Qed.

370
End FTZ_round.
371

372
End RND_FTZ.