Fcore_FLT.v 6.22 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 63 64 65 66 67 68 69 70 71 72 73 74
intros ((xm, xe), (Hx1, (Hx2, Hx3))).
destruct (Req_dec x 0) as [Hx4|Hx4].
rewrite Hx4.
apply generic_format_0.
simpl in Hx2, Hx3.
unfold generic_format, canonic, FLT_exp.
destruct (ln_beta beta x) as (ex, Hx5).
simpl.
specialize (Hx5 Hx4).
destruct (Zmax_spec (ex - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
rewrite Hx1, (F2R_prec_normalize beta xm xe ex prec Hx2).
now eexists.
now rewrite <- Hx1.
rewrite Hx1, (F2R_change_exp beta emin).
now eexists.
exact Hx3.
(* . *)
75 76 77 78 79 80
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.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
81 82
simpl.
split.
83 84
apply Zpower_gt_0.
now apply Zlt_le_trans with (2 := radix_prop beta).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
85
now apply Zlt_le_weak.
86
apply Zle_refl.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
87 88
rewrite Hx1.
eexists ; repeat split.
89
destruct (ln_beta beta x) as (ex, Hx4).
90
simpl in Hx2.
91
specialize (Hx4 Hx3).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
92
apply lt_Z2R.
93
rewrite Z2R_Zpower.
94
apply Rmult_lt_reg_r with (bpow (ex - prec)).
95 96
apply bpow_gt_0.
rewrite <- bpow_add.
97 98 99 100 101 102
replace (prec + (ex - prec))%Z with ex by ring.
apply Rle_lt_trans with (Z2R (Zabs xm) * bpow xe)%R.
rewrite Hx2.
apply Rmult_le_compat_l.
apply (Z2R_le 0).
apply Zabs_pos.
103
apply -> bpow_le.
104 105 106 107 108 109 110 111
apply Zle_max_l.
replace (Z2R (Zabs xm) * bpow xe)%R with (Rabs x).
exact (proj2 Hx4).
rewrite Hx1.
apply abs_F2R.
now apply Zlt_le_weak.
rewrite Hx2.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
112 113
Qed.

114 115 116 117
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
118 119 120
intros x.
apply iff_sym.
apply FLT_format_generic.
121 122
exact FLT_exp_correct.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
123

124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
Theorem FLT_canonic_FLX :
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
  forall f : float beta,
  ( canonic beta FLT_exp x f <-> canonic beta (FLX_exp prec) x f ).
Proof.
intros x Hx f.
unfold canonic.
replace (FLT_exp (projT1 (ln_beta beta x))) with (FLX_exp prec (projT1 (ln_beta beta x))).
apply iff_refl.
unfold FLX_exp, FLT_exp.
apply sym_eq.
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
simpl.
assert (emin + prec - 1 < ex)%Z. 2: omega.
apply <- (bpow_lt beta).
apply Rle_lt_trans with (1 := Hx).
apply He.
intros H.
elim Rlt_not_le with (2 := Hx).
rewrite H, Rabs_R0.
apply bpow_gt_0.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173
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.
assert (Hc := FLT_canonic_FLX x Hx).
split ; intros (f, Hf) ; exists f.
now apply -> Hc.
now apply <- Hc.
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.
assert (Hc := FLT_canonic_FLX 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.

174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
Theorem FLT_exp_FIX :
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
  FLT_exp (projT1 (ln_beta beta x)) = FIX_exp emin (projT1 (ln_beta beta x)).
Proof.
intros x Hx0 Hx.
unfold FIX_exp, FLT_exp.
rewrite Zmax_right.
apply refl_equal.
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.

Theorem FLT_canonic_FIX :
  forall x : R, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
  forall f : float beta,
  ( canonic beta FLT_exp x f <-> canonic beta (FIX_exp emin) x f ).
Proof.
intros x Hx0 Hx f.
unfold canonic.
now rewrite FLT_exp_FIX.
Qed.

202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222
Theorem FLT_format_FIX :
  forall x,
  (Rabs x <= bpow (emin + prec))%R ->
  ( FLT_format x <-> FIX_format beta emin x ).
Proof.
intros x Hx.
split.
(* . *)
intros ((xm, xe), (H1, (H2, H3))).
rewrite H1, (F2R_change_exp beta emin).
now eexists.
exact H3.
(* . *)
destruct Hx as [Hx|Hx].
(* . . *)
intros ((xm, xe), (H1, H2)).
rewrite H1.
eexists ; repeat split.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply Rmult_lt_reg_r with (bpow xe).
223
apply bpow_gt_0.
224 225
rewrite H1, abs_F2R in Hx.
apply Rlt_le_trans with (1 := Hx).
226 227
rewrite <- bpow_add.
apply -> bpow_le.
228 229 230 231 232 233 234 235 236 237
rewrite Zplus_comm, <- H2.
apply Zle_refl.
now apply Zlt_le_weak.
now apply Zeq_le.
(* . . *)
assert (Ha: forall x, FLT_format (Rabs x) -> FLT_format x).
clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
Guillaume Melquiond's avatar
Guillaume Melquiond committed
238
apply <- FLT_format_generic.
239 240
rewrite <- (Ropp_involutive x).
apply generic_format_sym.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
241
now apply -> FLT_format_generic.
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256
exact Ha.
(* . . *)
intros _.
apply Ha.
rewrite Hx.
exists (Float beta 1 (emin + prec)).
split.
apply sym_eq.
apply Rmult_1_l.
simpl.
split.
now apply Zpower_gt_1.
omega.
Qed.

257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
Theorem Rnd_NE_pt_FLT :
  Zodd (radix_val beta) \/ (1 < prec)%Z ->
  rounding_pred (Rnd_NE_pt beta FLT_exp).
Proof.
intros H.
apply Rnd_NE_pt_rounding.
apply FLT_exp_correct.
destruct H.
now left.
right.
intros e.
unfold FLT_exp.
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)].
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (e - prec + 1 - prec) emin).
omega.
rewrite H2.
generalize (Zmax_spec (e + 1 - prec) emin).
generalize (Zmax_spec (emin + 1 - prec) emin).
omega.
Qed.

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