Fcore_float_prop.v 10.3 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
(** * Basic properties of floating-point formats: lemmas about mantissa, exponent... *)
21 22
Require Import Fcore_Raux.
Require Import Fcore_defs.
23 24 25 26 27

Section Float_prop.

Variable beta : radix.

28
Notation bpow e := (bpow beta e).
29

Guillaume Melquiond's avatar
Guillaume Melquiond committed
30 31 32 33 34 35 36 37 38 39 40
Theorem Rcompare_F2R :
  forall e m1 m2 : Z,
  Rcompare (F2R (Float beta m1 e)) (F2R (Float beta m2 e)) = Zcompare m1 m2.
Proof.
intros e m1 m2.
unfold F2R. simpl.
rewrite Rcompare_mult_r.
apply Rcompare_Z2R.
apply bpow_gt_0.
Qed.

41
(** Basic facts *)
42 43 44 45 46 47 48 49
Theorem F2R_le_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R ->
  (m1 <= m2)%Z.
Proof.
intros e m1 m2 H.
apply le_Z2R.
apply Rmult_le_reg_r with (bpow e).
50
apply bpow_gt_0.
51 52 53 54 55 56 57 58 59 60 61
exact H.
Qed.

Theorem F2R_le_compat :
  forall m1 m2 e : Z,
  (m1 <= m2)%Z ->
  (F2R (Float beta m1 e) <= F2R (Float beta m2 e))%R.
Proof.
intros m1 m2 e H.
unfold F2R. simpl.
apply Rmult_le_compat_r.
62
apply bpow_ge_0.
63 64 65 66 67 68 69
now apply Z2R_le.
Qed.

Theorem F2R_lt_reg :
  forall e m1 m2 : Z,
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R ->
  (m1 < m2)%Z.
70
Proof.
71
intros e m1 m2 H.
72
apply lt_Z2R.
73
apply Rmult_lt_reg_r with (bpow e).
74
apply bpow_gt_0.
75 76 77 78 79 80 81 82 83 84 85
exact H.
Qed.

Theorem F2R_lt_compat :
  forall e m1 m2 : Z,
  (m1 < m2)%Z ->
  (F2R (Float beta m1 e) < F2R (Float beta m2 e))%R.
Proof.
intros e m1 m2 H.
unfold F2R. simpl.
apply Rmult_lt_compat_r.
86
apply bpow_gt_0.
87
now apply Z2R_lt.
88 89
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
90 91 92 93 94 95 96 97 98
Theorem F2R_eq_compat :
  forall e m1 m2 : Z,
  (m1 = m2)%Z ->
  (F2R (Float beta m1 e) = F2R (Float beta m2 e))%R.
Proof.
intros e m1 m2 H.
now apply (f_equal (fun m => F2R (Float beta m e))).
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
99 100 101 102 103 104 105 106 107 108 109 110
Theorem F2R_eq_reg :
  forall e m1 m2 : Z,
  F2R (Float beta m1 e) = F2R (Float beta m2 e) ->
  m1 = m2.
Proof.
intros e m1 m2 H.
apply Zle_antisym ;
  apply F2R_le_reg with e ;
  rewrite H ;
  apply Rle_refl.
Qed.

111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
Theorem abs_F2R :
  forall m e : Z,
  Rabs (F2R (Float beta m e)) = F2R (Float beta (Zabs m) e).
Proof.
intros m e.
unfold F2R.
rewrite Rabs_mult.
rewrite <- Z2R_abs.
simpl.
apply f_equal.
apply Rabs_right.
apply Rle_ge.
apply bpow_ge_0.
Qed.

Theorem opp_F2R :
  forall m e : Z,
  Ropp (F2R (Float beta m e)) = F2R (Float beta (Zopp m) e).
Proof.
intros m e.
unfold F2R. simpl.
rewrite <- Ropp_mult_distr_l_reverse.
now rewrite Z2R_opp.
Qed.

(** Sign facts *)
137 138 139 140 141 142 143 144 145
Theorem F2R_0 :
  forall e : Z,
  F2R (Float beta 0 e) = R0.
Proof.
intros e.
unfold F2R. simpl.
apply Rmult_0_l.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
146 147 148 149 150 151
Theorem F2R_eq_0_reg :
  forall m e : Z,
  F2R (Float beta m e) = R0 ->
  m = Z0.
