Fappli_IEEE.v 49.5 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 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
Section AnyRadix.

Inductive full_float :=
  | F754_zero : bool -> full_float
  | F754_infinity : bool -> full_float
36
  | F754_nan : bool -> positive -> full_float
37 38
  | 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.

49 50
Implicit Arguments exist [[A] [P]].

BOLDO Sylvie's avatar
BOLDO Sylvie committed
51 52 53
(** 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 *)
54
Variable prec emax : Z.
55
Context (prec_gt_0_ : Prec_gt_0 prec).
56
Hypothesis Hmax : (prec < emax)%Z.
57

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

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

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

69 70 71
Definition valid_binary x :=
  match x with
  | F754_finite _ m e => bounded m e
72
  | F754_nan _ pl => (Z_of_nat (S (digits2_Pnat pl)) <? prec)%Z
73 74 75
  | _ => true
  end.

76
(** Basic type used for representing binary FP numbers.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
77 78
    Note that there is exactly one such object per FP datum.
    NaNs do not have any payload. They cannot be distinguished. *)
79

80
Definition nan_pl := {pl | (Z_of_nat (S (digits2_Pnat pl)) <? prec)%Z  = true}.
81

82 83 84
Inductive binary_float :=
  | B754_zero : bool -> binary_float
  | B754_infinity : bool -> binary_float
85
  | B754_nan : bool -> nan_pl -> binary_float
86 87 88
  | B754_finite : bool ->
    forall (m : positive) (e : Z), bounded m e = true -> binary_float.

89 90 91 92 93
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
94
  | F754_nan b pl => fun H => B754_nan b (exist pl H)
95 96 97 98 99 100 101
  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
102
  | B754_nan b (exist pl _) => F754_nan b pl
103 104
  end.

105 106 107 108
Definition radix2 := Build_radix 2 (refl_equal true).

Definition B2R f :=
  match f with
Guillaume Melquiond's avatar
Guillaume Melquiond committed
109
  | B754_finite s m e _ => F2R (Float radix2 (cond_Zopp s (Zpos m)) e)
110 111 112
  | _ => R0
  end.

113 114 115 116
Theorem FF2R_B2FF :
  forall x,
  FF2R radix2 (B2FF x) = B2R x.
Proof.
117
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
118 119 120 121 122 123
Qed.

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

127 128 129 130
Theorem valid_binary_B2FF :
  forall x,
  valid_binary (B2FF x) = true.
Proof.
131
now intros [sx|sx|sx [plx Hplx]|sx mx ex Hx].
132 133 134 135 136 137
Qed.

Theorem FF2B_B2FF :
  forall x H,
  FF2B (B2FF x) H = x.
Proof.
138 139 140
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] H ; try easy.
simpl. apply f_equal, f_equal, eqbool_irrelevance.
apply f_equal, eqbool_irrelevance.
141 142 143 144 145 146 147 148 149 150
Qed.

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

151 152 153 154
Theorem B2R_FF2B :
  forall x Hx,
  B2R (FF2B x Hx) = FF2R radix2 x.
Proof.
155
now intros [sx|sx|sx plx|sx mx ex] Hx.
156 157
Qed.

158 159 160 161 162
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
163
  | B754_nan b (exist p _) => fn b p
164 165 166 167 168
  | B754_finite sx mx ex _ => ff sx mx ex
  end =
  match x with
  | F754_zero sx => fz sx
  | F754_infinity sx => fi sx
169
  | F754_nan b p => fn b p
170 171 172
  | F754_finite sx mx ex => ff sx mx ex
  end.
Proof.
173
now intros T fz fi fn ff [sx|sx|sx plx|sx mx ex] Hx.
174 175
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
176
Theorem canonic_canonic_mantissa :
177
  forall (sx : bool) mx ex,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
178
  canonic_mantissa mx ex = true ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
179
  canonic radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
180 181 182 183 184 185 186
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
187 188
rewrite ln_beta_F2R_Zdigits.
rewrite <- Zdigits_abs.
189 190 191 192 193 194 195 196 197
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.
198
intros [sx|sx|sx plx|sx mx ex Hx] ; try apply generic_format_0.
199 200
simpl.
apply generic_format_canonic.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
201
apply canonic_canonic_mantissa.
202 203 204
now destruct (andb_prop _ _ Hx) as (H, _).
Qed.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
205 206 207
Theorem FLT_format_B2R :
  forall x,
  FLT_format radix2 emin prec (B2R x).
