Fcore_FLT.v 7.53 KB
Newer Older
1
(**
2 3 4 5
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010 Sylvie Boldo
6
#<br />#
7 8 9 10 11 12 13 14 15 16 17 18 19
Copyright (C) 2010 Guillaume Melquiond

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

20
(** * Floating-point format with gradual underflow *)
21 22 23 24 25 26 27 28
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
29 30 31 32 33

Section RND_FLT.

Variable beta : radix.

34
Notation bpow e := (bpow beta e).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
35 36 37 38

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

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

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

46
(** Properties of the FLT format *)
47
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
48 49 50 51 52
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
53
split.
54 55 56 57 58
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
intros H0.
apply False_ind.
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
59
split.
60 61
generalize (Zmax_spec (k + 1 - prec) emin).
omega.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
62
split.
63 64 65 66 67 68 69 70
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
71
  forall x : R, FLT_format x <-> generic_format beta FLT_exp x.
72
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
73
split.
74
(* . *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
75 76 77 78 79 80
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
81
rewrite Hx1.
82 83 84 85 86 87
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.
88
apply (lt_bpow beta).
89 90 91 92 93 94 95 96
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).
97
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
98 99 100
intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
101
apply lt_Z2R.
102 103
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
104
apply bpow_gt_0.
105
rewrite <- bpow_plus.
106 107 108 109 110 111 112 113 114 115 116
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).
117
apply bpow_le.
118 119
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
120 121
apply Zle_max_l.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
122 123
Qed.

124 125 126
Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
127
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
128 129 130
intros x.
apply iff_sym.
apply FLT_format_generic.
131
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
132

133
Theorem FLT_canonic_FLX :
134
  forall x, x <> R0 ->
135
  (bpow (emin + prec - 1) <= Rabs x)%R ->
136
  canonic_exponent beta FLT_exp x = canonic_exponent beta (FLX_exp prec) x.
137
Proof.
138 139
intros x Hx0 Hx.
unfold canonic_exponent.
140 141
apply Zmax_left.
destruct (ln_beta beta x) as (ex, He).
142 143 144
unfold FLX_exp. simpl.
specialize (He Hx0).
cut (emin + prec - 1 < ex)%Z. omega.
145
apply (lt_bpow beta).
146 147 148 149
apply Rle_lt_trans with (1 := Hx).
apply He.
Qed.

150
(** Links between FLT and FLX *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
151 152 153 154 155 156
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.
157 158 159
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ;  apply generic_format_0.
160
unfold generic_format, scaled_mantissa.
161
now rewrite (FLT_canonic_FLX x Hx0 Hx).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
162 163
Qed.

164 165 166 167 168 169 170 171 172 173 174 175 176 177

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
178 179 180 181 182 183 184 185 186 187 188 189
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.

190

191
Theorem FLT_round_FLX : forall rnd x,
192
  (bpow (emin + prec - 1) <= Rabs x)%R ->
193
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
194
intros rnd x Hx.
195
unfold round, scaled_mantissa.
196 197 198 199 200 201 202
rewrite ->FLT_canonic_FLX; trivial.
intros H; contradict Hx.
rewrite H, Rabs_R0; apply Rlt_not_le.
apply bpow_gt_0.
Qed.


203
(** Links between FLT and FIX (underflow) *)
204
Theorem FLT_canonic_FIX :
205 206
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
207
  canonic_exponent beta FLT_exp x = canonic_exponent beta (FIX_exp emin) x.
208 209
Proof.
intros x Hx0 Hx.
210 211 212
unfold canonic_exponent.
apply Zmax_right.
unfold FIX_exp.
213 214 215
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
216
apply (lt_bpow beta).
217 218 219 220
apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.

221 222 223 224
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 ).
225
Proof.
226 227 228 229 230
intros x Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
split ; intros _ ;  apply generic_format_0.
destruct Hx as [Hx|Hx].
231
unfold generic_format, scaled_mantissa.
232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249
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.
250 251
Qed.

252 253 254 255 256
Theorem FLT_format_FIX :
  forall x,
  (Rabs x <= bpow (emin + prec))%R ->
  ( FLT_format x <-> FIX_format beta emin x ).
Proof.
257 258 259 260 261
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.
262 263
Qed.

264
(** FLT is a nice format: it has a monotone exponent... *)
265
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
266
Proof.
267 268
intros ex ey.
clear Hp.
269
unfold FLT_exp.
270
generalize (Zmax_spec (ex - prec) emin) (Zmax_spec (ey - prec) emin).
271 272 273
omega.
Qed.

274
(** and it allows a rounding to nearest, ties to even. *)
275
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
276

277
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
278
Proof.
279
destruct NE_prop as [H|H].
280 281 282 283
now left.
right.
intros e.
unfold FLT_exp.
284 285
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
286 287 288 289 290 291 292 293
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.

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