Proof.
intros m e H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
152 153
apply F2R_eq_reg with e.
now rewrite F2R_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
154 155
Qed.

156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 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 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
Theorem F2R_ge_0_reg :
  forall m e : Z,
  (0 <= F2R (Float beta m e))%R ->
  (0 <= m)%Z.
Proof.
intros m e H.
apply F2R_le_reg with e.
now rewrite F2R_0.
Qed.

Theorem F2R_le_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) <= 0)%R ->
  (m <= 0)%Z.
Proof.
intros m e H.
apply F2R_le_reg with e.
now rewrite F2R_0.
Qed.

Theorem F2R_gt_0_reg :
  forall m e : Z,
  (0 < F2R (Float beta m e))%R ->
  (0 < m)%Z.
Proof.
intros m e H.
apply F2R_lt_reg with e.
now rewrite F2R_0.
Qed.

Theorem F2R_lt_0_reg :
  forall m e : Z,
  (F2R (Float beta m e) < 0)%R ->
  (m < 0)%Z.
Proof.
intros m e H.
apply F2R_lt_reg with e.
now rewrite F2R_0.
Qed.

Theorem F2R_ge_0_compat :
  forall f : float beta,
  (0 <= Fnum f)%Z ->
  (0 <= F2R f)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_le_compat.
Qed.

Theorem F2R_le_0_compat :
  forall f : float beta,
  (Fnum f <= 0)%Z ->
  (F2R f <= 0)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_le_compat.
Qed.

Theorem F2R_gt_0_compat :
  forall f : float beta,
  (0 < Fnum f)%Z ->
  (0 < F2R f)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_lt_compat.
Qed.

Theorem F2R_lt_0_compat :
  forall f : float beta,
  (Fnum f < 0)%Z ->
  (F2R f < 0)%R.
Proof.
intros f H.
rewrite <- F2R_0 with (Fexp f).
now apply F2R_lt_compat.
Qed.

236
(** Floats and bpow *)
237 238 239 240 241 242 243 244 245
Theorem F2R_bpow :
  forall e : Z,
  F2R (Float beta 1 e) = bpow e.
Proof.
intros e.
unfold F2R. simpl.
apply Rmult_1_l.
Qed.

246
Theorem bpow_le_F2R :
247 248 249
  forall m e : Z,
  (0 < m)%Z ->
  (bpow e <= F2R (Float beta m e))%R.
250
Proof.
251
intros m e H.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
252 253
rewrite <- F2R_bpow.
apply F2R_le_compat.
254 255 256
now apply (Zlt_le_succ 0).
Qed.

257
Theorem F2R_p1_le_bpow :
258 259 260 261 262 263 264 265 266
  forall m e1 e2 : Z,
  (0 < m)%Z ->
  (F2R (Float beta m e1) < bpow e2)%R ->
  (F2R (Float beta (m + 1) e1) <= bpow e2)%R.
Proof.
intros m e1 e2 Hm.
intros H.
assert (He : (e1 <= e2)%Z).
(* . *)
267
apply (le_bpow beta).
268 269 270 271
apply Rle_trans with (F2R (Float beta m e1)).
unfold F2R. simpl.
rewrite <- (Rmult_1_l (bpow e1)) at 1.
apply Rmult_le_compat_r.
272
apply bpow_ge_0.
273 274 275 276 277 278
apply (Z2R_le 1).
now apply (Zlt_le_succ 0).
now apply Rlt_le.
(* . *)
revert H.
replace e2 with (e2 - e1 + e1)%Z by ring.
279
rewrite bpow_plus.
280 281 282 283
unfold F2R. simpl.
rewrite <- (Z2R_Zpower beta (e2 - e1)).
intros H.
apply Rmult_le_compat_r.
284
apply bpow_ge_0.
285 286 287 288
apply Rmult_lt_reg_r in H.
apply Z2R_le.
apply Zlt_le_succ.
now apply lt_Z2R.
289
apply bpow_gt_0.
290
now apply Zle_minus_le_0.
291 292
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
293 294 295 296 297 298 299 300 301
Theorem bpow_le_F2R_m1 :
  forall m e1 e2 : Z,
  (1 < m)%Z ->
  (bpow e2 < F2R (Float beta m e1))%R ->
  (bpow e2 <= F2R (Float beta (m - 1) e1))%R.