208
Proof with auto with typeclass_instances.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
209 210 211 212 213
intros x.
apply FLT_format_generic...
apply generic_format_B2R.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
214
Theorem B2FF_inj :
215 216 217 218
  forall x y : binary_float,
  B2FF x = B2FF y ->
  x = y.
Proof.
219
intros [sx|sx|sx [plx Hplx]|sx mx ex Hx] [sy|sy|sy [ply Hply]|sy my ey Hy] ; try easy.
220 221 222 223 224 225 226 227 228 229
(* *)
intros H.
now inversion H.
(* *)
intros H.
now inversion H.
(* *)
intros H.
inversion H.
clear H.
230 231 232 233 234 235 236 237
revert Hplx.
rewrite H2.
intros Hx.
apply f_equal, f_equal, eqbool_irrelevance.
(* *)
intros H.
inversion H.
clear H.
238 239 240
revert Hx.
rewrite H2, H3.
intros Hx.
241
apply f_equal, eqbool_irrelevance.
242 243
Qed.

244 245 246 247 248 249
Definition is_finite_strict f :=
  match f with
  | B754_finite _ _ _ _ => true
  | _ => false
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
250
Theorem B2R_inj:
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277
  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
278
apply canonic_canonic_mantissa.
279
exact (proj1 (andb_prop _ _ Hx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
280
apply canonic_canonic_mantissa.
281 282 283 284 285 286 287 288 289
exact (proj1 (andb_prop _ _ Hy)).
(* *)
revert Hx.
rewrite Hs, (proj1 H), (proj2 H).
intros Hx.
apply f_equal.
apply eqbool_irrelevance.
Qed.

290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
Definition Bsign x :=
  match x with
  | B754_nan s _ => s
  | B754_zero s => s
  | B754_infinity s => s
  | B754_finite s _ _ _ => s
  end.

Definition sign_FF x :=
  match x with
  | F754_nan s _ => s
  | F754_zero s => s
  | F754_infinity s => s
  | F754_finite s _ _ => s
  end.

Theorem Bsign_FF2B :
  forall x H,
  Bsign (FF2B x H) = sign_FF x.
Proof.
now intros [sx|sx|sx plx|sx mx ex] H.
Qed.

313 314 315 316 317 318 319
Definition is_finite f :=
  match f with
  | B754_finite _ _ _ _ => true
  | B754_zero _ => true
  | _ => false
  end.

320 321 322 323 324 325 326 327 328 329 330 331 332 333
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.

334 335 336 337
Theorem is_finite_FF_B2FF :
  forall x,
  is_finite_FF (B2FF x) = is_finite x.
Proof.
338 339 340
now intros [| |? []|].
Qed.

341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360
Theorem B2R_Bsign_inj:
  forall x y : binary_float,
    is_finite x = true ->
    is_finite y = true ->
    B2R x = B2R y ->
    Bsign x = Bsign y ->
    x = y.
Proof.
intros. destruct x, y; try (apply B2R_inj; now eauto).
- simpl in H2. congruence.
- symmetry in H1. apply Rmult_integral in H1.
  destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b0; discriminate H1.
  simpl in H1. pose proof (bpow_gt_0 radix2 e).
  rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
- apply Rmult_integral in H1.
  destruct H1. apply eq_Z2R with (n:=0%Z) in H1. destruct b; discriminate H1.
  simpl in H1. pose proof (bpow_gt_0 radix2 e).
  rewrite H1 in H3. apply Rlt_irrefl in H3. destruct H3.
Qed.

361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376
Definition is_nan f :=
  match f with
  | B754_nan _ _ => true
  | _ => false
  end.

Definition is_nan_FF f :=
  match f with
  | F754_nan _ _ => true
  | _ => false
  end.

Theorem is_nan_FF2B :
  forall x Hx,
  is_nan (FF2B x Hx) = is_nan_FF x.
Proof.
377 378 379
now intros [| | |].
Qed.

380 381 382 383 384 385 386 387
Theorem is_nan_FF_B2FF :
  forall x,
  is_nan_FF (B2FF x) = is_nan x.
Proof.
now intros [| |? []|].
Qed.

Definition Bopp opp_nan x :=
Guillaume Melquiond's avatar
Guillaume Melquiond committed
388
  match x with
389 390
  | B754_nan sx plx =>
    let '(sres, plres) := opp_nan sx plx in B754_nan sres plres
Guillaume Melquiond's avatar
Guillaume Melquiond committed
391 392 393 394 395 396
  | 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 :
397 398 399
  forall opp_nan x,
  is_nan x = false ->
  Bopp opp_nan (Bopp opp_nan x) = x.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
400
Proof.
401
now intros opp_nan [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try rewrite Bool.negb_involutive.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
402 403 404
Qed.

Theorem B2R_Bopp :
405 406
  forall opp_nan x,
  B2R (Bopp opp_nan x) = (- B2R x)%R.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
407
Proof.
408 409
intros opp_nan [sx|sx|sx plx|sx mx ex Hx]; apply sym_eq ; try apply Ropp_0.
simpl. destruct opp_nan. apply Ropp_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
410
simpl.
411
rewrite <- F2R_opp.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
412 413 414
now case sx.
Qed.

415 416 417
Theorem is_finite_Bopp :
  forall opp_nan x,
  is_finite (Bopp opp_nan x) = is_finite x.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
418
Proof.
419 420 421 422
intros opp_nan [| | |] ; try easy.
intros s pl.
simpl.
now case opp_nan.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
423 424
Qed.

425 426 427
Theorem bounded_lt_emax :
  forall mx ex,
  bounded mx ex = true ->
428
  (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R.
429
Proof.
430
intros mx ex Hx.
431 432 433
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
434
generalize (ln_beta_F2R_Zdigits radix2 (Zpos mx) ex).
435 436 437 438
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').
439
change (Zpos mx) with (Zabs (Zpos mx)).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
440
rewrite F2R_Zabs.
441 442 443 444 445 446 447 448 449
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
450
generalize (Zdigits radix2 (Zpos mx)).
451 452
intros ; zify ; subst.
clear -H H2. clearbody emin.
453 454 455
omega.
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
456
Theorem abs_B2R_lt_emax :
457
  forall x,
458
  (Rabs (B2R x) < bpow radix2 emax)%R.
459
Proof.
460
intros [sx|sx|sx plx|sx mx ex Hx] ; simpl ; try ( rewrite Rabs_R0 ; apply bpow_gt_0 ).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
461
rewrite <- F2R_Zabs, abs_cond_Zopp.
462 463 464
now apply bounded_lt_emax.
Qed.

465 466 467
Theorem bounded_canonic_lt_emax :
  forall mx ex,
  canonic radix2 fexp (Float radix2 (Zpos mx) ex) ->
468
  (F2R (Float radix2 (Zpos mx) ex) < bpow radix2 emax)%R ->
469 470
  bounded mx ex = true.
Proof.
471
intros mx ex Cx Bx.
472 473
apply andb_true_intro.
split.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
474
unfold canonic_mantissa.
475 476 477 478
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
479 480
unfold canonic_exp.
rewrite ln_beta_F2R_Zdigits. 2: discriminate.
481 482 483 484
now apply -> Zeq_is_eq_bool.
apply Zle_bool_true.
unfold canonic, Fexp in Cx.
rewrite Cx.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
485
unfold canonic_exp, fexp, FLT_exp.
486
destruct (ln_beta radix2 (F2R (Float radix2 (Zpos mx) ex))) as (e',Ex). simpl.
487 488
apply Zmax_lub.
cut (e' - 1 < emax)%Z. clear ; omega.
489 490 491
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
492
rewrite F2R_Zabs.
493 494 495
apply Ex.
apply Rgt_not_eq.
now apply F2R_gt_0_compat.
496 497 498
unfold emin.
generalize (prec_gt_0 prec).
clear -Hmax ; omega.
499 500
Qed.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
501
(** mantissa, round and sticky bits *)
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 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552
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
553
Lemma inbetween_shr_1 :
554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605
  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 [|[| |]].
606
simpl nat_rect.
607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622
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
623
Definition Zdigits2 m :=
624 625
  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
626
Theorem Zdigits2_Zdigits :
627
  forall m,
BOLDO Sylvie's avatar
BOLDO Sylvie committed
628
  Zdigits2 m = Zdigits radix2 m.
629
Proof.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
630
unfold Zdigits2.
631 632 633 634
intros [|m|m] ; try apply Z_of_nat_S_digits2_Pnat.
easy.
Qed.

635
Definition shr_fexp m e l :=
BOLDO Sylvie's avatar
BOLDO Sylvie committed
636
  shr (shr_record_of_loc m l) e (fexp (Zdigits2 m + e) - e).
637 638 639 640 641 642 643 644 645 646 647

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
648
rewrite Zdigits2_Zdigits.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
649
case_eq (fexp (Zdigits radix2 m + e) - e)%Z.
650 651 652 653 654 655 656 657 658
(* *)
intros He.
unfold truncate.
rewrite He.
simpl.
intros H.
now inversion H.
(* *)
intros p Hp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
659
assert (He: (e <= fexp (Zdigits radix2 m + e))%Z).
660 661
clear -Hp ; zify ; omega.
destruct (inbetween_float_ex radix2 m e l) as (x, Hx).
BOLDO Sylvie's avatar
BOLDO Sylvie committed
662
generalize (inbetween_shr x m e l (fexp (Zdigits radix2 m + e) - e) Hm Hx).
663 664 665 666
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
667
case_eq (shr (shr_record_of_loc m l) e (fexp (Zdigits radix2 m + e) - e)).
668
intros mrs e'' H3 H4 H1.
669
generalize (truncate_correct radix2 _ x m e l Hx0 Hx (or_introl _ He)).
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692
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.

693 694 695 696
Inductive mode := mode_NE | mode_ZR | mode_DN | mode_UP | mode_NA.

Definition round_mode m :=
  match m with
697 698 699 700 701
  | mode_NE => ZnearestE
  | mode_ZR => Ztrunc
  | mode_DN => Zfloor
  | mode_UP => Zceil
  | mode_NA => ZnearestA
702
  end.
703 704 705 706 707 708 709 710 711 712

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.

713 714 715 716 717
Global Instance valid_rnd_round_mode : forall m, Valid_rnd (round_mode m).
Proof.
destruct m ; unfold round_mode ; auto with typeclass_instances.
Qed.

718 719 720 721 722 723 724 725 726 727 728 729 730
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
731
Definition binary_round_aux mode sx mx ex lx :=
732 733 734
  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
735
  | Z0 => F754_zero sx
736
  | Zpos m => if Zle_bool e'' (emax - prec) then F754_finite sx m e'' else binary_overflow mode sx
737
  | _ => F754_nan false xH (* dummy *)
738 739
  end.

BOLDO Sylvie's avatar
BOLDO Sylvie committed
740
Theorem binary_round_aux_correct :
741 742
  forall mode x mx ex lx,
  inbetween_float radix2 (Zpos mx) ex (Rabs x) lx ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
743
  (ex <= fexp (Zdigits radix2 (Zpos mx) + ex))%Z ->
BOLDO Sylvie's avatar
BOLDO Sylvie committed
744
  let z := binary_round_aux mode (Rlt_bool x 0) mx ex lx in
745
  valid_binary z = true /\
746
  if Rlt_bool (Rabs (round radix2 fexp (round_mode mode) x)) (bpow radix2 emax) then
747
    FF2R radix2 z = round radix2 fexp (round_mode mode) x /\
748
    is_finite_FF z = true /\ sign_FF z = Rlt_bool x 0
749
  else
750
    z = binary_overflow mode (Rlt_bool x 0).
751
Proof with auto with typeclass_instances.
752
intros m x mx ex lx Bx Ex z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
753
unfold binary_round_aux in z.
754
revert z.
755
rewrite shr_truncate. 2: easy.
756 757
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)).
758
destruct (truncate radix2 fexp (Zpos mx, ex, lx)) as ((m1, e1), l1).
759
rewrite loc_of_shr_record_of_loc, shr_m_shr_record_of_loc.
760 761 762 763 764 765 766 767 768 769 770 771 772 773
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
774
rewrite F2R_Zabs.
775 776 777 778 779 780 781 782 783 784 785 786
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 *)
787
rewrite shr_truncate. 2: apply Zle_refl.
788 789
generalize (truncate_0 radix2 fexp e1 loc_Exact).
destruct (truncate radix2 fexp (Z0, e1, loc_Exact)) as ((m2, e2), l2).
790
rewrite shr_m_shr_record_of_loc.
791
intros Hm2.
792
rewrite Hm2.
793
intros z.
794 795
repeat split.
rewrite Rlt_bool_true.
796
repeat split.
797 798
apply sym_eq.
case Rlt_bool ; apply F2R_0.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
799
rewrite <- F2R_Zabs, abs_cond_Zopp, F2R_0.
800
apply bpow_gt_0.
801
(* . 0 < m1' *)
BOLDO Sylvie's avatar
BOLDO Sylvie committed
802 803
assert (He: (e1 <= fexp (Zdigits radix2 (Zpos m1') + e1))%Z).
rewrite <- ln_beta_F2R_Zdigits, <- Hr, ln_beta_abs.
804 805
2: discriminate.
rewrite H1b.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
806 807 808
rewrite canonic_exp_abs.
fold (canonic_exp radix2 fexp (round radix2 fexp (round_mode m) x)).
apply canonic_exp_round_ge...
809 810 811 812 813 814
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.
815
refine (_ (truncate_correct_partial _ _ _ _ _ _ _ Br He)).
816 817 818
2: now rewrite Hr ; apply F2R_gt_0_compat.
refine (_ (truncate_correct_format radix2 fexp (Zpos m1') e1 _ _ He)).
2: discriminate.
819
rewrite shr_truncate. 2: easy.
820
destruct (truncate radix2 fexp (Zpos m1', e1, loc_Exact)) as ((m2, e2), l2).
821
rewrite shr_m_shr_record_of_loc.
822 823 824 825 826
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.
827
rewrite F2R_cond_Zopp, H3, abs_cond_Ropp, <- F2R_abs.
828
simpl Zabs.
829 830 831 832
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
833
unfold canonic_mantissa.
834 835
apply Zeq_bool_true.
rewrite Z_of_nat_S_digits2_Pnat.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
836
rewrite <- ln_beta_F2R_Zdigits.
837 838 839 840 841
apply sym_eq.
now rewrite H3 in H4.
discriminate.
exact He2.
apply (conj H).
842
rewrite Rlt_bool_true.
843
repeat split.
844 845
apply F2R_cond_Zopp.
now apply bounded_lt_emax.
846 847 848 849
rewrite (Rlt_bool_false _ (bpow radix2 emax)).
refine (conj _ (refl_equal _)).
unfold binary_overflow.
case overflow_to_inf.
850
apply refl_equal.
851 852 853 854 855 856
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
857
replace (Zdigits radix2 (Zpos (match (Zpower 2 prec - 1)%Z with Zpos p => p | _ => xH end))) with prec.
858
unfold fexp, FLT_exp, emin.
859 860
generalize (prec_gt_0 prec).
clear -Hmax ; zify ; omega.
861 862
change 2%Z with (radix_val radix2).
case_eq (Zpower radix2 prec - 1)%Z.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
863
simpl Zdigits.
864
generalize (Zpower_gt_1 radix2 prec (prec_gt_0 prec)).
865 866 867
clear ; omega.
intros p Hp.
apply Zle_antisym.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
868 869
cut (prec - 1 < Zdigits radix2 (Zpos p))%Z. clear ; omega.
apply Zdigits_gt_Zpower.
870 871 872 873 874 875 876
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
877
apply Zdigits_le_Zpower.
878 879 880
simpl Zabs. rewrite <- Hp.
apply Zlt_pred.
intros p Hp.
881
generalize (Zpower_gt_1 radix2 _ (prec_gt_0 prec)).
882
clear -Hp ; zify ; omega.
883 884
apply Rnot_lt_le.
intros Hx.
885 886 887 888
generalize (refl_equal (bounded m2 e2)).
unfold bounded at 2.
rewrite He2.
rewrite Bool.andb_false_r.
889 890
rewrite bounded_canonic_lt_emax with (2 := Hx).
discriminate.
891 892 893 894 895 896 897
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.
898 899
apply generic_format_abs...
apply generic_format_round...
900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915
(* . 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.
916

BOLDO Sylvie's avatar
BOLDO Sylvie committed
917 918
(** Multiplication *)

919 920 921 922
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
923
  let z := binary_round_aux m (xorb sx sy) (mx * my) (ex + ey) loc_Exact in
924 925
  valid_binary z = true /\
  if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (x * y))) (bpow radix2 emax) then
926
    FF2R radix2 z = round radix2 fexp (round_mode m) (x * y) /\
927
    is_finite_FF z = true /\ sign_FF z = xorb sx sy
928
  else
929
    z = binary_overflow m (xorb sx sy).
930
Proof.
931 932
intros m sx mx ex Hx sy my ey Hy x y.
unfold x, y.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
933
rewrite <- F2R_mult.
934
simpl.
935
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
936
apply binary_round_aux_correct.
937
constructor.
938
rewrite <- F2R_abs.
939 940 941 942 943
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
944
assert (forall m e, bounded m e = true -> fexp (Zdigits radix2 (Zpos m) + e) = e)%Z.
945 946 947 948 949
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).
950
clear x y sx sy Hx Hy H.
951
unfold fexp, FLT_exp.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
952
refine (_ (Zdigits_mult_ge radix2 (Zpos mx) (Zpos my) _ _)) ; try discriminate.
953
refine (_ (Zdigits_gt_0 radix2 (Zpos mx) _) (Zdigits_gt_0 radix2 (Zpos my) _)) ; try discriminate.
BOLDO Sylvie's avatar
BOLDO Sylvie committed
954
generalize (Zdigits radix2 (Zpos mx)) (Zdigits radix2 (Zpos my)) (Zdigits radix2 (Zpos mx * Zpos my)).
955
clear -Hmax.
956
unfold emin.
957 958 959 960 961 962 963 964 965 966 967 968 969 970
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.
971

972 973
Definition Bmult mult_nan m x y :=
  let f pl := B754_nan (fst pl) (snd pl) in
974
  match x, y with
975
  | B754_nan _ _, _ | _, B754_nan _ _ => f (mult_nan x y)
976 977 978
  | 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)
979 980
  | B754_infinity _, B754_zero _ => f (mult_nan x y)
  | B754_zero _, B754_infinity _ => f (mult_nan x y)
981 982 983 984 985 986 987 988
  | 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 :
989
  forall mult_nan m x y,
990
  if Rlt_bool (Rabs (round radix2 fexp (round_mode m) (B2R x * B2R y))) (bpow radix2 emax) then
991
    B2R (Bmult mult_nan m x y) = round radix2 fexp (round_mode m) (B2R x * B2R y) /\
992 993 994
    is_finite (Bmult mult_nan m x y) = andb (is_finite x) (is_finite y) /\
    (is_nan (Bmult mult_nan m x y) = false ->
      Bsign (Bmult mult_nan m x y) = xorb (Bsign x) (Bsign y))
995
  else
996
    B2FF (Bmult mult_nan m x y) = binary_overflow m (xorb (Bsign x) (Bsign y)).
997
Proof.
998
intros mult_nan m [sx|sx|sx plx|sx mx ex Hx] [sy|sy|sy ply|sy my ey Hy] ;
999
  try ( rewrite ?Rmult_0_r, ?Rmult_0_l, round_0, Rabs_R0, Rlt_bool_true ; [ now repeat constructor | apply bpow_gt_0 | now auto with typeclass_instances ] ).
1000 1001
simpl.
case Bmult_correct_aux.
1002 1003
intros H1.
case Rlt_bool.
1004
intros (H2, (H3, H4)).
1005
split.
1006
now rewrite B2R_FF2B.
1007
split.
1008
now rewrite is_finite_FF2B.
1009
rewrite Bsign_FF2B. auto.
1010
intros H2.
1011 1012 1013
now rewrite B2FF_FF2B.
Qed.

1014 1015
Definition Bmult_FF mult_nan m x y :=
  let f pl := F754_nan (fst pl) (snd pl) in
1016
  match x, y with
1017
  | F754_nan _ _, _ | _, F754_nan _ _ => f (mult_nan x y)
1018 1019 1020
  | 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)
1021 1022
  | F754_infinity _, F754_zero _ => f (mult_nan x y)
  | F754_zero _, F754_infinity _ => f (mult_nan x y)
1023 1024 1025 1026
  | 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
1027
    binary_round_aux m (xorb sx sy) (mx * my) (ex + ey) loc_Exact
1028 1029 1030
  end.

Theorem B2FF_Bmult :
1031
  forall mult_nan mult_nan_ff,