Fcore_FLT.v 7.11 KB
Newer Older
1 2 3 4 5 6 7 8
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.
Require Import Fcore_FIX.
Require Import Fcore_rnd_ne.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
9 10 11 12 13

Section RND_FLT.

Variable beta : radix.

14
Notation bpow e := (bpow beta e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
15 16 17 18

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

19 20 21
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
  exists f : float beta,
22
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
23

24 25 26 27 28 29 30 31 32 33 34
Definition FLT_RoundingModeP (rnd : R -> R):=
  Rounding_for_Format FLT_format rnd.

Definition FLT_exp e := Zmax (e - prec) emin.

Theorem FLT_exp_correct : valid_exp FLT_exp.
Proof.
intros k.
unfold FLT_exp.
destruct (Zmax_spec (k - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
35
split.
36 37 38 39 40
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
intros H0.
apply False_ind.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
41
split.
42 43
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
44
split.
45 46 47 48 49 50 51 52
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
intros l H0.
generalize (Zmax_spec (l - prec) emin).
omega.
Qed.

Theorem FLT_format_generic :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
53
  forall x : R, FLT_format x <-> generic_format beta FLT_exp x.
54
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
55
split.
56
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
57 58 59 60 61 62
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
destruct (ln_beta beta x) as (ex, Hx5).
specialize (Hx5 Hx4).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
63
rewrite Hx1.
64 65 66 67 68 69 70 71 72 73 74 75 76 77 78
apply generic_format_canonic_exponent.
rewrite <- Hx1.
rewrite canonic_exponent_fexp with (1 := Hx5).
unfold FLT_exp.
apply Zmax_lub. 2: exact Hx3.
cut (ex -1 < prec + xe)%Z. omega.
apply <- bpow_lt.
apply Rle_lt_trans with (1 := proj1 Hx5).
rewrite Hx1.
apply F2R_lt_bpow.
simpl.
now ring_simplify (prec + xe - xe)%Z.
(* . *)
unfold generic_format.
set (ex := canonic_exponent beta FLT_exp x).
79
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
80 81 82
intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
83
apply lt_Z2R.
84 85
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
86
apply bpow_gt_0.
87
rewrite <- bpow_plus.
88 89 90 91 92 93 94 95 96 97 98
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
rewrite <- abs_F2R.
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
unfold canonic_exponent in ex.
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
99
apply -> bpow_le.
100 101
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
102 103
apply Zle_max_l.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
104 105
Qed.

106 107 108 109
Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp _)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
110 111 112
intros x.
apply iff_sym.
apply FLT_format_generic.
113 114
exact FLT_exp_correct.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
115

116
Theorem FLT_canonic_FLX :
117
  forall x, x <> R0 ->
118
  (bpow (emin + prec - 1) <= Rabs x)%R ->
119
  canonic_exponent beta FLT_exp x = canonic_exponent beta (FLX_exp prec) x.
120
Proof.
121 122
intros x Hx0 Hx.
unfold canonic_exponent.
123 124
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
125 126 127
unfold FLX_exp. simpl.
specialize (He Hx0).
cut (emin + prec - 1 < ex)%Z. omega.
128 129 130 131 132
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
133 134 135 136 137 138
Theorem FLT_generic_format_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  ( generic_format beta FLT_exp x <-> generic_format beta (FLX_exp prec) x ).
Proof.
intros x Hx.
139 140 141
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ;  apply generic_format_0.
142
unfold generic_format, scaled_mantissa.
143
now rewrite (FLT_canonic_FLX x Hx0 Hx).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
144 145
Qed.

146 147 148 149 150 151 152 153 154 155 156 157 158 159

Theorem FLX_generic_format_FLT :
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.
intros x Hx.
unfold generic_format in Hx; rewrite Hx.
apply generic_format_canonic_exponent.
rewrite <- Hx.
unfold canonic_exponent, FLX_exp, FLT_exp.
apply Zle_max_l.
Qed.


Guillaume Melquiond's avatar
Guillaume Melquiond committed
160 161 162 163 164 165 166 167 168 169 170 171
Theorem FLT_format_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  ( FLT_format x <-> FLX_format beta prec x ).
Proof.
intros x Hx1.
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FLX x Hx1).
apply iff_sym.
now apply FLX_format_generic.
Qed.

172

173
Theorem FLT_round_FLX : forall rnd x,
174
  (bpow (emin + prec - 1) <= Rabs x)%R ->
175
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
176
intros rnd x Hx.
177
unfold round, scaled_mantissa.
178 179 180 181 182 183 184 185
rewrite ->FLT_canonic_FLX; trivial.
intros H; contradict Hx.
rewrite H, Rabs_R0; apply Rlt_not_le.
apply bpow_gt_0.
Qed.



186
Theorem FLT_canonic_FIX :
187 188
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
189
  canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
190 191
Proof.
intros x Hx0 Hx.
192 193 194
unfold canonic_exponent.
apply Zmax_right.
unfold FIX_exp.
195 196 197 198 199 200 201 202
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.

203 204 205 206
Theorem FLT_generic_format_FIX :
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
  ( generic_format beta FLT_exp x <-> generic_format beta (FIX_exp emin) x ).
207
Proof.
208 209 210 211 212
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ;  apply generic_format_0.
destruct Hx as [Hx|Hx].
213
unfold generic_format, scaled_mantissa.
214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231
now rewrite (FLT_canonic_FIX x Hx0 Hx).
(* extra case *)
rewrite <- (Rabs_pos_eq (bpow (emin + prec))) in Hx. 2: apply bpow_ge_0.
assert (H1: generic_format beta FLT_exp (bpow (emin + prec))).
rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FLT_exp.
rewrite F2R_bpow, ln_beta_bpow.
apply Zmax_lub ; omega.
assert (H2: generic_format beta (FIX_exp emin) (bpow (emin + prec))).
rewrite <- F2R_bpow.
apply generic_format_canonic_exponent.
unfold generic_format, canonic_exponent, FIX_exp.
omega.
destruct Rabs_eq_Rabs with (1 := Hx) as [H|H] ;
  rewrite H ; clear H ;
  split ; intros _ ;
  try apply generic_format_opp ; easy.
232 233
Qed.

234 235 236 237 238
Theorem FLT_format_FIX :
  forall x,
  (Rabs x <= bpow (emin + prec))%R ->
  ( FLT_format x <-> FIX_format beta emin x ).
Proof.
239 240 241 242 243
intros x Hx1.
apply iff_trans with (1 := FLT_format_generic x).
apply iff_trans with (1 := FLT_generic_format_FIX x Hx1).
apply iff_sym.
now apply FIX_format_generic.
244 245
Qed.

246 247 248 249 250 251 252 253 254 255 256 257 258
Theorem FLT_not_FTZ :
  not_FTZ_prop FLT_exp.
Proof.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.

259
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
260 261 262

Theorem NE_ex_prop_FLT :
  NE_ex_prop beta FLT_exp.
263
Proof.
264
destruct NE_prop as [H|H].
265 266 267 268
now left.
right.
intros e.
unfold FLT_exp.
269 270
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
271 272 273 274 275 276 277 278
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.

279 280
Theorem generic_NE_pt_FLT :
  forall x,
281
  Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x).
282 283 284 285 286 287 288 289
Proof.
intros x.
apply generic_NE_pt.
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

Theorem Rnd_NE_pt_FLT :
290
  round_pred (Rnd_NE_pt beta FLT_exp).
291
Proof.
292
apply Rnd_NE_pt_round.
293 294 295 296
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
297
End RND_FLT.