Fappli_IEEE.v 44.1 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/

BOLDO Sylvie's avatar
BOLDO Sylvie committed
5
Copyright (C) 2010-2011 Sylvie Boldo
6
#<br />#
BOLDO Sylvie's avatar
BOLDO Sylvie committed
7
Copyright (C) 2010-2011 Guillaume Melquiond
8 9 10 11 12 13 14 15 16 17 18 19 20

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.
*)

(** * IEEE-754 arithmetic *)
21
Require Import Fcore.
22
Require Import Fcore_digits.
23
Require Import Fcalc_digits.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
24 25 26
Require Import Fcalc_round.
Require Import Fcalc_bracket.
Require Import Fcalc_ops.
27
Require Import Fcalc_div.
28
Require Import Fcalc_sqrt.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
29
Require Import Fprop_relative.
30

31 32 33 34 35 36 37 38
Section AnyRadix.

Inductive full_float :=
  | F754_zero : bool -> full_float
  | F754_infinity : bool -> full_float
  | F754_nan : full_float
  | F754_finite : bool -> positive -> Z -> full_float.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
39
Definition FF2R beta x :=
40
  match x with
BOLDO Sylvie's avatar
BOLDO Sylvie committed
41
  | F754_finite s m e => F2R (Float beta (cond_Zopp s (Zpos m)) e)
42 43 44 45 46
  | _ => R0
  end.

End AnyRadix.

47 48
Section Binary.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
49 50 51
(** prec is the number of bits of the mantissa including the implicit one
    emax is the exponent of the infinities
    Typically p=24 and emax = 128 in single precision *)
52
Variable prec emax : Z.
53
Context (prec_gt_0_ : Prec_gt_0 prec).
54
Hypothesis Hmax : (prec < emax)%Z.
55

56
Let emin := (3 - emax - prec)%Z.
57
Let fexp := FLT_exp emin prec.
58
Instance fexp_correct : Valid_exp fexp := FLT_exp_valid emin prec.
59
Instance fexp_monotone : Monotone_exp fexp := FLT_exp_monotone emin prec.
60

BOLDO Sylvie's avatar
BOLDO Sylvie committed
61
Definition canonic_mantissa m e :=
62 63 64
  Zeq_bool (fexp (Z_of_nat (S (digits2_Pnat m)) + e)) e.

Definition bounded m e :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
65
  andb (canonic_mantissa m e) (Zle_bool e (emax - prec)).
66

67 68 69 70 71 72
Definition valid_binary x :=
  match x with
  | F754_finite _ m e => bounded m e
  | _ => true
  end.

73
(** Basic type used for representing binary FP numbers.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
74 75
    Note that there is exactly one such object per FP datum.
    NaNs do not have any payload. They cannot be distinguished. *)
76 77 78 79 80 81 82
Inductive binary_float :=
  | B754_zero : bool -> binary_float
  | B754_infinity : bool -> binary_float
  | B754_nan : binary_float
  | B754_finite : bool ->
    forall (m : positive) (e : Z), bounded m e = true -> binary_float.

83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
Definition FF2B x :=
  match x as x return valid_binary x = true -> binary_float with
  | F754_finite s m e => B754_finite s m e
  | F754_infinity s => fun _ => B754_infinity s
  | F754_zero s => fun _ => B754_zero s
  | F754_nan => fun _ => B754_nan
  end.

Definition B2FF x :=
  match x with
  | B754_finite s m e _ => F754_finite s m e
  | B754_infinity s => F754_infinity s
  | B754_zero s => F754_zero s
  | B754_nan => F754_nan
  end.

99 100 101 102
Definition radix2 := Build_radix 2 (refl_equal true).

Definition B2R f :=
  match f with
Guillaume Melquiond's avatar
Guillaume Melquiond committed
103
  | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
104 105 106
  | _ => R0
  end.

107 108 109 110 111 112 113 114 115 116 117 118 119 120
Theorem FF2R_B2FF :
  forall x,
  FF2R radix2 (B2FF x) = B2R x.
Proof.
now intros [sx|sx| |sx mx ex Hx].
Qed.

Theorem B2FF_FF2B :
  forall x Hx,
  B2FF (FF2B x Hx) = x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
Qed.

121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
Theorem valid_binary_B2FF :
  forall x,
  valid_binary (B2FF x) = true.
Proof.
now intros [sx|sx| |sx mx ex Hx].
Qed.

Theorem FF2B_B2FF :
  forall x H,
  FF2B (B2FF x) H = x.
Proof.
intros [sx|sx| |sx mx ex Hx] H ; try easy.
apply f_equal.
apply eqbool_irrelevance.
Qed.

Theorem FF2B_B2FF_valid :
  forall x,
  FF2B (B2FF x) (valid_binary_B2FF x) = x.
Proof.
intros x.
apply FF2B_B2FF.
Qed.

145 146 147 148 149 150 151
Theorem B2R_FF2B :
  forall x Hx,
  B2R (FF2B x Hx) = FF2R radix2 x.
Proof.
now intros [sx|sx| |sx mx ex] Hx.
Qed.

