Fcore_FLX.v 5.81 KB
Newer Older
1 2 3 4 5 6 7
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_FIX.
Require Import Fcore_rnd_ne.
8

9
Section RND_FLX.
10 11 12

Variable beta : radix.

13
Notation bpow e := (bpow beta e).
14 15 16 17

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

18 19 20
(* unbounded floating-point format *)
Definition FLX_format (x : R) :=
  exists f : float beta,
21
  x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z.
22 23 24 25

Definition FLX_RoundingModeP (rnd : R -> R):=
  Rounding_for_Format FLX_format rnd.

26 27 28 29 30 31 32 33 34
Definition FLX_exp (e : Z) := (e - prec)%Z.

Theorem FLX_exp_correct : valid_exp FLX_exp.
Proof.
intros k.
unfold FLX_exp.
repeat split ; intros ; omega.
Qed.

35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55
Theorem FLX_format_FIX :
  forall x e,
  (bpow (e - 1) <= Rabs x <= bpow e)%R ->
  ( FLX_format x <-> FIX_format beta (e - prec) x ).
Proof.
intros x e Hx.
split.
(* . *)
intros ((xm, xe), (H1, H2)).
rewrite H1, (F2R_prec_normalize beta xm xe e prec).
now eexists.
exact H2.
now rewrite <- H1.
(* . *)
destruct Hx as (Hx1,[Hx2|Hx2]).
(* . . *)
intros ((xm, xe), (H1, H2)).
rewrite H1.
eexists ; repeat split.
apply lt_Z2R.
apply Rmult_lt_reg_r with (bpow (e - prec)).
56 57
apply bpow_gt_0.
rewrite Z2R_Zpower, <- bpow_add.
58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
ring_simplify (prec + (e - prec))%Z.
rewrite <- H2.
simpl.
change (F2R (Float beta (Zabs xm) xe) < bpow e)%R.
now rewrite <- abs_F2R, <- H1.
now apply Zlt_le_weak.
(* . . *)
intros ((xm, xe), (H1, H2)).
assert (Ha: forall x, FLX_format (Rabs x) -> FLX_format x).
clear.
intros x Ha.
unfold Rabs in Ha.
destruct (Rcase_abs x) as [Hx|Hx].
destruct Ha as ((m,e),(Ha,Hb)).
exists (Float beta (-m) e).
split.
now rewrite <- opp_F2R, <- Ha, Ropp_involutive.
simpl.
now rewrite Zabs_Zopp.
exact Ha.
(* . . *)
apply Ha.
rewrite Hx2.
exists (Float beta 1 e).
split.
apply sym_eq.
apply Rmult_1_l.
now apply Zpower_gt_1.
Qed.

88
Theorem FLX_format_generic :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
89
  forall x : R, FLX_format x <-> generic_format beta FLX_exp x.
90
Proof.
91 92
intros x.
destruct (Req_dec x 0) as [Hx|Hx1].
93
(* . *)
94
split ; intros H ; rewrite Hx.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
95
apply generic_format_0.
96 97
exists (Float beta 0 0).
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
98
now rewrite F2R_0.
99
now apply Zpower_gt_0.
100
(* . *)
101
destruct (ln_beta beta x) as (ex, Hx2).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
102
simpl.
103
specialize (Hx2 Hx1).
104
apply iff_trans with (generic_format beta (FIX_exp (ex - prec)) x).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
105 106 107 108
apply iff_trans with (FIX_format beta (ex - prec) x).
apply FLX_format_FIX.
exact (conj (proj1 Hx2) (Rlt_le _ _ (proj2 Hx2))).
apply FIX_format_generic.
109
assert (Hf: FLX_exp (ln_beta beta x) = FIX_exp (ex - prec) (ln_beta beta x)).
110 111
unfold FIX_exp, FLX_exp.
now rewrite ln_beta_unique with (1 := Hx2).
112
split ;
113
  unfold generic_format, scaled_mantissa, canonic_exponent ;
114
  now rewrite Hf.
115 116 117 118 119
Qed.

Theorem FLX_format_satisfies_any :
  satisfies_any FLX_format.
Proof.
Guillaume Melquiond's avatar
Typo.  
Guillaume Melquiond committed
120
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
121 122 123
intros x.
apply iff_sym.
apply FLX_format_generic.
124
exact FLX_exp_correct.
125 126
Qed.

127 128 129
(* unbounded floating-point format with normal mantissas *)
Definition FLXN_format (x : R) :=
  exists f : float beta,
Guillaume Melquiond's avatar
Guillaume Melquiond committed
130
  x = F2R f /\ (x <> R0 ->
131
  Zpower beta (prec - 1) <= Zabs (Fnum f) < Zpower beta prec)%Z.
132 133 134 135 136 137 138 139 140 141 142 143 144 145 146

