Fcore_FTZ.v 8.4 KB
 Guillaume Melquiond committed Feb 24, 2010 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. `````` Guillaume Melquiond committed Sep 16, 2009 7 8 9 10 11 `````` Section RND_FTZ. Variable beta : radix. `````` Guillaume Melquiond committed Oct 29, 2009 12 ``````Notation bpow e := (bpow beta e). `````` Guillaume Melquiond committed Sep 16, 2009 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 committed Oct 01, 2010 20 `````` x = F2R f /\ (x <> R0 -> Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z /\ `````` Guillaume Melquiond committed Sep 16, 2009 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 committed Sep 23, 2009 52 `````` forall x : R, FTZ_format x <-> generic_format beta FTZ_exp x. `````` Guillaume Melquiond committed Sep 16, 2009 53 54 55 ``````Proof. split. (* . *) `````` Guillaume Melquiond committed Sep 23, 2009 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). `````` Guillaume Melquiond committed Mar 04, 2010 61 62 63 64 ``````rewrite Hx1. apply generic_format_canonic_exponent. unfold canonic_exponent, FTZ_exp. rewrite <- Hx1. `````` Guillaume Melquiond committed Sep 23, 2009 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. `````` Guillaume Melquiond committed Mar 04, 2010 70 ``````elim (Rlt_not_le _ _ (proj2 Hx6)). `````` Guillaume Melquiond committed Sep 23, 2009 71 ``````apply Rle_trans with (bpow (prec - 1) * bpow emin)%R. `````` Guillaume Melquiond committed Oct 01, 2010 72 ``````rewrite <- bpow_plus. `````` Guillaume Melquiond committed Oct 29, 2009 73 ``````apply -> bpow_le. `````` Guillaume Melquiond committed Sep 23, 2009 74 ``````omega. `````` Guillaume Melquiond committed Mar 04, 2010 75 ``````rewrite Hx1, abs_F2R. `````` Guillaume Melquiond committed Sep 23, 2009 76 77 ``````unfold F2R. simpl. apply Rmult_le_compat. `````` Guillaume Melquiond committed Oct 29, 2009 78 79 ``````apply bpow_ge_0. apply bpow_ge_0. `````` Guillaume Melquiond committed Sep 23, 2009 80 81 82 83 ``````rewrite <- Z2R_Zpower. now apply Z2R_le. apply Zle_minus_le_0. now apply (Zlt_le_succ 0). `````` Guillaume Melquiond committed Oct 29, 2009 84 ``````now apply -> bpow_le. `````` Guillaume Melquiond committed Mar 04, 2010 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 committed Sep 23, 2009 93 ``````(* . *) `````` Guillaume Melquiond committed Mar 04, 2010 94 ``````intros Hx. `````` Guillaume Melquiond committed Sep 16, 2009 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. `````` Guillaume Melquiond committed Mar 10, 2010 104 ``````unfold generic_format, scaled_mantissa, canonic_exponent, FTZ_exp in Hx. `````` Guillaume Melquiond committed Sep 23, 2009 105 ``````destruct (ln_beta beta x) as (ex, Hx4). `````` Guillaume Melquiond committed Mar 04, 2010 106 ``````simpl in Hx. `````` Guillaume Melquiond committed Sep 23, 2009 107 ``````specialize (Hx4 Hx3). `````` Guillaume Melquiond committed Mar 04, 2010 108 ``````generalize (Zlt_cases (ex - prec) emin) Hx. clear Hx. `````` Guillaume Melquiond committed Sep 16, 2009 109 110 111 ``````case (Zlt_bool (ex - prec) emin) ; intros Hx5 Hx2. elim Rlt_not_ge with (1 := proj2 Hx4). apply Rle_ge. `````` Guillaume Melquiond committed Mar 04, 2010 112 ``````rewrite Hx2, abs_F2R. `````` Guillaume Melquiond committed Sep 16, 2009 113 114 115 116 ``````rewrite <- (Rmult_1_l (bpow ex)). unfold F2R. simpl. apply Rmult_le_compat. now apply (Z2R_le 0 1). `````` Guillaume Melquiond committed Oct 29, 2009 117 ``````apply bpow_ge_0. `````` Guillaume Melquiond committed Sep 16, 2009 118 119 120 ``````apply (Z2R_le 1). apply (Zlt_le_succ 0). apply lt_Z2R. `````` Guillaume Melquiond committed Mar 04, 2010 121 ``````apply Rmult_lt_reg_r with (bpow (emin + prec - 1)). `````` Guillaume Melquiond committed Oct 29, 2009 122 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Sep 16, 2009 123 ``````rewrite Rmult_0_l. `````` Guillaume Melquiond committed Mar 04, 2010 124 125 ``````change (0 < F2R (Float beta (Zabs (Ztrunc (x * bpow (- (emin + prec - 1))))) (emin + prec - 1)))%R. rewrite <- abs_F2R, <- Hx2. `````` Guillaume Melquiond committed Sep 16, 2009 126 ``````now apply Rabs_pos_lt. `````` Guillaume Melquiond committed Oct 29, 2009 127 ``````apply -> bpow_le. `````` Guillaume Melquiond committed Sep 16, 2009 128 ``````omega. `````` Guillaume Melquiond committed Mar 04, 2010 129 130 ``````rewrite Hx2. eexists ; repeat split ; simpl. `````` Guillaume Melquiond committed Sep 16, 2009 131 132 133 ``````apply le_Z2R. rewrite Z2R_Zpower. apply Rmult_le_reg_r with (bpow (ex - prec)). `````` Guillaume Melquiond committed Oct 29, 2009 134 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Oct 01, 2010 135 ``````rewrite <- bpow_plus. `````` Guillaume Melquiond committed Sep 16, 2009 136 ``````replace (prec - 1 + (ex - prec))%Z with (ex - 1)%Z by ring. `````` Guillaume Melquiond committed Mar 04, 2010 137 138 ``````change (bpow (ex - 1) <= F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)))%R. rewrite <- abs_F2R, <- Hx2. `````` Guillaume Melquiond committed Sep 16, 2009 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)). `````` Guillaume Melquiond committed Oct 29, 2009 145 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Oct 01, 2010 146 ``````rewrite <- bpow_plus. `````` Guillaume Melquiond committed Sep 16, 2009 147 ``````replace (prec + (ex - prec))%Z with ex by ring. `````` Guillaume Melquiond committed Mar 04, 2010 148 149 ``````change (F2R (Float beta (Zabs (Ztrunc (x * bpow (- (ex - prec))))) (ex - prec)) < bpow ex)%R. rewrite <- abs_F2R, <- Hx2. `````` Guillaume Melquiond committed Sep 16, 2009 150 151 152 153 154 ``````apply Hx4. now apply Zlt_le_weak. now apply Zge_le. Qed. `````` Guillaume Melquiond committed Sep 16, 2009 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 committed Sep 23, 2009 159 160 161 ``````intros x. apply iff_sym. apply FTZ_format_generic. `````` Guillaume Melquiond committed Sep 16, 2009 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 committed Sep 23, 2009 177 ``````apply <- FLX_format_generic. `````` Guillaume Melquiond committed Sep 16, 2009 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. `````` Guillaume Melquiond committed Oct 29, 2009 193 ``````apply <- (bpow_lt beta). `````` Guillaume Melquiond committed Sep 16, 2009 194 195 ``````apply Rmult_lt_reg_l with (Z2R (Zabs xm)). apply Rmult_lt_reg_r with (bpow xe). `````` Guillaume Melquiond committed Oct 29, 2009 196 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Sep 16, 2009 197 198 199 ``````rewrite Rmult_0_l. rewrite H1, abs_F2R in Hx. apply Rlt_le_trans with (2 := Hx). `````` Guillaume Melquiond committed Oct 29, 2009 200 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Sep 16, 2009 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. `````` Guillaume Melquiond committed Oct 01, 2010 204 ``````rewrite bpow_plus. `````` Guillaume Melquiond committed Sep 16, 2009 205 ``````apply Rmult_lt_compat_r. `````` Guillaume Melquiond committed Oct 29, 2009 206 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Sep 16, 2009 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). `````` Guillaume Melquiond committed Oct 29, 2009 213 ``````apply bpow_gt_0. `````` Guillaume Melquiond committed Sep 16, 2009 214 215 216 217 ``````apply Rle_refl. now apply Zlt_le_weak. Qed. `````` Guillaume Melquiond committed Oct 01, 2010 218 ``````Section FTZ_round. `````` Guillaume Melquiond committed Sep 14, 2010 219 `````` `````` Guillaume Melquiond committed Oct 01, 2010 220 ``````Hypothesis rnd : Zround. `````` Guillaume Melquiond committed Sep 14, 2010 221 `````` `````` 222 223 ``````Definition Zrnd_FTZ x := if Rle_bool R1 (Rabs x) then Zrnd rnd x else Z0. `````` Guillaume Melquiond committed Sep 14, 2010 224 225 `````` Theorem Z_FTZ_Z2R : `````` 226 `````` forall n, Zrnd_FTZ (Z2R n) = n. `````` Guillaume Melquiond committed Sep 14, 2010 227 ``````Proof. `````` 228 ``````intros n. `````` Guillaume Melquiond committed Sep 14, 2010 229 230 231 232 ``````unfold Zrnd_FTZ. rewrite Zrnd_Z2R. case Rle_bool_spec. easy. `````` Guillaume Melquiond committed Oct 01, 2010 233 ``````rewrite <- Z2R_abs. `````` Guillaume Melquiond committed Sep 14, 2010 234 235 236 237 238 239 240 ``````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. `````` Guillaume Melquiond committed Sep 14, 2010 243 ``````Proof. `````` 244 ``````intros x y Hxy. `````` Guillaume Melquiond committed Sep 14, 2010 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). `````` Guillaume Melquiond committed Sep 14, 2010 252 253 ``````apply Zrnd_monotone. apply Rle_trans with (Z2R (-1)). 2: now apply Z2R_le. `````` Guillaume Melquiond committed Sep 22, 2010 254 ``````destruct (Rabs_ge_inv _ _ Hx) as [Hx1|Hx1]. `````` Guillaume Melquiond committed Sep 14, 2010 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). `````` Guillaume Melquiond committed Sep 14, 2010 262 263 264 ``````apply Zrnd_monotone. apply Rle_trans with (Z2R 1). now apply Z2R_le. `````` Guillaume Melquiond committed Sep 22, 2010 265 ``````destruct (Rabs_ge_inv _ _ Hy) as [Hy1|Hy1]. `````` Guillaume Melquiond committed Sep 14, 2010 266 267 268 269 270 271 ``````elim Rle_not_lt with (1 := Hy1). apply Rlt_le_trans with (2 := Hxy). apply (Rabs_def2 _ _ Hx). exact Hy1. Qed. `````` Guillaume Melquiond committed Oct 01, 2010 272 ``````Definition ZrFTZ := mkZround Zrnd_FTZ Z_FTZ_monotone Z_FTZ_Z2R. `````` Guillaume Melquiond committed Sep 14, 2010 273 `````` `````` Guillaume Melquiond committed Oct 01, 2010 274 ``````Theorem FTZ_round : `````` Guillaume Melquiond committed Sep 14, 2010 275 276 `````` forall x : R, (bpow (emin + prec - 1) <= Rabs x)%R -> `````` Guillaume Melquiond committed Oct 01, 2010 277 `````` round beta FTZ_exp ZrFTZ x = round beta (FLX_exp prec) rnd x. `````` Guillaume Melquiond committed Sep 14, 2010 278 279 ``````Proof. intros x Hx. `````` Guillaume Melquiond committed Oct 01, 2010 280 ``````unfold round, scaled_mantissa, canonic_exponent. `````` Guillaume Melquiond committed Sep 14, 2010 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 ``````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)). `````` Guillaume Melquiond committed Oct 01, 2010 300 ``````rewrite bpow_plus. `````` Guillaume Melquiond committed Sep 14, 2010 301 302 303 304 305 306 307 308 309 310 311 312 313 314 ``````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. `````` Guillaume Melquiond committed Oct 01, 2010 315 ``````Theorem FTZ_round_small : `````` Guillaume Melquiond committed Sep 14, 2010 316 317 `````` forall x : R, (Rabs x < bpow (emin + prec - 1))%R -> `````` Guillaume Melquiond committed Oct 01, 2010 318 `````` round beta FTZ_exp ZrFTZ x = R0. `````` Guillaume Melquiond committed Sep 14, 2010 319 320 321 322 ``````Proof. intros x Hx. destruct (Req_dec x 0) as [Hx0|Hx0]. rewrite Hx0. `````` Guillaume Melquiond committed Oct 01, 2010 323 324 ``````apply round_0. unfold round, scaled_mantissa, canonic_exponent. `````` Guillaume Melquiond committed Sep 14, 2010 325 326 327 328 329 330 331 332 333 ``````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)). `````` Guillaume Melquiond committed Oct 01, 2010 334 ``````rewrite bpow_plus. `````` Guillaume Melquiond committed Sep 14, 2010 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 ``````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. `````` Guillaume Melquiond committed Oct 01, 2010 352 ``````End FTZ_round. `````` Guillaume Melquiond committed Sep 14, 2010 353 `````` `````` Guillaume Melquiond committed Sep 16, 2009 354 ``End RND_FTZ.``