Proof.
intros m e1 e2 Hm.
case (Zle_or_lt e1 e2); intros He.
replace e2 with (e2 - e1 + e1)%Z by ring.
302
rewrite bpow_plus.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
unfold F2R. simpl.
rewrite <- (Z2R_Zpower beta (e2 - e1)).
intros H.
apply Rmult_le_compat_r.
apply bpow_ge_0.
apply Rmult_lt_reg_r in H.
apply Z2R_le.
rewrite (Zpred_succ (Zpower _ _)).
apply Zplus_le_compat_r.
apply Zlt_le_succ.
now apply lt_Z2R.
apply bpow_gt_0.
now apply Zle_minus_le_0.
intros H.
apply Rle_trans with (1*bpow e1)%R.
rewrite Rmult_1_l.
319
apply bpow_le.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
320 321 322 323 324 325 326 327 328
now apply Zlt_le_weak.
unfold F2R. simpl.
apply Rmult_le_compat_r.
apply bpow_ge_0.
replace 1%R with (Z2R 1) by reflexivity.
apply Z2R_le.
omega.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
329 330
Theorem F2R_lt_bpow :
  forall f : float beta, forall e',
331
  (Zabs (Fnum f) < Zpower beta (e' - Fexp f))%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
332 333 334 335 336 337 338 339
  (Rabs (F2R f) < bpow e')%R.
Proof.
intros (m, e) e' Hm.
rewrite abs_F2R.
destruct (Zle_or_lt e e') as [He|He].
unfold F2R. simpl.
apply Rmult_lt_reg_r with (bpow (-e)).
apply bpow_gt_0.
340
rewrite Rmult_assoc, <- 2!bpow_plus, Zplus_opp_r, Rmult_1_r.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
341 342 343 344 345 346 347 348 349 350 351
rewrite <-Z2R_Zpower. 2: now apply Zle_left.
now apply Z2R_lt.
elim Zlt_not_le with (1 := Hm).
simpl.
cut (e' - e < 0)%Z. 2: omega.
clear.
case (e' - e)%Z ; try easy.
intros p _.
apply Zabs_pos.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
352 353 354
Theorem F2R_change_exp :
  forall e' m e : Z,
  (e' <= e)%Z ->
355
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e')) e').
Guillaume Melquiond's avatar
Guillaume Melquiond committed
356 357 358
Proof.
intros e' m e He.
unfold F2R. simpl.
359
rewrite Z2R_mult, Z2R_Zpower, Rmult_assoc.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
360 361
apply f_equal.
pattern e at 1 ; replace e with (e - e' + e')%Z by ring.
362
apply bpow_plus.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
363 364 365 366
now apply Zle_minus_le_0.
Qed.

Theorem F2R_prec_normalize :
367
  forall m e e' p : Z,
368
  (Zabs m < Zpower beta p)%Z ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
369
  (bpow (e' - 1)%Z <= Rabs (F2R (Float beta m e)))%R ->
370
  F2R (Float beta m e) = F2R (Float beta (m * Zpower beta (e - e' + p)) (e' - p)).
371 372
Proof.
intros m e e' p Hm Hf.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
373 374 375 376 377 378 379
assert (Hp: (0 <= p)%Z).
destruct p ; try easy.
now elim (Zle_not_lt _ _ (Zabs_pos m)).
(* . *)
replace (e - e' + p)%Z with (e - (e' - p))%Z by ring.
apply F2R_change_exp.
cut (e' - 1 < e + p)%Z. omega.
380
apply (lt_bpow beta).
381
apply Rle_lt_trans with (1 := Hf).
382
rewrite abs_F2R, Zplus_comm, bpow_plus.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
383
apply Rmult_lt_compat_r.
384
apply bpow_gt_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
385
rewrite <- Z2R_Zpower.
386
now apply Z2R_lt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
387
exact Hp.
388 389
Qed.

390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413
(** Floats and ln_beta *)
Theorem ln_beta_F2R_bounds :
  forall x m e, (0 < m)%Z ->
  (F2R (Float beta m e) <= x < F2R (Float beta (m + 1) e))%R ->
  ln_beta beta x = ln_beta beta (F2R (Float beta m e)) :> Z.
Proof.
intros x m e Hp (Hx,Hx2).
destruct (ln_beta beta (F2R (Float beta m e))) as (ex, He).
simpl.
apply ln_beta_unique.
assert (Hp1: (0 < F2R (Float beta m e))%R).
now apply F2R_gt_0_compat.
specialize (He (Rgt_not_eq _ _ Hp1)).
rewrite Rabs_pos_eq in He. 2: now apply Rlt_le.
destruct He as (He1, He2).
assert (Hx1: (0 < x)%R).
now apply Rlt_le_trans with (2 := Hx).
rewrite Rabs_pos_eq. 2: now apply Rlt_le.
split.
now apply Rle_trans with (1 := He1).
apply Rlt_le_trans with (1 := Hx2).
now apply F2R_p1_le_bpow.
Qed.

414 415 416
Theorem ln_beta_F2R :
  forall m e : Z,
  m <> Z0 ->
417
  (ln_beta beta (F2R (Float beta m e)) = ln_beta beta (Z2R m) + e :> Z)%Z.
418 419 420 421 422 423 424 425
Proof.
intros m e H.
destruct (ln_beta beta (Z2R m)) as (d, Hd).
simpl.
specialize (Hd (Z2R_neq _ _ H)).
apply ln_beta_unique.
rewrite abs_F2R.
unfold F2R. simpl.
426
rewrite <- Z2R_abs in Hd.
427 428
split.
replace (d + e - 1)%Z with (d - 1 + e)%Z by ring.
429
rewrite bpow_plus.
430
apply Rmult_le_compat_r.
431
apply bpow_ge_0.
432
apply Hd.
433
rewrite bpow_plus.
434
apply Rmult_lt_compat_r.
435
apply bpow_gt_0.
436 437 438 439 440 441 442
apply Hd.
Qed.

Theorem float_distribution_pos :
  forall m1 e1 m2 e2 : Z,
  (0 < m1)%Z ->
  (F2R (Float beta m1 e1) < F2R (Float beta m2 e2) < F2R (Float beta (m1 + 1) e1))%R ->
443
  (e2 < e1)%Z /\ (e1 + ln_beta beta (Z2R m1) = e2 + ln_beta beta (Z2R m2))%Z.
444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475
Proof.
intros m1 e1 m2 e2 Hp1 (H12, H21).
assert (He: (e2 < e1)%Z).
(* . *)
apply Znot_ge_lt.
intros H0.
elim Rlt_not_le with (1 := H21).
apply Zge_le in H0.
apply (F2R_change_exp e1 m2 e2) in H0.
rewrite H0.
apply F2R_le_compat.
apply Zlt_le_succ.
apply (F2R_lt_reg e1).
now rewrite <- H0.
(* . *)
split.
exact He.
rewrite (Zplus_comm e1), (Zplus_comm e2).
assert (Hp2: (0 < m2)%Z).
apply (F2R_gt_0_reg m2 e2).
apply Rlt_trans with (2 := H12).
now apply F2R_gt_0_compat.
rewrite <- 2!ln_beta_F2R.
destruct (ln_beta beta (F2R (Float beta m1 e1))) as (e1', H1).
simpl.
apply sym_eq.
apply ln_beta_unique.
assert (H2 : (bpow (e1' - 1) <= F2R (Float beta m1 e1) < bpow e1')%R).
rewrite <- (Zabs_eq m1), <- abs_F2R.
apply H1.
apply Rgt_not_eq.
apply Rlt_gt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
476
now apply F2R_gt_0_compat.
477 478 479 480 481 482 483 484
now apply Zlt_le_weak.
clear H1.
rewrite abs_F2R, Zabs_eq.
split.
apply Rlt_le.
apply Rle_lt_trans with (2 := H12).
apply H2.
apply Rlt_le_trans with (1 := H21).
485
now apply F2R_p1_le_bpow.
486 487 488 489 490 491 492
now apply Zlt_le_weak.
apply sym_not_eq.
now apply Zlt_not_eq.
apply sym_not_eq.
now apply Zlt_not_eq.
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
493
End Float_prop.