Definition FLXN_RoundingModeP (rnd : R -> R):=
  Rounding_for_Format FLXN_format rnd.

Theorem FLX_format_FLXN :
  forall x : R, FLX_format x <-> FLXN_format x.
Proof.
intros x.
split.
(* . *)
intros ((xm, xe), (H1, H2)).
destruct (Z_eq_dec xm 0) as [H3|H3].
exists (Float beta 0 0).
split.
rewrite H1, H3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
147
now rewrite 2!F2R_0.
148
intros H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
149 150
elim H.
rewrite H1, H3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151
apply F2R_0.
152 153
destruct (ln_beta beta (Z2R xm)) as (d,H4).
specialize (H4 (Z2R_neq _ _ H3)).
154 155
assert (H5: (0 <= prec - d)%Z).
cut (d - 1 < prec)%Z. omega.
156
apply <- (bpow_lt beta).
157
apply Rle_lt_trans with (Rabs (Z2R xm)).
158
apply H4.
159
rewrite <- Z2R_Zpower, <- abs_Z2R.
160 161
now apply Z2R_lt.
now apply Zlt_le_weak.
162
exists (Float beta (xm * Zpower beta (prec - d)) (xe + d - prec)).
163 164 165
split.
unfold F2R. simpl.
rewrite mult_Z2R, Z2R_Zpower.
166
rewrite Rmult_assoc, <- bpow_add.
167 168 169 170 171 172 173
rewrite H1.
now ring_simplify (prec - d + (xe + d - prec))%Z.
exact H5.
intros _. simpl.
split.
apply le_Z2R.
apply Rmult_le_reg_r with (bpow (d - prec)).
174 175 176 177
apply bpow_gt_0.
rewrite abs_Z2R, mult_Z2R, Rabs_mult, 2!Z2R_Zpower.
rewrite <- bpow_add.
rewrite <- abs_Z2R.
178
rewrite Rabs_pos_eq.
179
rewrite Rmult_assoc, <- bpow_add.
180 181
ring_simplify (prec - 1 + (d - prec))%Z.
ring_simplify (prec - d + (d - prec))%Z.
182 183
now rewrite Rmult_1_r, abs_Z2R.
apply bpow_ge_0.
184 185 186
exact H5.
omega.
apply lt_Z2R.
187
rewrite abs_Z2R, mult_Z2R, Rabs_mult.
188
rewrite 2!Z2R_Zpower.
189
rewrite <- abs_Z2R, Rabs_pos_eq.
190
apply Rmult_lt_reg_r with (bpow (d - prec)).
191 192
apply bpow_gt_0.
rewrite Rmult_assoc, <- 2!bpow_add.
193 194
ring_simplify (prec + (d - prec))%Z.
ring_simplify (prec - d + (d - prec))%Z.
195 196
now rewrite Rmult_1_r, abs_Z2R.
apply bpow_ge_0.
197 198 199 200
now apply Zlt_le_weak.
exact H5.
(* . *)
intros ((xm, xe), (H1, H2)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
201 202
destruct (Req_dec x 0) as [H3|H3].
rewrite H3.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
203
apply <- FLX_format_generic.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
204
apply generic_format_0.
205 206 207 208 209 210 211 212 213 214 215 216
specialize (H2 H3). clear H3.
rewrite H1.
eexists ; repeat split.
apply H2.
Qed.

Theorem FLXN_format_satisfies_any :
  satisfies_any FLXN_format.
Proof.
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLX_exp _)).
split ; intros H.
apply -> FLX_format_FLXN.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
217 218
now apply <- FLX_format_generic.
apply -> FLX_format_generic.
219 220 221 222
now apply <- FLX_format_FLXN.
exact FLX_exp_correct.
Qed.

223 224 225 226 227 228 229 230
Theorem FLX_not_FTZ :
  not_FTZ_prop FLX_exp.
Proof.
intros e.
unfold FLX_exp.
omega.
Qed.

231
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252

Theorem NE_ex_prop_FLX :
  NE_ex_prop beta FLX_exp.
Proof.
destruct NE_prop as [H|H].
now left.
right.
unfold FLX_exp.
split ; omega.
Qed.

Theorem generic_NE_pt_FLX :
  forall x,
  Rnd_NE_pt beta FLX_exp x (rounding beta FLX_exp ZrndNE x).
Proof.
intros x.
apply generic_NE_pt.
apply FLX_exp_correct.
apply NE_ex_prop_FLX.
Qed.

253 254 255 256 257
Theorem Rnd_NE_pt_FLX :
  rounding_pred (Rnd_NE_pt beta FLX_exp).
Proof.
apply Rnd_NE_pt_rounding.
apply FLX_exp_correct.
258
apply NE_ex_prop_FLX.
259 260
Qed.

261
End RND_FLX.