Fcore_FTZ.v 5.2 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,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
20
  x = F2R f /\ (x <> R0 -> Zpower (radix_val beta) (prec - 1) <= Zabs (Fnum f) < Zpower (radix_val 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 61 62 63 64 65 66 67 68 69 70
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
specialize (Hx2 Hx4).
unfold generic_format, canonic, FTZ_exp.
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.
elim (Rlt_not_ge _ _ (proj2 Hx6)).
apply Rle_ge.
rewrite Hx1.
apply Rle_trans with (bpow (prec - 1) * bpow emin)%R.
71 72
rewrite <- bpow_add.
apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
73 74 75 76
omega.
rewrite abs_F2R.
unfold F2R. simpl.
apply Rmult_le_compat.
77 78
apply bpow_ge_0.
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
79 80 81 82
rewrite <- Z2R_Zpower.
now apply Z2R_le.
apply Zle_minus_le_0.
now apply (Zlt_le_succ 0).
83
now apply -> bpow_le.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
84 85 86 87
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec (proj2 Hx2)).
now eexists.
now rewrite <- Hx1.
(* . *)
88 89 90 91 92 93 94 95 96 97
intros ((xm, xe), (Hx1, Hx2)).
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.
98
destruct (ln_beta beta x) as (ex, Hx4).
99
simpl in Hx2.
100
specialize (Hx4 Hx3).
101 102 103 104 105 106 107 108 109 110
unfold FTZ_exp in Hx2.
generalize (Zlt_cases (ex - prec) emin) Hx2. clear Hx2.
case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2.
elim Rlt_not_ge with (1 := proj2 Hx4).
apply Rle_ge.
rewrite Hx1, abs_F2R.
rewrite <- (Rmult_1_l (bpow ex)).
unfold F2R. simpl.
apply Rmult_le_compat.
now apply (Z2R_le 0 1).
111
apply bpow_ge_0.
112 113 114 115
apply (Z2R_le 1).
apply (Zlt_le_succ 0).
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow xe).
116
apply bpow_gt_0.
117 118 119 120
rewrite Rmult_0_l.
change (0 < F2R (Float beta (Zabs xm) xe))%R.
rewrite <- abs_F2R, <- Hx1.
now apply Rabs_pos_lt.
121
apply -> bpow_le.
122 123 124 125 126 127 128 129 130 131
omega.
exists (Float beta xm xe).
split.
exact Hx1.
split.
intros _.
split.
apply le_Z2R.
rewrite Z2R_Zpower.
apply Rmult_le_reg_r with (bpow (ex - prec)).
132 133
apply bpow_gt_0.
rewrite <- bpow_add.
134 135 136 137 138 139 140 141 142 143
replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring.
rewrite <- Hx2.
change (bpow (ex - 1) <= F2R (Float beta (Zabs xm) xe))%R.
rewrite <- abs_F2R, <- Hx1.
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)).
144 145
apply bpow_gt_0.
rewrite <- bpow_add.
146 147 148 149 150 151 152 153 154 155 156
replace (prec + (ex - prec))%Z with ex by ring.
rewrite <- Hx2.
change (F2R (Float beta (Zabs xm) xe) < bpow ex)%R.
rewrite <- abs_F2R, <- Hx1.
apply Hx4.
now apply Zlt_le_weak.
simpl.
rewrite Hx2.
now apply Zge_le.
Qed.

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

End RND_FTZ.