Fcore_FTZ.v 8.43 KB
Newer Older
1 2 3 4 5 6
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.
7 8 9 10 11

Section RND_FTZ.

Variable beta : radix.

12
Notation bpow e := (bpow beta e).
13 14 15 16 17 18 19

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

(* floating-point format with abrupt underflow *)
Definition FTZ_format (x : R) :=
  exists f : float beta,
20
  x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\
21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
  (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
52
  forall x : R, FTZ_format x <-> generic_format beta FTZ_exp x.
53 54 55
Proof.
split.
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
56 57 58 59 60
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
61 62 63 64
rewrite Hx1.
apply generic_format_canonic_exponent.
unfold canonic_exponent, FTZ_exp.
rewrite <- Hx1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
65 66 67 68 69
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.
70
elim (Rlt_not_le _ _ (proj2 Hx6)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
71
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
72 73
rewrite <- bpow_add.
apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
74
omega.
75
rewrite Hx1, abs_F2R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
76 77
unfold F2R. simpl.
apply Rmult_le_compat.
78 79
apply bpow_ge_0.
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
80 81 82 83
rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
84
now apply -> bpow_le.
85 86 87 88 89 90 91 92
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
93
(* . *)
94
intros Hx.
95 96 97 98 99 100 101 102 103
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.
104
unfold generic_format, scaled_mantissa, canonic_exponent, FTZ_exp in Hx.
105
destruct (ln_beta beta x) as (ex, Hx4).
106
simpl in Hx.
107
specialize (Hx4 Hx3).
108
generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx.
109 110 111
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
112
rewrite Hx2, abs_F2R.
113 114 115 116
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
now apply (Z2R_le 0 1).
117
apply bpow_ge_0.
118 119 120
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
121
apply Rmult_lt_reg_r with (bpow (emin + prec - 1)).
122
apply bpow_gt_0.
123
rewrite Rmult_0_l.
124 125
change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R.
rewrite <- abs_F2R, <- Hx2.
126
now apply Rabs_pos_lt.
127
apply -> bpow_le.
128
omega.
129 130
rewrite Hx2.
eexists ; repeat split ; simpl.
131 132 133
apply le_Z2R.
rewrite Z2R_Zpower.
apply Rmult_le_reg_r with (bpow (ex - prec)).
134 135
apply bpow_gt_0.
rewrite <- bpow_add.
136
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
137 138
change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R.
rewrite <- abs_F2R, <- Hx2.
139 140 141 142 143 144
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)).
145 146
apply bpow_gt_0.
rewrite <- bpow_add.
147
replace (prec + (ex - prec))%Z with ex by ring.
148 149
change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx2.
150 151 152 153 154
apply Hx4.
now apply Zlt_le_weak.
now apply Zge_le.
Qed.

155 156 157 158
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
159 160 161
intros x.
apply iff_sym.
apply FTZ_format_generic.
162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
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
177
apply <- FLX_format_generic.
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192
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.
193
apply <- (bpow_lt beta).
194 195
apply Rmult_lt_reg_l with (Z2R (Zabs xm)).
apply Rmult_lt_reg_r with (bpow xe).
196
apply bpow_gt_0.
197 198 199
rewrite Rmult_0_l.
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (2 := Hx).
200
apply bpow_gt_0.
201 202 203
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.
204
rewrite bpow_add.
205
apply Rmult_lt_compat_r.
206
apply bpow_gt_0.
207 208 209 210 211 212
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).
213
apply bpow_gt_0.
214 215 216 217
apply Rle_refl.
now apply Zlt_le_weak.
Qed.

218 219 220 221
Section FTZ_rounding.

Hypothesis rnd : Zrounding.

222 223
Definition Zrnd_FTZ x :=
  if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0.
224 225

Theorem Z_FTZ_Z2R :
226
  forall n, Zrnd_FTZ (Z2R n) = n.
227
Proof.
228
intros n.
229 230 231 232 233 234 235 236 237 238 239 240
unfold Zrnd_FTZ.
rewrite Zrnd_Z2R.
case Rle_bool_spec.
easy.
rewrite <- abs_Z2R.
intros H.
generalize (lt_Z2R _ 1 H).
clear.
now case n ; trivial ; simpl ; intros [p|p|].
Qed.

Theorem Z_FTZ_monotone :
241 242
  forall x y, (x <= y)%R ->
  (Zrnd_FTZ x <= Zrnd_FTZ y)%Z.
243
Proof.
244
intros x y Hxy.
245 246 247 248 249 250
unfold Zrnd_FTZ.
case Rle_bool_spec ; intros Hx ;
  case Rle_bool_spec ; intros Hy.
4: easy.
(* 1 <= |x| *)
now apply Zrnd_monotone.
251
rewrite <- (Zrnd_Z2R rnd 0).
252 253
apply Zrnd_monotone.
apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le.
254
destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1].
255 256 257 258 259 260
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 *)
261
rewrite <- (Zrnd_Z2R rnd 0).
262 263 264
apply Zrnd_monotone.
apply Rle_trans with (Z2R 1).
now apply Z2R_le.
265
destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1].
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 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353
elim Rle_not_lt with (1 := Hy1).
apply Rlt_le_trans with (2 := Hxy).
apply (Rabs_def2 _ _ Hx).
exact Hy1.
Qed.

Definition ZrFTZ := mkZrounding Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R.

Theorem FTZ_rounding :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  rounding beta FTZ_exp ZrFTZ x = rounding beta (FLX_exp prec) rnd x.
Proof.
intros x Hx.
unfold rounding, scaled_mantissa, canonic_exponent.
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)).
rewrite bpow_add.
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.

Theorem FTZ_rounding_small :
  forall x : R,
  (Rabs x < bpow (emin + prec - 1))%R ->
  rounding beta FTZ_exp ZrFTZ x = R0.
Proof.
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
apply rounding_0.
unfold rounding, scaled_mantissa, canonic_exponent.
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)).
rewrite bpow_add.
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.

End FTZ_rounding.

354
End RND_FTZ.