Fcore_FLT.v 6.54 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 22
(* floating-point format with gradual underflow *)
Definition FLT_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Zabs (Fnum f) < Zpower (radix_val 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 87
apply bpow_gt_0.
rewrite <- bpow_add.
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 146 147 148 149 150 151 152 153 154 155 156 157
Qed.

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.

158
Theorem FLT_canonic_FIX :
159 160
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
161
  canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
162 163
Proof.
intros x Hx0 Hx.
164 165 166
unfold canonic_exponent.
apply Zmax_right.
unfold FIX_exp.
167 168 169 170 171 172 173 174
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.

175 176 177 178
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 ).
179
Proof.
180 181 182 183 184
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ;  apply generic_format_0.
destruct Hx as [Hx|Hx].
185
unfold generic_format, scaled_mantissa.
186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203
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.
204 205
Qed.

206 207 208 209 210
Theorem FLT_format_FIX :
  forall x,
  (Rabs x <= bpow (emin + prec))%R ->
  ( FLT_format x <-> FIX_format beta emin x ).
Proof.
211 212 213 214 215
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.
216 217
Qed.

218 219 220 221 222 223 224 225 226 227 228 229 230
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.

231 232 233 234
Hypothesis NE_prop : Zeven (radix_val beta) = false \/ (1 < prec)%Z.

Theorem NE_ex_prop_FLT :
  NE_ex_prop beta FLT_exp.
235
Proof.
236
destruct NE_prop as [H|H].
237 238 239 240
now left.
right.
intros e.
unfold FLT_exp.
241 242
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
243 244 245 246 247 248 249 250
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.

251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268
Theorem generic_NE_pt_FLT :
  forall x,
  Rnd_NE_pt beta FLT_exp x (rounding beta FLT_exp ZrndNE x).
Proof.
intros x.
apply generic_NE_pt.
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

Theorem Rnd_NE_pt_FLT :
  rounding_pred (Rnd_NE_pt beta FLT_exp).
Proof.
apply Rnd_NE_pt_rounding.
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

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