Fcore_FLT.v 7.76 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(*
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/

Copyright (C) 2010 Sylvie Boldo
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.
*)

19 20 21 22 23 24 25 26
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
27 28 29 30 31

Section RND_FLT.

Variable beta : radix.

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

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

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

42 43 44 45 46 47 48 49 50 51 52
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
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 88 89 90 91 92 93 94 95 96
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).
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 127
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
128 129 130
intros x.
apply iff_sym.
apply FLT_format_generic.
131 132
exact FLT_exp_correct.
Qed.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
133

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

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 203
rewrite ->FLT_canonic_FLX; trivial.
intros H; contradict Hx.
rewrite H, Rabs_R0; apply Rlt_not_le.
apply bpow_gt_0.
Qed.



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 216 217 218 219 220
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.

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 265 266 267 268 269 270 271 272 273 274 275 276
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.

277
Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z.
278 279 280

Theorem NE_ex_prop_FLT :
  NE_ex_prop beta FLT_exp.
281
Proof.
282
destruct NE_prop as [H|H].
283 284 285 286
now left.
right.
intros e.
unfold FLT_exp.
287 288
destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ;
  rewrite H2 ; clear H2.
289 290 291 292 293 294 295 296
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.

297 298
Theorem generic_NE_pt_FLT :
  forall x,
299
  Rnd_NE_pt beta FLT_exp x (round beta FLT_exp rndNE x).
300 301 302 303 304 305 306 307
Proof.
intros x.
apply generic_NE_pt.
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

Theorem Rnd_NE_pt_FLT :
308
  round_pred (Rnd_NE_pt beta FLT_exp).
309
Proof.
310
apply Rnd_NE_pt_round.
311 312 313 314
apply FLT_exp_correct.
apply NE_ex_prop_FLT.
Qed.

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