152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169
Theorem match_FF2B :
  forall {T} fz fi fn ff x Hx,
  match FF2B x Hx return T with
  | B754_zero sx => fz sx
  | B754_infinity sx => fi sx
  | B754_nan => fn
  | B754_finite sx mx ex _ => ff sx mx ex
  end =
  match x with
  | F754_zero sx => fz sx
  | F754_infinity sx => fi sx
  | F754_nan => fn
  | F754_finite sx mx ex => ff sx mx ex
  end.
Proof.
now intros T fz fi fn ff [sx|sx| |sx mx ex] Hx.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
170
Theorem canonic_canonic_mantissa :
171
  forall (sx : bool) mx ex,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
172
  canonic_mantissa mx ex = true ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
173
  canonic radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
174 175 176 177 178 179 180
Proof.
intros sx mx ex H.
assert (Hx := Zeq_bool_eq _ _ H). clear H.
apply sym_eq.
simpl.
pattern ex at 2 ; rewrite <- Hx.
apply (f_equal fexp).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
181 182
rewrite ln_beta_F2R_Zdigits.
rewrite <- Zdigits_abs.
183 184 185 186 187 188 189 190 191 192 193 194
rewrite Z_of_nat_S_digits2_Pnat.
now case sx.
now case sx.
Qed.

Theorem generic_format_B2R :
  forall x,
  generic_format radix2 fexp (B2R x).
Proof.
intros [sx|sx| |sx mx ex Hx] ; try apply generic_format_0.
simpl.
apply generic_format_canonic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
195
apply canonic_canonic_mantissa.
196 197 198
now destruct (andb_prop _ _ Hx) as (H, _).
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
199
Theorem B2FF_inj :
200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221
  forall x y : binary_float,
  B2FF x = B2FF y ->
  x = y.
Proof.
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
(* *)
intros H.
now inversion H.
(* *)
intros H.
now inversion H.
(* *)
intros H.
inversion H.
clear H.
revert Hx.
rewrite H2, H3.
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
Qed.

222 223 224 225 226 227
Definition is_finite_strict f :=
  match f with
  | B754_finite _ _ _ _ => true
  | _ => false
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
228
Theorem B2R_inj:
229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255
  forall x y : binary_float,
  is_finite_strict x = true ->
  is_finite_strict y = true ->
  B2R x = B2R y ->
  x = y.
