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

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

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

Variable emin prec : Z.
37 38

Context { prec_gt_0_ : Prec_gt_0 prec }.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
39

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

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

47
(** Properties of the FLT format *)
48
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
49 50 51
Proof.
intros k.
unfold FLT_exp.
52 53 54
generalize (prec_gt_0 prec).
repeat split ;
  intros ; zify ; omega.
55 56
Qed.

57 58
Theorem generic_format_FLT :
  forall x, FLT_format x -> generic_format beta FLT_exp x.
59
Proof.
60
clear prec_gt_0_.
61 62 63
intros x ((mx, ex), (H1, (H2, H3))).
simpl in H2, H3.
rewrite H1.
64 65
apply generic_format_F2R.
intros Zmx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
66
unfold canonic_exp, FLT_exp.
67 68 69 70
rewrite ln_beta_F2R with (1 := Zmx).
apply Zmax_lub with (2 := H3).
apply Zplus_le_reg_r with (prec - ex)%Z.
ring_simplify.
71
now apply ln_beta_le_Zpower.
72 73 74 75 76 77
Qed.

Theorem FLT_format_generic :
  forall x, generic_format beta FLT_exp x -> FLT_format x.
Proof.
intros x.
78
unfold generic_format.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
79
set (ex := canonic_exp beta FLT_exp x).
80
set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)).
81 82 83
intros Hx.
rewrite Hx.
eexists ; repeat split ; simpl.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
84
apply lt_Z2R.
85 86
rewrite Z2R_Zpower. 2: now apply Zlt_le_weak.
apply Rmult_lt_reg_r with (bpow ex).
87
apply bpow_gt_0.
88
rewrite <- bpow_plus.
89
change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
90
rewrite F2R_Zabs.
91 92 93 94
rewrite <- Hx.
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0, Rabs_R0.
apply bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
95
unfold canonic_exp in ex.
96 97 98 99
destruct (ln_beta beta x) as (ex', He).
simpl in ex.
specialize (He Hx0).
apply Rlt_le_trans with (1 := proj2 He).
100
apply bpow_le.
101 102
cut (ex' - prec <= ex)%Z. omega.
unfold ex, FLT_exp.
103 104
apply Zle_max_l.
apply Zle_max_r.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
105 106
Qed.

107 108 109 110 111 112 113 114 115 116 117 118 119

Theorem FLT_format_bpow :
  forall e, (emin <= e)%Z -> generic_format beta FLT_exp (bpow e).
Proof.
intros e He.
apply generic_format_bpow; unfold FLT_exp.
apply Z.max_case; try assumption.
unfold Prec_gt_0 in prec_gt_0_; omega.
Qed.




120 121 122
Theorem FLT_format_satisfies_any :
  satisfies_any FLT_format.
Proof.
123
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
124
intros x.
125
split.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
126
apply FLT_format_generic.
127
apply generic_format_FLT.
128
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
129

130
Theorem canonic_exp_FLT_FLX :
Sylvie Boldo's avatar
Sylvie Boldo committed
131
  forall x,
132
  (bpow (emin + prec - 1) <= Rabs x)%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133
  canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x.
134
Proof.
Sylvie Boldo's avatar
Sylvie Boldo committed
135 136 137 138
intros x Hx.
assert (Hx0: x <> 0%R).
intros H1; rewrite H1, Rabs_R0 in Hx.
contradict Hx; apply Rlt_not_le, bpow_gt_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
139
unfold canonic_exp.
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 *)
151
Theorem generic_format_FLT_FLX :
Guillaume Melquiond's avatar
Guillaume Melquiond committed
152 153
  forall x : R,
  (bpow (emin + prec - 1) <= Rabs x)%R ->
154 155
  generic_format beta (FLX_exp prec) x ->
  generic_format beta FLT_exp x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
156
Proof.
157
intros x Hx H.
158 159
destruct (Req_dec x 0) as [Hx0|Hx0].
rewrite Hx0.
160
apply generic_format_0.
161
unfold generic_format, scaled_mantissa.
162
now rewrite canonic_exp_FLT_FLX.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
163 164
Qed.

165
Theorem generic_format_FLX_FLT :
166 167 168
  forall x : R,
  generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x.
Proof.
169
clear prec_gt_0_.
170 171
intros x Hx.
unfold generic_format in Hx; rewrite Hx.
172 173
apply generic_format_F2R.
intros _.
174
rewrite <- Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
175
unfold canonic_exp, FLX_exp, FLT_exp.
176 177 178
apply Zle_max_l.
Qed.

179
Theorem round_FLT_FLX : forall rnd x,
180
  (bpow (emin + prec - 1) <= Rabs x)%R ->
181
  round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
182
intros rnd x Hx.
183
unfold round, scaled_mantissa.
184
rewrite canonic_exp_FLT_FLX ; trivial.
185 186
Qed.

187
(** Links between FLT and FIX (underflow) *)
188
Theorem canonic_exp_FLT_FIX :
189 190
  forall x, x <> R0 ->
  (Rabs x < bpow (emin + prec))%R ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
191
  canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x.
192 193
Proof.
intros x Hx0 Hx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
194
unfold canonic_exp.
195 196
apply Zmax_right.
unfold FIX_exp.
197 198 199
destruct (ln_beta beta x) as (ex, Hex).
simpl.
cut (ex - 1 < emin + prec)%Z. omega.
200
apply (lt_bpow beta).
201 202 203 204
apply Rle_lt_trans with (2 := Hx).
now apply Hex.
Qed.

205
Theorem generic_format_FIX_FLT :
206 207 208 209
  forall x : R,
  generic_format beta FLT_exp x ->
  generic_format beta (FIX_exp emin) x.
Proof.
210
clear prec_gt_0_.
211 212
intros x Hx.
rewrite Hx.
213 214
apply generic_format_F2R.
intros _.
215 216 217 218
rewrite <- Hx.
apply Zle_max_r.
Qed.

219
Theorem generic_format_FLT_FIX :
220 221
  forall x : R,
  (Rabs x <= bpow (emin + prec))%R ->
222 223
  generic_format beta (FIX_exp emin) x ->
  generic_format beta FLT_exp x.
224 225 226
Proof with auto with typeclass_instances.
apply generic_inclusion_le...
intros e He.
227
unfold FIX_exp.
228 229 230
apply Zmax_lub.
omega.
apply Zle_refl.
231 232
Qed.

233
(** FLT is a nice format: it has a monotone exponent... *)
234
Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.
235
Proof.
236
intros ex ey.
237
unfold FLT_exp.
238
zify ; omega.
239 240
Qed.

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

244
Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.
245
Proof.
246
destruct NE_prop as [H|H].
247 248 249 250
now left.
right.
intros e.
unfold FLT_exp.
251 252
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
253 254 255 256 257 258 259 260
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
261
End RND_FLT.