Proof.
intros [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
simpl.
intros _ _ Heq.
assert (Hs: sx = sy).
(* *)
revert Heq. clear.
case sx ; case sy ; try easy ;
  intros Heq ; apply False_ind ; revert Heq.
apply Rlt_not_eq.
apply Rlt_trans with R0.
now apply F2R_lt_0_compat.
now apply F2R_gt_0_compat.
apply Rgt_not_eq.
apply Rgt_trans with R0.
now apply F2R_gt_0_compat.
now apply F2R_lt_0_compat.
assert (mx = my /\ ex = ey).
(* *)
refine (_ (canonic_unicity _ fexp _ _ _ _ Heq)).
rewrite Hs.
now case sy ; intro H ; injection H ; split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
256
apply canonic_canonic_mantissa.
257
exact (proj1 (andb_prop _ _ Hx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
258
apply canonic_canonic_mantissa.
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
exact (proj1 (andb_prop _ _ Hy)).
(* *)
revert Hx.
rewrite Hs, (proj1 H), (proj2 H).
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
Qed.

Definition is_finite f :=
  match f with
  | B754_finite _ _ _ _ => true
  | B754_zero _ => true
  | _ => false
  end.

275 276 277 278 279 280 281 282 283 284 285 286 287 288
Definition is_finite_FF f :=
  match f with
  | F754_finite _ _ _ => true
  | F754_zero _ => true
  | _ => false
  end.

Theorem is_finite_FF2B :
  forall x Hx,
  is_finite (FF2B x Hx) = is_finite_FF x.
Proof.
now intros [| | |].
Qed.

289 290 291 292 293 294 295
Theorem is_finite_FF_B2FF :
  forall x,
  is_finite_FF (B2FF x) = is_finite x.
Proof.
now intros [| | |].
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315
Definition Bopp x :=
  match x with
  | B754_nan => x
  | B754_infinity sx => B754_infinity (negb sx)
  | B754_finite sx mx ex Hx => B754_finite (negb sx) mx ex Hx
  | B754_zero sx => B754_zero (negb sx)
  end.

Theorem Bopp_involutive :
  forall x, Bopp (Bopp x) = x.
Proof.
now intros [sx|sx| |sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
Qed.

Theorem B2R_Bopp :
  forall x,
  B2R (Bopp x) = (- B2R x)%R.
Proof.
intros [sx|sx| |sx mx ex Hx] ; apply sym_eq ; try apply Ropp_0.
simpl.
316
rewrite <- F2R_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
317 318 319
now case sx.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
320 321 322 323 324 325 326 327 328

Theorem is_finite_Bopp: forall x,
  is_finite (Bopp x) = is_finite x.
Proof.
now intros [| | |].
Qed.



329 330 331
Theorem bounded_lt_emax :
  forall mx ex,
  bounded mx ex = true ->
332
  (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R.
333
Proof.
334
intros mx ex Hx.
335 336 337
destruct (andb_prop _ _ Hx) as (H1,H2).
generalize (Zeq_bool_eq _ _ H1). clear H1. intro H1.
generalize (Zle_bool_imp_le _ _ H2). clear H2. intro H2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
338
generalize (ln_beta_F2R_Zdigits radix2 (Zpos mx) ex).
339 340 341 342
destruct (ln_beta radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex).
unfold ln_beta_val.
intros H.
apply Rlt_le_trans with (bpow radix2 e').
343
change (Zpos mx) with (Zabs (Zpos mx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
344
rewrite F2R_Zabs.
345 346 347 348 349 350 351 352 353
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
apply bpow_le.
rewrite H. 2: discriminate.
revert H1. clear -H2.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
unfold fexp, FLT_exp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
354
generalize (Zdigits radix2 (Zpos mx)).
355 356
intros ; zify ; subst.
clear -H H2. clearbody emin.
357 358 359
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
360
Theorem abs_B2R_lt_emax :
361
  forall x,
362
  (Rabs (B2R x) < bpow radix2 emax)%R.
363 364
Proof.
intros [sx|sx| |sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
365
rewrite <- F2R_Zabs, abs_cond_Zopp.
366 367 368
now apply bounded_lt_emax.
Qed.

369 370 371
Theorem bounded_canonic_lt_emax :
  forall mx ex,
  canonic radix2 fexp (Float radix2 (Zpos mx) ex) ->
372
  (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R ->
373 374
  bounded mx ex = true.
Proof.
375
intros mx ex Cx Bx.
376 377
apply andb_true_intro.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
378
unfold canonic_mantissa.
379 380 381 382
unfold canonic, Fexp in Cx.
rewrite Cx at 2.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
383 384
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
385 386 387 388
now apply -> Zeq_is_eq_bool.
apply Zle_bool_true.
unfold canonic, Fexp in Cx.
rewrite Cx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
389
unfold canonic_exp, fexp, FLT_exp.
390
destruct (ln_beta radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl.
391 392
apply Zmax_lub.
cut (e' - 1 < emax)%Z. clear ; omega.
393 394 395
apply lt_bpow with radix2.
apply Rle_lt_trans with (2 := Bx).
change (Zpos mx) with (Zabs (Zpos mx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
396
rewrite F2R_Zabs.
397 398 399
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
400 401 402
unfold emin.
generalize (prec_gt_0 prec).
clear -Hmax ; omega.
403 404
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
405
(** mantissa, round and sticky bits *)
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456
Record shr_record := { shr_m : Z ; shr_r : bool ; shr_s : bool }.

Definition shr_1 mrs :=
  let '(Build_shr_record m r s) := mrs in
  let s := orb r s in
  match m with
  | Z0 => Build_shr_record Z0 false s
  | Zpos xH => Build_shr_record Z0 true s
  | Zpos (xO p) => Build_shr_record (Zpos p) false s
  | Zpos (xI p) => Build_shr_record (Zpos p) true s
  | Zneg xH => Build_shr_record Z0 true s
  | Zneg (xO p) => Build_shr_record (Zneg p) false s
  | Zneg (xI p) => Build_shr_record (Zneg p) true s
  end.

Definition loc_of_shr_record mrs :=
  match mrs with
  | Build_shr_record _ false false => loc_Exact
  | Build_shr_record _ false true => loc_Inexact Lt
  | Build_shr_record _ true false => loc_Inexact Eq
  | Build_shr_record _ true true => loc_Inexact Gt
  end.

Definition shr_record_of_loc m l :=
  match l with
  | loc_Exact => Build_shr_record m false false
  | loc_Inexact Lt => Build_shr_record m false true
  | loc_Inexact Eq => Build_shr_record m true false
  | loc_Inexact Gt => Build_shr_record m true true
  end.

Theorem shr_m_shr_record_of_loc :
  forall m l,
  shr_m (shr_record_of_loc m l) = m.
Proof.
now intros m [|[| |]].
Qed.

Theorem loc_of_shr_record_of_loc :
  forall m l,
  loc_of_shr_record (shr_record_of_loc m l) = l.
Proof.
now intros m [|[| |]].
Qed.

Definition shr mrs e n :=
  match n with
  | Zpos p => (iter_pos p _ shr_1 mrs, (e + n)%Z)
  | _ => (mrs, e)
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
457
Lemma inbetween_shr_1 :
458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526
  forall x mrs e,
  (0 <= shr_m mrs)%Z ->
  inbetween_float radix2 (shr_m mrs) e x (loc_of_shr_record mrs) ->
  inbetween_float radix2 (shr_m (shr_1 mrs)) (e + 1) x (loc_of_shr_record (shr_1 mrs)).
Proof.
intros x mrs e Hm Hl.
refine (_ (new_location_even_correct (F2R (Float radix2 (shr_m (shr_1 mrs)) (e + 1))) (bpow radix2 e) 2 _ _ _ x (if shr_r (shr_1 mrs) then 1 else 0) (loc_of_shr_record mrs) _ _)) ; try easy.
2: apply bpow_gt_0.
2: now case (shr_r (shr_1 mrs)) ; split.
change (Z2R 2) with (bpow radix2 1).
rewrite <- bpow_plus.
rewrite (Zplus_comm 1), <- (F2R_bpow radix2 (e + 1)).
unfold inbetween_float, F2R. simpl.
rewrite Z2R_plus, Rmult_plus_distr_r.
replace (new_location_even 2 (if shr_r (shr_1 mrs) then 1%Z else 0%Z) (loc_of_shr_record mrs)) with (loc_of_shr_record (shr_1 mrs)).
easy.
clear -Hm.
destruct mrs as (m, r, s).
now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
rewrite (F2R_change_exp radix2 e).
2: apply Zle_succ.
unfold F2R. simpl.
rewrite <- 2!Rmult_plus_distr_r, <- 2!Z2R_plus.
rewrite Zplus_assoc.
replace (shr_m (shr_1 mrs) * 2 ^ (e + 1 - e) + (if shr_r (shr_1 mrs) then 1%Z else 0%Z))%Z with (shr_m mrs).
exact Hl.
ring_simplify (e + 1 - e)%Z.
change (2^1)%Z with 2%Z.
rewrite Zmult_comm.
clear -Hm.
destruct mrs as (m, r, s).
now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
Qed.

Theorem inbetween_shr :
  forall x m e l n,
  (0 <= m)%Z ->
  inbetween_float radix2 m e x l ->
  let '(mrs, e') := shr (shr_record_of_loc m l) e n in
  inbetween_float radix2 (shr_m mrs) e' x (loc_of_shr_record mrs).
Proof.
intros x m e l n Hm Hl.
destruct n as [|n|n].
now destruct l as [|[| |]].
2: now destruct l as [|[| |]].
unfold shr.
rewrite iter_nat_of_P.
rewrite Zpos_eq_Z_of_nat_o_nat_of_P.
induction (nat_of_P n).
simpl.
rewrite Zplus_0_r.
now destruct l as [|[| |]].
simpl iter_nat.
rewrite inj_S.
unfold Zsucc.
rewrite  Zplus_assoc.
revert IHn0.
apply inbetween_shr_1.
clear -Hm.
induction n0.
now destruct l as [|[| |]].
simpl.
revert IHn0.
generalize (iter_nat n0 shr_record shr_1 (shr_record_of_loc m l)).
clear.
intros (m, r, s) Hm.
now destruct m as [|[m|m|]|m] ; try (now elim Hm) ; destruct r as [|] ; destruct s as [|].
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
527
Definition Zdigits2 m :=
528 529
  match m with Z0 => m | Zpos p => Z_of_nat (S (digits2_Pnat p)) | Zneg p => Z_of_nat (S (digits2_Pnat p)) end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
530
Theorem Zdigits2_Zdigits :
531
  forall m,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
532
  Zdigits2 m = Zdigits radix2 m.
533
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
534
unfold Zdigits2.
535 536 537 538
intros [|m|m] ; try apply Z_of_nat_S_digits2_Pnat.
easy.
Qed.

539
Definition shr_fexp m e l :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
540
  shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e).
541 542 543 544 545 546 547 548 549 550 551

Theorem shr_truncate :
  forall m e l,
  (0 <= m)%Z ->
  shr_fexp m e l =
  let '(m', e', l') := truncate radix2 fexp (m, e, l) in (shr_record_of_loc m' l', e').
Proof.
intros m e l Hm.
case_eq (truncate radix2 fexp (m, e, l)).
intros (m', e') l'.
unfold shr_fexp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
552
rewrite Zdigits2_Zdigits.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
553
case_eq (fexp (Zdigits radix2 m + e) - e)%Z.
554 555 556 557 558 559 560 561 562
(* *)
intros He.
unfold truncate.
rewrite He.
simpl.
intros H.
now inversion H.
(* *)
intros p Hp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
563
assert (He: (e <= fexp (Zdigits radix2 m + e))%Z).
564 565
clear -Hp ; zify ; omega.
destruct (inbetween_float_ex radix2 m e l) as (x, Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
566
generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx).
567 568 569 570
assert (Hx0 : (0 <= x)%R).
apply Rle_trans with (F2R (Float radix2 m e)).
now apply F2R_ge_0_compat.
exact (proj1 (inbetween_float_bounds _ _ _ _ _ Hx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
571
case_eq (shr (shr_record_of_loc m l) e (fexp (Zdigits radix2 m + e) - e)).
572
intros mrs e'' H3 H4 H1.
573
generalize (truncate_correct radix2 _ x m e l Hx0 Hx (or_introl _ He)).
574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596
rewrite H1.
intros (H2,_).
rewrite <- Hp, H3.
assert (e'' = e').
change (snd (mrs, e'') = snd (fst (m',e',l'))).
rewrite <- H1, <- H3.
unfold truncate.
now rewrite Hp.
rewrite H in H4 |- *.
apply (f_equal (fun v => (v, _))).
destruct (inbetween_float_unique _ _ _ _ _ _ _ H2 H4) as (H5, H6).
rewrite H5, H6.
case mrs.
now intros m0 [|] [|].
(* *)
intros p Hp.
unfold truncate.
rewrite Hp.
simpl.
intros H.
now inversion H.
Qed.

597 598 599 600
Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.

Definition round_mode m :=
  match m with
601 602 603 604 605
  | mode_NE => ZnearestE
  | mode_ZR => Ztrunc
  | mode_DN => Zfloor
  | mode_UP => Zceil
  | mode_NA => ZnearestA
606
  end.
607 608 609 610 611 612 613 614 615 616

Definition choice_mode m sx mx lx :=
  match m with
  | mode_NE => cond_incr (round_N (negb (Zeven mx)) lx) mx
  | mode_ZR => mx
  | mode_DN => cond_incr (round_sign_DN sx lx) mx
  | mode_UP => cond_incr (round_sign_UP sx lx) mx
  | mode_NA => cond_incr (round_N true lx) mx
  end.

617 618 619 620 621
Global Instance valid_rnd_round_mode : forall m, Valid_rnd (round_mode m).
Proof.
destruct m ; unfold round_mode ; auto with typeclass_instances.
Qed.

622 623 624 625 626 627 628 629 630 631 632 633 634
Definition overflow_to_inf m s :=
  match m with
  | mode_NE => true
  | mode_NA => true
  | mode_ZR => false
  | mode_UP => negb s
  | mode_DN => s
  end.

Definition binary_overflow m s :=
  if overflow_to_inf m s then F754_infinity s
  else F754_finite s (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end) (emax - prec).

BOLDO Sylvie's avatar
BOLDO Sylvie committed
635
Definition binary_round_aux mode sx mx ex lx :=
636 637 638
  let '(mrs', e') := shr_fexp (Zpos mx) ex lx in
  let '(mrs'', e'') := shr_fexp (choice_mode mode sx (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in
  match shr_m mrs'' with
639
  | Z0 => F754_zero sx
640
  | Zpos m => if Zle_bool e'' (emax - prec) then F754_finite sx m e'' else binary_overflow mode sx
641
  | _ => F754_nan (* dummy *)
642 643
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
644
Theorem binary_round_aux_correct :
645 646
  forall mode x mx ex lx,
  inbetween_float radix2 (Zpos mx) ex (Rabs x) lx ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
647
  (ex <= fexp (Zdigits radix2 (Zpos mx) + ex))%Z ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
648
  let z := binary_round_aux mode (Rlt_bool x 0) mx ex lx in
649
  valid_binary z = true /\
650
  if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 emax) then
651 652
    FF2R radix2 z = round radix2 fexp (round_mode mode) x /\
    is_finite_FF z = true
653
  else
654
    z = binary_overflow mode (Rlt_bool x 0).
655
Proof with auto with typeclass_instances.
656
intros m x mx ex lx Bx Ex z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
657
unfold binary_round_aux in z.
658
revert z.
659
rewrite shr_truncate. 2: easy.
660 661
refine (_ (round_trunc_sign_any_correct _ _ (round_mode m) (choice_mode m) _ x (Zpos mx) ex lx Bx (or_introl _ Ex))).
refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Bx Ex)).
662
destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1).
663
rewrite loc_of_shr_record_of_loc, shr_m_shr_record_of_loc.
664 665 666 667 668 669 670 671 672 673 674 675 676 677
set (m1' := choice_mode m (Rlt_bool x 0) m1 l1).
intros (H1a,H1b) H1c.
rewrite H1c.
assert (Hm: (m1 <= m1')%Z).
(* . *)
unfold m1', choice_mode, cond_incr.
case m ;
  try apply Zle_refl ;
  match goal with |- (m1 <= if ?b then _ else _)%Z =>
    case b ; [ apply Zle_succ | apply Zle_refl ] end.
assert (Hr: Rabs (round radix2 fexp (round_mode m) x) = F2R (Float radix2 m1' e1)).
(* . *)
rewrite <- (Zabs_eq m1').
replace (Zabs m1') with (Zabs (cond_Zopp (Rlt_bool x 0) m1')).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
678
rewrite F2R_Zabs.
679 680 681 682 683 684 685 686 687 688 689 690
now apply f_equal.
apply abs_cond_Zopp.
apply Zle_trans with (2 := Hm).
apply Zlt_succ_le.
apply F2R_gt_0_reg with radix2 e1.
apply Rle_lt_trans with (1 := Rabs_pos x).
exact (proj2 (inbetween_float_bounds _ _ _ _ _ H1a)).
(* . *)
assert (Br: inbetween_float radix2 m1' e1 (Rabs (round radix2 fexp (round_mode m) x)) loc_Exact).
now apply inbetween_Exact.
destruct m1' as [|m1'|m1'].
(* . m1' = 0 *)
691
rewrite shr_truncate. 2: apply Zle_refl.
692 693
generalize (truncate_0 radix2 fexp e1 loc_Exact).
destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
694
rewrite shr_m_shr_record_of_loc.
695
intros Hm2.
696
rewrite Hm2.
697
intros z.
698 699
repeat split.
rewrite Rlt_bool_true.
700
repeat split.
701 702
apply sym_eq.
case Rlt_bool ; apply F2R_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
703
rewrite <- F2R_Zabs, abs_cond_Zopp, F2R_0.
704
apply bpow_gt_0.
705
(* . 0 < m1' *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
706 707
assert (He: (e1 <= fexp (Zdigits radix2 (Zpos m1') + e1))%Z).
rewrite <- ln_beta_F2R_Zdigits, <- Hr, ln_beta_abs.
708 709
2: discriminate.
rewrite H1b.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
710 711 712
rewrite canonic_exp_abs.
fold (canonic_exp radix2 fexp (round radix2 fexp (round_mode m) x)).
apply canonic_exp_round_ge...
713 714 715 716 717 718
rewrite H1c.
case (Rlt_bool x 0).
apply Rlt_not_eq.
now apply F2R_lt_0_compat.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
719
refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)).
720 721 722
2: now rewrite Hr ; apply F2R_gt_0_compat.
refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)).
2: discriminate.
723
rewrite shr_truncate. 2: easy.
724
destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2).
725
rewrite shr_m_shr_record_of_loc.
726 727 728 729 730
intros (H3,H4) (H2,_).
destruct m2 as [|m2|m2].
elim Rgt_not_eq with (2 := H3).
rewrite F2R_0.
now apply F2R_gt_0_compat.
731
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, <- F2R_abs.
732
simpl Zabs.
733 734 735 736
case_eq (Zle_bool e2 (emax - prec)) ; intros He2.
assert (bounded m2 e2 = true).
apply andb_true_intro.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
737
unfold canonic_mantissa.
738 739
apply Zeq_bool_true.
rewrite Z_of_nat_S_digits2_Pnat.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
740
rewrite <- ln_beta_F2R_Zdigits.
741 742 743 744 745
apply sym_eq.
now rewrite H3 in H4.
discriminate.
exact He2.
apply (conj H).
746
rewrite Rlt_bool_true.
747
repeat split.
748 749
apply F2R_cond_Zopp.
now apply bounded_lt_emax.
750 751 752 753
rewrite (Rlt_bool_false _ (bpow radix2 emax)).
refine (conj _ (refl_equal _)).
unfold binary_overflow.
case overflow_to_inf.
754
apply refl_equal.
755 756 757 758 759 760
unfold valid_binary, bounded.
rewrite Zle_bool_refl.
rewrite Bool.andb_true_r.
apply Zeq_bool_true.
rewrite Z_of_nat_S_digits2_Pnat.
change Fcalc_digits.radix2 with radix2.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
761
replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
762
unfold fexp, FLT_exp, emin.
763 764
generalize (prec_gt_0 prec).
clear -Hmax ; zify ; omega.
765 766
change 2%Z with (radix_val radix2).
case_eq (Zpower radix2 prec - 1)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
767
simpl Zdigits.
768
generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
769 770 771
clear ; omega.
intros p Hp.
apply Zle_antisym.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
772 773
cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega.
apply Zdigits_gt_Zpower.
774 775 776 777 778 779 780
simpl Zabs. rewrite <- Hp.
cut (Zpower radix2 (prec - 1) < Zpower radix2 prec)%Z. clear ; omega.
apply lt_Z2R.
rewrite 2!Z2R_Zpower. 2: now apply Zlt_le_weak.
apply bpow_lt.
apply Zlt_pred.
now apply Zlt_0_le_0_pred.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
781
apply Zdigits_le_Zpower.
782 783 784
simpl Zabs. rewrite <- Hp.
apply Zlt_pred.
intros p Hp.
785
generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
786
clear -Hp ; zify ; omega.
787 788
apply Rnot_lt_le.
intros Hx.
789 790 791 792
generalize (refl_equal (bounded m2 e2)).
unfold bounded at 2.
rewrite He2.
rewrite Bool.andb_false_r.
793 794
rewrite bounded_canonic_lt_emax with (2 := Hx).
discriminate.
795 796 797 798 799 800 801
unfold canonic.
now rewrite <- H3.
elim Rgt_not_eq with (2 := H3).
apply Rlt_trans with R0.
now apply F2R_lt_0_compat.
now apply F2R_gt_0_compat.
rewrite <- Hr.
802 803
apply generic_format_abs...
apply generic_format_round...
804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819
(* . not m1' < 0 *)
elim Rgt_not_eq with (2 := Hr).
apply Rlt_le_trans with R0.
now apply F2R_lt_0_compat.
apply Rabs_pos.
(* *)
apply Rlt_le_trans with (2 := proj1 (inbetween_float_bounds _ _ _ _ _ Bx)).
now apply F2R_gt_0_compat.
(* all the modes are valid *)
clear. case m.
exact inbetween_int_NE_sign.
exact inbetween_int_ZR_sign.
exact inbetween_int_DN_sign.
exact inbetween_int_UP_sign.
exact inbetween_int_NA_sign.
Qed.
820

821 822 823 824 825 826 827 828
Definition Bsign x :=
  match x with
  | B754_nan => false
  | B754_zero s => s
  | B754_infinity s => s
  | B754_finite s _ _ _ => s
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
829
Definition sign_FF x :=
830 831 832 833 834 835 836 837 838
  match x with
  | F754_nan => false
  | F754_zero s => s
  | F754_infinity s => s
  | F754_finite s _ _ => s
  end.

Theorem Bsign_FF2B :
  forall x H,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
839
  Bsign (FF2B x H) = sign_FF x.
840 841 842 843
Proof.
now intros [sx|sx| |sx mx ex] H.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
844 845
(** Multiplication *)

846 847 848 849
Lemma Bmult_correct_aux :
  forall m sx mx ex (Hx : bounded mx ex = true) sy my ey (Hy : bounded my ey = true),
  let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
  let y := F2R (Float radix2 (cond_Zopp sy (Zpos my)) ey) in
BOLDO Sylvie's avatar
BOLDO Sylvie committed
850
  let z := binary_round_aux m (xorb sx sy) (mx * my) (ex + ey) loc_Exact in
851 852
  valid_binary z = true /\
  if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x * y))) (bpow radix2 emax) then
853 854
    FF2R radix2 z = round radix2 fexp (round_mode m) (x * y) /\
    is_finite_FF z = true
855
  else
856
    z = binary_overflow m (xorb sx sy).
857
Proof.
858 859
intros m sx mx ex Hx sy my ey Hy x y.
unfold x, y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
860
rewrite <- F2R_mult.
861
simpl.
862
replace (xorb sx sy) with (Rlt_bool (F2R (Float radix2 (cond_Zopp sx (Zpos mx) * cond_Zopp sy (Zpos my)) (ex + ey))) 0).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
863
apply binary_round_aux_correct.
864
constructor.
865
rewrite <- F2R_abs.
866 867 868 869 870
apply F2R_eq_compat.
rewrite Zabs_Zmult.
now rewrite 2!abs_cond_Zopp.
(* *)
change (Zpos (mx * my)) with (Zpos mx * Zpos my)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
871
assert (forall m e, bounded m e = true -> fexp (Zdigits radix2 (Zpos m) + e) = e)%Z.
872 873 874 875 876
clear. intros m e Hb.
destruct (andb_prop _ _ Hb) as (H,_).
apply Zeq_bool_eq.
now rewrite <- Z_of_nat_S_digits2_Pnat.
generalize (H _ _ Hx) (H _ _ Hy).
877
clear x y sx sy Hx Hy H.
878
unfold fexp, FLT_exp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
879
refine (_ (Zdigits_mult_ge radix2 (Zpos mx) (Zpos my) _ _)) ; try discriminate.
880
refine (_ (Zdigits_gt_0 radix2 (Zpos mx) _) (Zdigits_gt_0 radix2 (Zpos my) _)) ; try discriminate.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
881
generalize (Zdigits radix2 (Zpos mx)) (Zdigits radix2 (Zpos my)) (Zdigits radix2 (Zpos mx * Zpos my)).
882
clear -Hmax.
883
unfold emin.
884 885 886 887 888 889 890 891 892 893 894 895 896 897
intros dx dy dxy Hx Hy Hxy.
zify ; intros ; subst.
omega.
(* *)
case sx ; case sy.
apply Rlt_bool_false.
now apply F2R_ge_0_compat.
apply Rlt_bool_true.
now apply F2R_lt_0_compat.
apply Rlt_bool_true.
now apply F2R_lt_0_compat.
apply Rlt_bool_false.
now apply F2R_ge_0_compat.
Qed.
898

899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917
Definition Bmult m x y :=
  match x, y with
  | B754_nan, _ => x
  | _, B754_nan => y
  | B754_infinity sx, B754_infinity sy => B754_infinity (xorb sx sy)
  | B754_infinity sx, B754_finite sy _ _ _ => B754_infinity (xorb sx sy)
  | B754_finite sx _ _ _, B754_infinity sy => B754_infinity (xorb sx sy)
  | B754_infinity _, B754_zero _ => B754_nan
  | B754_zero _, B754_infinity _ => B754_nan
  | B754_finite sx _ _ _, B754_zero sy => B754_zero (xorb sx sy)
  | B754_zero sx, B754_finite sy _ _ _ => B754_zero (xorb sx sy)
  | B754_zero sx, B754_zero sy => B754_zero (xorb sx sy)
  | B754_finite sx mx ex Hx, B754_finite sy my ey Hy =>
    FF2B _ (proj1 (Bmult_correct_aux m sx mx ex Hx sy my ey Hy))
  end.

Theorem Bmult_correct :
  forall m x y,
  if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then
918 919
    B2R (Bmult m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
    is_finite (Bmult m x y) = andb (is_finite x) (is_finite y)
920
  else
921
    B2FF (Bmult m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
922 923
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ;
924
  try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ split ; apply refl_equal | apply bpow_gt_0 | auto with typeclass_instances ] ).
925 926
simpl.
case Bmult_correct_aux.
927 928 929 930
intros H1.
case Rlt_bool.
intros (H2, H3).
split.
931
now rewrite B2R_FF2B.
932 933
now rewrite is_finite_FF2B.
intros H2.
934 935 936
now rewrite B2FF_FF2B.
Qed.

937 938 939 940 941 942 943 944 945 946 947 948 949
Definition Bmult_FF m x y :=
  match x, y with
  | F754_nan, _ => x
  | _, F754_nan => y
  | F754_infinity sx, F754_infinity sy => F754_infinity (xorb sx sy)
  | F754_infinity sx, F754_finite sy _ _ => F754_infinity (xorb sx sy)
  | F754_finite sx _ _, F754_infinity sy => F754_infinity (xorb sx sy)
  | F754_infinity _, F754_zero _ => F754_nan
  | F754_zero _, F754_infinity _ => F754_nan
  | F754_finite sx _ _, F754_zero sy => F754_zero (xorb sx sy)
  | F754_zero sx, F754_finite sy _ _ => F754_zero (xorb sx sy)
  | F754_zero sx, F754_zero sy => F754_zero (xorb sx sy)
  | F754_finite sx mx ex, F754_finite sy my ey =>
BOLDO Sylvie's avatar
BOLDO Sylvie committed
950
    binary_round_aux m (xorb sx sy) (mx * my) (ex + ey) loc_Exact
951 952 953 954 955 956 957 958 959 960
  end.

Theorem B2FF_Bmult :
  forall m x y,
  B2FF (Bmult m x y) = Bmult_FF m (B2FF x) (B2FF y).
Proof.
intros m [sx|sx| |sx mx ex Hx] [sy|sy| |sy my ey Hy] ; try easy.
apply B2FF_FF2B.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
961 962

Definition shl_align mx ex ex' :=
963 964 965 966 967
  match (ex' - ex)%Z with
  | Zneg d => (shift_pos d mx, ex')
  | _ => (mx, ex)
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
968
Theorem shl_align_correct :
969
  forall mx ex ex',
BOLDO Sylvie's avatar
BOLDO Sylvie committed
970
  let (mx', ex'') := shl_align mx ex ex' in
971 972
  F2R (Float radix2 (Zpos mx) ex) = F2R (Float radix2 (Zpos mx') ex'') /\
  (ex'' <= ex')%Z.
973
Proof.
974
intros mx ex ex'.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
975
unfold shl_align.
976
case_eq (ex' - ex)%Z.
977 978 979 980 981 982 983 984
(* d = 0 *)
intros H.
repeat split.
rewrite Zminus_eq with (1 := H).
apply Zle_refl.
(* d > 0 *)
intros d Hd.
repeat split.
985
replace ex' with (ex' - ex + ex)%Z by ring.
986 987 988 989 990 991 992 993 994 995
rewrite Hd.
pattern ex at 1 ; rewrite <- Zplus_0_l.
now apply Zplus_le_compat_r.
(* d < 0 *)
intros d Hd.
rewrite shift_pos_correct, Zmult_comm.
change (Zpower_pos 2 d) with (Zpower radix2 (Zpos d)).
change (Zpos d) with (Zopp (Zneg d)).
rewrite <- Hd.
split.
996
replace (- (ex' - ex))%Z with (ex - ex')%Z by ring.
997 998
apply F2R_change_exp.
apply Zle_0_minus_le.
999
replace (ex - ex')%Z with (- (ex' - ex))%Z by ring.
1000 1001 1002
now rewrite Hd.
apply Zle_refl.
Qed.
1003

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1004
Theorem snd_shl_align :
1005 1006
  forall mx ex ex',
  (ex' <= ex)%Z ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1007
  snd (shl_align mx ex ex') = ex'.
1008 1009
Proof.
intros mx ex ex' He.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1010
unfold shl_align.
1011 1012 1013 1014 1015 1016 1017 1018 1019
case_eq (ex' - ex)%Z ; simpl.
intros H.
now rewrite Zminus_eq with (1 := H).
intros p.
clear -He ; zify ; omega.
intros.
apply refl_equal.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1020 1021
Definition shl_align_fexp mx ex :=
  shl_align mx ex (fexp (Z_of_nat (S (digits2_Pnat mx)) + ex)).
1022

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1023
Theorem shl_align_fexp_correct :
1024
  forall mx ex,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1025
  let (mx', ex') := shl_align_fexp mx ex in
1026
  F2R (Float radix2 (Zpos mx) ex) = F2R (Float radix2 (Zpos mx') ex') /\
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1027
  (ex' <= fexp (Zdigits radix2 (Zpos mx') + ex'))%Z.
1028 1029
Proof.
intros mx ex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1030 1031
unfold shl_align_fexp.
generalize (shl_align_correct mx ex (fexp (Z_of_nat (S (digits2_Pnat mx)) + ex))).
1032
rewrite Z_of_nat_S_digits2_Pnat.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1033
case shl_align.
1034 1035 1036
intros mx' ex' (H1, H2).
split.
exact H1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1037
rewrite <- ln_beta_F2R_Zdigits. 2: easy.
1038
rewrite <- H1.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1039
now rewrite ln_beta_F2R_Zdigits.
1040 1041
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1042 1043
Definition binary_round m sx mx ex :=
  let '(mz, ez) := shl_align_fexp mx ex in binary_round_aux m sx mz ez loc_Exact.
1044

BOLDO Sylvie's avatar
BOLDO Sylvie committed
1045
Theorem binary_round_correct :
1046
  forall m sx mx ex,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1047
  let z := binary_round m sx mx ex in
1048 1049
  valid_binary z = true /\
  let x := F2R (Float radix2 (cond_Zopp sx (Zpos mx)) ex) in
1050
  if Rlt_bool (Rabs (round radix2 fexp (round_mode m) x)) (bpow radix2 emax) then
1051 1052
    FF2R radix2 z = round radix2 fexp (round_mode m) x /\
    is_finite_FF z = true
1053
  else
1054
    z = binary_overflow m sx.
1055 1056
Proof.
intros m sx mx ex.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
1057 1058 1059
unfold binary_round.
generalize (shl_align_fexp_correct mx ex).
destruct (shl_align_fexp mx ex) as (mz, ez).
Guillaume Melquiond's avatar