Float32.v 37.8 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require Reals.Rbasic_fun.
Require Reals.R_sqrt.
Require BuiltIn.
Require int.Int.
Require real.Real.
Require real.RealInfix.
Require real.Abs.
Require real.FromInt.
Require real.Truncate.
Require real.Square.
Require bv.Pow2int.
Require ieee_float.RoundingMode.
Require ieee_float.GenericFloat.

Guillaume Melquiond's avatar
Guillaume Melquiond committed
29 30
Import Flocq.Core.Core.
Import Flocq.IEEE754.Binary.
31 32 33 34 35 36 37 38 39 40
Import ieee_float.RoundingMode.
Import ieee_float.GenericFloat.

(* Why3 goal *)
Definition t : Type.
Proof.
  exact (t 8 24).
Defined.

(* Why3 goal *)
41
Definition t'real : t -> R.
42 43 44 45 46
Proof.
  apply B2R.
Defined.

(* Why3 goal *)
47
Definition t'isFinite : t -> Prop.
48 49 50 51 52
Proof.
  apply is_finite.
Defined.

(* Why3 goal *)
53 54
Lemma t'axiom :
  forall (x:t), (t'isFinite x) ->
Guillaume Melquiond's avatar
Guillaume Melquiond committed
55 56
  ((-340282346638528859811704183484516925440%R)%R <= (t'real x))%R /\
  ((t'real x) <= 340282346638528859811704183484516925440%R)%R.
57 58 59
Proof.
intros x _.
apply Rabs_le_inv.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
60 61
change 340282346638528859811704183484516925440%Z with (16777215 * 20282409603651670423947251286016)%Z.
rewrite mult_IZR.
62 63
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R.
destruct x as [s|s|s|s m e H] ;
Guillaume Melquiond's avatar
Guillaume Melquiond committed
64
  try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0).
65 66 67 68 69 70 71
simpl.
rewrite <- F2R_Zabs.
rewrite abs_cond_Zopp.
apply andb_prop in H.
destruct H as [H1 H2].
apply Zeq_bool_eq in H1.
apply Zle_bool_imp_le in H2.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
72
rewrite Digits.Zpos_digits2_pos in H1.
73
apply Rmult_le_compat.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
74
now apply (IZR_le 0).
75
apply bpow_ge_0.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
76
apply IZR_le.
77
apply (Z.lt_le_pred (Z.abs (Zpos m)) (Zpower radix2 24)).
Guillaume Melquiond's avatar
Guillaume Melquiond committed
78
apply Digits.Zpower_gt_Zdigits.
79
revert H1.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
80
generalize (Digits.Zdigits radix2 (Z.pos m)).
81 82 83 84 85 86
unfold FLT_exp, sb.
intros ; zify ; omega.
now apply bpow_le.
Qed.

(* Why3 goal *)
87
Definition zeroF : t.
88 89 90 91 92
Proof.
  apply zeroF.
Defined.

(* Why3 goal *)
93
Definition add : ieee_float.RoundingMode.mode -> t -> t -> t.
94 95 96 97 98
Proof.
  now apply add.
Defined.

(* Why3 goal *)
99
Definition sub : ieee_float.RoundingMode.mode -> t -> t -> t.
100 101 102 103 104
Proof.
  now apply sub.
Defined.

(* Why3 goal *)
105
Definition mul : ieee_float.RoundingMode.mode -> t -> t -> t.
106 107 108 109 110
Proof.
  now apply mul.
Defined.

(* Why3 goal *)
111
Definition div : ieee_float.RoundingMode.mode -> t -> t -> t.
112 113 114 115 116
Proof.
  now apply div.
Defined.

(* Why3 goal *)
117
Definition abs : t -> t.
118
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
119
  now apply abs.
120 121 122
Defined.

(* Why3 goal *)
123
Definition neg : t -> t.
124
Proof.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
125
  now apply neg.
126 127 128
Defined.

(* Why3 goal *)
129
Definition fma : ieee_float.RoundingMode.mode -> t -> t -> t -> t.
130 131 132 133 134
Proof.
  now apply fma.
Defined.

(* Why3 goal *)
135
Definition sqrt : ieee_float.RoundingMode.mode -> t -> t.
136 137 138 139 140
Proof.
  now apply GenericFloat.sqrt.
Defined.

(* Why3 goal *)
141
Definition roundToIntegral : ieee_float.RoundingMode.mode -> t -> t.
142 143 144 145 146
Proof.
  now apply roundToIntegral.
Defined.

(* Why3 goal *)
147
Definition min : t -> t -> t.
148 149 150 151 152
Proof.
  now apply min.
Defined.

(* Why3 goal *)
153
Definition max : t -> t -> t.
154 155 156 157 158
Proof.
  now apply max.
Defined.

(* Why3 goal *)
159
Definition le : t -> t -> Prop.
160 161 162 163 164
Proof.
  apply le.
Defined.

(* Why3 goal *)
165
Definition lt : t -> t -> Prop.
166 167 168 169 170
Proof.
  apply lt.
Defined.

(* Why3 goal *)
171
Definition eq : t -> t -> Prop.
172 173 174 175 176
Proof.
  apply eq.
Defined.

(* Why3 goal *)
177
Definition is_normal : t -> Prop.
178 179 180 181 182
Proof.
  apply is_normal.
Defined.

(* Why3 goal *)
183
Definition is_subnormal : t -> Prop.
184 185 186 187 188
Proof.
  apply is_subnormal.
Defined.

(* Why3 goal *)
189
Definition is_zero : t -> Prop.
190 191 192 193 194
Proof.
  apply is_zero.
Defined.

(* Why3 goal *)
195
Definition is_infinite : t -> Prop.
196 197 198 199 200
Proof.
  apply is_infinite.
Defined.

(* Why3 goal *)
201
Definition is_nan : t -> Prop.
202 203 204 205 206
Proof.
  apply is_nan.
Defined.

(* Why3 goal *)
207
Definition is_positive : t -> Prop.
208 209 210 211 212
Proof.
  apply is_positive.
Defined.

(* Why3 goal *)
213
Definition is_negative : t -> Prop.
214 215 216 217 218
Proof.
  apply is_negative.
Defined.

(* Why3 assumption *)
219 220
Definition is_plus_infinity (x:t) : Prop :=
  (is_infinite x) /\ (is_positive x).
221 222

(* Why3 assumption *)
223 224
Definition is_minus_infinity (x:t) : Prop :=
  (is_infinite x) /\ (is_negative x).
225 226

(* Why3 assumption *)
227
Definition is_plus_zero (x:t) : Prop := (is_zero x) /\ (is_positive x).
228 229

(* Why3 assumption *)
230
Definition is_minus_zero (x:t) : Prop := (is_zero x) /\ (is_negative x).
231 232

(* Why3 assumption *)
233
Definition is_not_nan (x:t) : Prop := (t'isFinite x) \/ (is_infinite x).
234 235

(* Why3 goal *)
236
Lemma is_not_nan1 : forall (x:t), (is_not_nan x) <-> ~ (is_nan x).
237 238 239 240 241
Proof.
  apply is_not_nan1.
Qed.

(* Why3 goal *)
242
Lemma is_not_finite :
243
  forall (x:t), ~ (t'isFinite x) <-> ((is_infinite x) \/ (is_nan x)).
244 245 246 247 248
Proof.
  apply is_not_finite.
Qed.

(* Why3 goal *)
249
Lemma zeroF_is_positive : is_positive zeroF.
250 251 252 253 254
Proof.
  apply zeroF_is_positive.
Qed.

(* Why3 goal *)
255
Lemma zeroF_is_zero : is_zero zeroF.
256 257 258 259 260
Proof.
  apply zeroF_is_zero.
Qed.

(* Why3 goal *)
261 262
Lemma zero_to_real :
  forall (x:t), (is_zero x) <-> ((t'isFinite x) /\ ((t'real x) = 0%R)).
263 264 265 266 267
Proof.
  apply zero_to_real.
Qed.

(* Why3 goal *)
268
Definition of_int : ieee_float.RoundingMode.mode -> Z -> t.
269 270 271 272 273
Proof.
  now apply z_to_fp.
Defined.

(* Why3 goal *)
274
Definition to_int : ieee_float.RoundingMode.mode -> t -> Z.
275 276 277 278 279
Proof.
  now apply fp_to_z.
Defined.

(* Why3 goal *)
280 281
Lemma zero_of_int :
  forall (m:ieee_float.RoundingMode.mode), (zeroF = (of_int m 0%Z)).
282 283 284 285 286
Proof.
  apply zero_of_int.
Qed.

(* Why3 goal *)
287
Definition round : ieee_float.RoundingMode.mode -> R -> R.
288 289 290 291 292 293 294 295 296 297 298 299 300 301
Proof.
  apply (round 8 24).
Defined.

Lemma max_real_cst :
  max_real 8 24 = (33554430 * 10141204801825835211973625643008)%R.
Proof.
  change (33554430 * 10141204801825835211973625643008)%R
    with (F2R (Float radix2 (16777215 * Zpower radix2 (104 - 103)) 103)).
  rewrite <- F2R_change_exp by easy.
  now rewrite <- max_real_is_F2R.
Qed.

(* Why3 goal *)
302
Definition max_int : Z.
303 304 305 306 307
Proof.
  exact (33554430 * 10141204801825835211973625643008)%Z.
Defined.

(* Why3 goal *)
308 309
Lemma max_real_int :
  ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
310 311
Proof.
  unfold max_int.
Guillaume Melquiond's avatar
Guillaume Melquiond committed
312
  now rewrite mult_IZR.
313 314 315
Qed.

(* Why3 assumption *)
316
Definition in_range (x:R) : Prop :=
317 318
  ((-(33554430 * 10141204801825835211973625643008)%R)%R <= x)%R /\
  (x <= (33554430 * 10141204801825835211973625643008)%R)%R.
319 320

(* Why3 assumption *)
321 322
Definition in_int_range (i:Z) : Prop :=
  ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z.
323 324

(* Why3 goal *)
325
Lemma is_finite : forall (x:t), (t'isFinite x) -> in_range (t'real x).
326 327 328 329 330 331 332 333
Proof.
  unfold t'isFinite, in_range.
  intros x Hx.
  rewrite <- max_real_cst.
  now apply is_finite1.
Qed.

(* Why3 assumption *)
334
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
335
  in_range (round m x).
336 337

(* Why3 goal *)
338
Lemma Bounded_real_no_overflow :
339 340
  forall (m:ieee_float.RoundingMode.mode) (x:R), (in_range x) ->
  no_overflow m x.
341 342 343 344 345 346 347
Proof.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply (Bounded_real_no_overflow 8 24).
Qed.

(* Why3 goal *)
348
Lemma Round_monotonic :
349 350
  forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R), (x <= y)%R ->
  ((round m x) <= (round m y))%R.
351 352 353 354 355
Proof.
  apply Round_monotonic.
Qed.

(* Why3 goal *)
356 357 358 359
Lemma Round_idempotent :
  forall (m1:ieee_float.RoundingMode.mode) (m2:ieee_float.RoundingMode.mode)
    (x:R),
  ((round m1 (round m2 x)) = (round m2 x)).
360 361 362 363 364
Proof.
  apply Round_idempotent.
Qed.

(* Why3 goal *)
365
Lemma Round_to_real :
366 367
  forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) ->
  ((round m (t'real x)) = (t'real x)).
368 369 370 371 372
Proof.
  apply Round_to_real.
Qed.

(* Why3 goal *)
373 374
Lemma Round_down_le :
  forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R.
375 376 377 378 379
Proof.
  apply Round_down_le.
Qed.

(* Why3 goal *)
380 381
Lemma Round_up_ge :
  forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R.
382 383 384 385 386
Proof.
  apply Round_up_ge.
Qed.

(* Why3 goal *)
387 388 389 390
Lemma Round_down_neg :
  forall (x:R),
  ((round ieee_float.RoundingMode.RTN (-x)%R) =
   (-(round ieee_float.RoundingMode.RTP x))%R).
391 392 393 394 395
Proof.
  apply Round_down_neg.
Qed.

(* Why3 goal *)
396 397 398 399
Lemma Round_up_neg :
  forall (x:R),
  ((round ieee_float.RoundingMode.RTP (-x)%R) =
   (-(round ieee_float.RoundingMode.RTN x))%R).
400 401 402 403 404
Proof.
  apply Round_up_neg.
Qed.

(* Why3 assumption *)
405 406
Definition in_safe_int_range (i:Z) : Prop :=
  ((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z.
407 408

(* Why3 goal *)
409
Lemma Exact_rounding_for_integers :
410 411
  forall (m:ieee_float.RoundingMode.mode) (i:Z), (in_safe_int_range i) ->
  ((round m (BuiltIn.IZR i)) = (BuiltIn.IZR i)).
412 413 414 415 416 417
Proof.
  intros m i h1.
  now apply Exact_rounding_for_integers.
Qed.

(* Why3 assumption *)
418 419 420
Definition same_sign (x:t) (y:t) : Prop :=
  ((is_positive x) /\ (is_positive y)) \/
  ((is_negative x) /\ (is_negative y)).
421 422

(* Why3 assumption *)
423 424 425
Definition diff_sign (x:t) (y:t) : Prop :=
  ((is_positive x) /\ (is_negative y)) \/
  ((is_negative x) /\ (is_positive y)).
426 427

(* Why3 goal *)
428
Lemma feq_eq :
429 430
  forall (x:t) (y:t), (t'isFinite x) -> (t'isFinite y) -> ~ (is_zero x) ->
  (eq x y) -> (x = y).
431 432 433 434 435
Proof.
  apply feq_eq.
Qed.

(* Why3 goal *)
436
Lemma eq_feq :
437
  forall (x:t) (y:t), (t'isFinite x) -> (t'isFinite y) -> (x = y) -> eq x y.
438 439 440 441 442
Proof.
  apply eq_feq.
Qed.

(* Why3 goal *)
443
Lemma eq_refl : forall (x:t), (t'isFinite x) -> eq x x.
444 445 446 447 448
Proof.
  apply eq_refl.
Qed.

(* Why3 goal *)
449
Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> eq y x.
450 451 452 453 454
Proof.
  apply eq_sym.
Qed.

(* Why3 goal *)
455
Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> (eq y z) -> eq x z.
456 457 458 459 460
Proof.
  apply eq_trans.
Qed.

(* Why3 goal *)
461
Lemma eq_zero : eq zeroF (neg zeroF).
462 463 464 465 466
Proof.
  apply eq_zero.
Qed.

(* Why3 goal *)
467
Lemma eq_to_real_finite :
468
  forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
469
  (eq x y) <-> ((t'real x) = (t'real y)).
470 471 472 473 474
Proof.
  apply eq_to_real_finite.
Qed.

(* Why3 goal *)
475 476 477 478 479 480
Lemma eq_special :
  forall (x:t) (y:t), (eq x y) ->
  (is_not_nan x) /\
  ((is_not_nan y) /\
   (((t'isFinite x) /\ (t'isFinite y)) \/
    ((is_infinite x) /\ ((is_infinite y) /\ (same_sign x y))))).
481 482 483 484 485
Proof.
  apply eq_special.
Qed.

(* Why3 goal *)
486
Lemma lt_finite :
487
  forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
488
  (lt x y) <-> ((t'real x) < (t'real y))%R.
489 490 491 492 493
Proof.
  apply lt_finite.
Qed.

(* Why3 goal *)
494
Lemma le_finite :
495
  forall (x:t) (y:t), ((t'isFinite x) /\ (t'isFinite y)) ->
496
  (le x y) <-> ((t'real x) <= (t'real y))%R.
497 498 499 500 501
Proof.
  apply le_finite.
Qed.

(* Why3 goal *)
502
Lemma le_lt_trans :
503
  forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> lt x z.
504 505 506 507 508
Proof.
  apply le_lt_trans.
Qed.

(* Why3 goal *)
509
Lemma lt_le_trans :
510
  forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> lt x z.
511 512 513 514 515
Proof.
  apply lt_le_trans.
Qed.

(* Why3 goal *)
516
Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> eq x y.
517 518 519 520 521
Proof.
  apply le_ge_asym.
Qed.

(* Why3 goal *)
522
Lemma not_lt_ge :
523 524
  forall (x:t) (y:t), (~ (lt x y) /\ ((is_not_nan x) /\ (is_not_nan y))) ->
  le y x.
525 526 527 528 529
Proof.
  apply not_lt_ge.
Qed.

(* Why3 goal *)
530
Lemma not_gt_le :
531 532
  forall (x:t) (y:t), (~ (lt y x) /\ ((is_not_nan x) /\ (is_not_nan y))) ->
  le x y.
533 534 535 536 537
Proof.
 apply not_gt_le.
Qed.

(* Why3 goal *)
538 539 540 541 542
Lemma le_special :
  forall (x:t) (y:t), (le x y) ->
  ((t'isFinite x) /\ (t'isFinite y)) \/
  (((is_minus_infinity x) /\ (is_not_nan y)) \/
   ((is_not_nan x) /\ (is_plus_infinity y))).
543 544 545 546 547
Proof.
  apply le_special.
Qed.

(* Why3 goal *)
548 549 550 551 552
Lemma lt_special :
  forall (x:t) (y:t), (lt x y) ->
  ((t'isFinite x) /\ (t'isFinite y)) \/
  (((is_minus_infinity x) /\ ((is_not_nan y) /\ ~ (is_minus_infinity y))) \/
   ((is_not_nan x) /\ (~ (is_plus_infinity x) /\ (is_plus_infinity y)))).
553 554 555 556 557
Proof.
  apply lt_special.
Qed.

(* Why3 goal *)
558
Lemma lt_lt_finite :
559
  forall (x:t) (y:t) (z:t), (lt x y) -> (lt y z) -> t'isFinite y.
560 561 562 563 564
Proof.
  apply lt_lt_finite.
Qed.

(* Why3 goal *)
565
Lemma positive_to_real :
566
  forall (x:t), (t'isFinite x) -> (is_positive x) -> (0%R <= (t'real x))%R.
567 568 569 570 571
Proof.
  apply positive_to_real.
Qed.

(* Why3 goal *)
572
Lemma to_real_positive :
573
  forall (x:t), (t'isFinite x) -> (0%R < (t'real x))%R -> is_positive x.
574 575 576 577 578
Proof.
  apply to_real_positive.
Qed.

(* Why3 goal *)
579
Lemma negative_to_real :
580
  forall (x:t), (t'isFinite x) -> (is_negative x) -> ((t'real x) <= 0%R)%R.
581 582 583 584 585
Proof.
  apply negative_to_real.
Qed.

(* Why3 goal *)
586
Lemma to_real_negative :
587
  forall (x:t), (t'isFinite x) -> ((t'real x) < 0%R)%R -> is_negative x.
588 589 590 591 592
Proof.
  apply to_real_negative.
Qed.

(* Why3 goal *)
593 594
Lemma negative_xor_positive :
  forall (x:t), ~ ((is_positive x) /\ (is_negative x)).
595 596 597 598 599
Proof.
  apply negative_xor_positive.
Qed.

(* Why3 goal *)
600
Lemma negative_or_positive :
601
  forall (x:t), (is_not_nan x) -> (is_positive x) \/ (is_negative x).
602 603 604 605 606
Proof.
  apply negative_or_positive.
Qed.

(* Why3 goal *)
607
Lemma diff_sign_trans :
608 609
  forall (x:t) (y:t) (z:t), ((diff_sign x y) /\ (diff_sign y z)) ->
  same_sign x z.
610 611 612 613 614
Proof.
  apply diff_sign_trans.
Qed.

(* Why3 goal *)
615 616 617 618 619
Lemma diff_sign_product :
  forall (x:t) (y:t),
  ((t'isFinite x) /\
   ((t'isFinite y) /\ (((t'real x) * (t'real y))%R < 0%R)%R)) ->
  diff_sign x y.
620 621 622 623 624
Proof.
  apply diff_sign_product.
Qed.

(* Why3 goal *)
625 626 627 628
Lemma same_sign_product :
  forall (x:t) (y:t),
  ((t'isFinite x) /\ ((t'isFinite y) /\ (same_sign x y))) ->
  (0%R <= ((t'real x) * (t'real y))%R)%R.
629 630 631 632 633
Proof.
  apply same_sign_product.
Qed.

(* Why3 assumption *)
634
Definition product_sign (z:t) (x:t) (y:t) : Prop :=
635
  ((same_sign x y) -> is_positive z) /\ ((diff_sign x y) -> is_negative z).
636 637

(* Why3 assumption *)
638
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
639
  match m with
640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656
  | ieee_float.RoundingMode.RTN =>
      ((is_positive x) ->
       (t'isFinite x) /\
       ((t'real x) = (33554430 * 10141204801825835211973625643008)%R)) /\
      (~ (is_positive x) -> is_infinite x)
  | ieee_float.RoundingMode.RTP =>
      ((is_positive x) -> is_infinite x) /\
      (~ (is_positive x) ->
       (t'isFinite x) /\
       ((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R))
  | ieee_float.RoundingMode.RTZ =>
      ((is_positive x) ->
       (t'isFinite x) /\
       ((t'real x) = (33554430 * 10141204801825835211973625643008)%R)) /\
      (~ (is_positive x) ->
       (t'isFinite x) /\
       ((t'real x) = (-(33554430 * 10141204801825835211973625643008)%R)%R))
657
  | ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE => is_infinite x
658 659 660
  end.

(* Why3 assumption *)
661
Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
662 663
  (is_zero x) ->
  match m with
664 665
  | ieee_float.RoundingMode.RTN => is_negative x
  | _ => is_positive x
666 667 668
  end.

(* Why3 goal *)
669 670 671 672 673
Lemma add_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) ->
  (t'isFinite y) -> (no_overflow m ((t'real x) + (t'real y))%R) ->
  (t'isFinite (add m x y)) /\
  ((t'real (add m x y)) = (round m ((t'real x) + (t'real y))%R)).
674 675 676 677 678 679 680 681
Proof.
  intros m x y h1 h2 h3.
  apply add_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
682 683
Lemma add_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
684
  (t'isFinite (add m x y)) -> (t'isFinite x) /\ (t'isFinite y).
685 686 687 688 689
Proof.
  apply add_finite_rev.
Qed.

(* Why3 goal *)
690 691 692 693 694
Lemma add_finite_rev_n :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> (t'isFinite (add m x y)) ->
  (no_overflow m ((t'real x) + (t'real y))%R) /\
  ((t'real (add m x y)) = (round m ((t'real x) + (t'real y))%R)).
695 696 697 698 699 700 701 702
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply add_finite_rev_n.
Qed.

(* Why3 goal *)
703 704 705 706 707
Lemma sub_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) ->
  (t'isFinite y) -> (no_overflow m ((t'real x) - (t'real y))%R) ->
  (t'isFinite (sub m x y)) /\
  ((t'real (sub m x y)) = (round m ((t'real x) - (t'real y))%R)).
708 709 710 711 712 713 714 715
Proof.
  intros m x y h1 h2 h3.
  apply sub_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
716 717
Lemma sub_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
718
  (t'isFinite (sub m x y)) -> (t'isFinite x) /\ (t'isFinite y).
719 720 721 722 723
Proof.
  apply sub_finite_rev.
Qed.

(* Why3 goal *)
724 725 726 727 728
Lemma sub_finite_rev_n :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> (t'isFinite (sub m x y)) ->
  (no_overflow m ((t'real x) - (t'real y))%R) /\
  ((t'real (sub m x y)) = (round m ((t'real x) - (t'real y))%R)).
729 730 731 732 733 734 735 736
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply sub_finite_rev_n.
Qed.

(* Why3 goal *)
737 738 739 740 741
Lemma mul_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) ->
  (t'isFinite y) -> (no_overflow m ((t'real x) * (t'real y))%R) ->
  (t'isFinite (mul m x y)) /\
  ((t'real (mul m x y)) = (round m ((t'real x) * (t'real y))%R)).
742 743 744 745 746 747 748 749
Proof.
  intros m x y h1 h2 h3.
  apply mul_finite ; try easy.
  unfold no_overflow, in_range in h3.
  now rewrite <- max_real_cst in h3.
Qed.

(* Why3 goal *)
750 751
Lemma mul_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
752
  (t'isFinite (mul m x y)) -> (t'isFinite x) /\ (t'isFinite y).
753 754 755 756 757
Proof.
  apply mul_finite_rev.
Qed.

(* Why3 goal *)
758 759 760 761 762
Lemma mul_finite_rev_n :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> (t'isFinite (mul m x y)) ->
  (no_overflow m ((t'real x) * (t'real y))%R) /\
  ((t'real (mul m x y)) = (round m ((t'real x) * (t'real y))%R)).
763 764 765 766 767 768 769 770
Proof.
  intros m x y h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply mul_finite_rev_n.
Qed.

(* Why3 goal *)
771 772 773 774 775 776
Lemma div_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t), (t'isFinite x) ->
  (t'isFinite y) -> ~ (is_zero y) ->
  (no_overflow m ((t'real x) / (t'real y))%R) ->
  (t'isFinite (div m x y)) /\
  ((t'real (div m x y)) = (round m ((t'real x) / (t'real y))%R)).
777 778 779 780 781 782 783 784
Proof.
  intros m x y h1 h2 h3 h4.
  apply div_finite ; try easy.
  unfold no_overflow, in_range in h4.
  now rewrite <- max_real_cst in h4.
Qed.

(* Why3 goal *)
785 786 787
Lemma div_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (div m x y)) ->
788 789
  ((t'isFinite x) /\ ((t'isFinite y) /\ ~ (is_zero y))) \/
  ((t'isFinite x) /\ ((is_infinite y) /\ ((t'real (div m x y)) = 0%R))).
790 791 792 793 794
Proof.
  apply div_finite_rev.
Qed.

(* Why3 goal *)
795 796 797 798 799 800
Lemma div_finite_rev_n :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (ieee_float.RoundingMode.to_nearest m) -> (t'isFinite (div m x y)) ->
  (t'isFinite y) ->
  (no_overflow m ((t'real x) / (t'real y))%R) /\
  ((t'real (div m x y)) = (round m ((t'real x) / (t'real y))%R)).
801 802 803 804 805 806 807 808
Proof.
  intros m x y h1 h2 h3.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply div_finite_rev_n.
Qed.

(* Why3 goal *)
809
Lemma neg_finite :
810
  forall (x:t), (t'isFinite x) ->
811
  (t'isFinite (neg x)) /\ ((t'real (neg x)) = (-(t'real x))%R).
812 813 814 815 816
Proof.
  apply neg_finite.
Qed.

(* Why3 goal *)
817
Lemma neg_finite_rev :
818
  forall (x:t), (t'isFinite (neg x)) ->
819
  (t'isFinite x) /\ ((t'real (neg x)) = (-(t'real x))%R).
820 821 822 823 824
Proof.
  apply neg_finite_rev.
Qed.

(* Why3 goal *)
825 826 827 828 829
Lemma abs_finite :
  forall (x:t), (t'isFinite x) ->
  (t'isFinite (abs x)) /\
  (((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x))) /\
   (is_positive (abs x))).
830 831 832 833 834
Proof.
  apply abs_finite.
Qed.

(* Why3 goal *)
835
Lemma abs_finite_rev :
836
  forall (x:t), (t'isFinite (abs x)) ->
837
  (t'isFinite x) /\ ((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x))).
838 839 840 841 842
Proof.
  apply abs_finite_rev.
Qed.

(* Why3 goal *)
843
Lemma abs_universal : forall (x:t), ~ (is_negative (abs x)).
844 845 846 847 848
Proof.
  apply abs_universal.
Qed.

(* Why3 goal *)
849 850 851 852 853 854 855
Lemma fma_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (t'isFinite x) -> (t'isFinite y) -> (t'isFinite z) ->
  (no_overflow m (((t'real x) * (t'real y))%R + (t'real z))%R) ->
  (t'isFinite (fma m x y z)) /\
  ((t'real (fma m x y z)) =
   (round m (((t'real x) * (t'real y))%R + (t'real z))%R)).
856 857 858 859 860 861 862 863
Proof.
  intros m x y z h1 h2 h3 h4.
  apply fma_finite ; try easy.
  unfold no_overflow, in_range in h4.
  now rewrite <- max_real_cst in h4.
Qed.

(* Why3 goal *)
864 865 866
Lemma fma_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (t'isFinite (fma m x y z)) ->
867
  (t'isFinite x) /\ ((t'isFinite y) /\ (t'isFinite z)).
868 869 870 871 872
Proof.
  apply fma_finite_rev.
Qed.

(* Why3 goal *)
873 874 875 876 877 878
Lemma fma_finite_rev_n :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (ieee_float.RoundingMode.to_nearest m) -> (t'isFinite (fma m x y z)) ->
  (no_overflow m (((t'real x) * (t'real y))%R + (t'real z))%R) /\
  ((t'real (fma m x y z)) =
   (round m (((t'real x) * (t'real y))%R + (t'real z))%R)).
879 880 881 882 883 884 885 886
Proof.
  intros m x y z h1 h2.
  unfold no_overflow, in_range.
  rewrite <- max_real_cst.
  now apply fma_finite_rev_n.
Qed.

(* Why3 goal *)
887 888 889 890 891
Lemma sqrt_finite :
  forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite x) ->
  (0%R <= (t'real x))%R ->
  (t'isFinite (sqrt m x)) /\
  ((t'real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (t'real x)))).
892 893 894 895 896
Proof.
  apply sqrt_finite.
Qed.

(* Why3 goal *)
897 898 899 900 901
Lemma sqrt_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t), (t'isFinite (sqrt m x)) ->
  (t'isFinite x) /\
  ((0%R <= (t'real x))%R /\
   ((t'real (sqrt m x)) = (round m (Reals.R_sqrt.sqrt (t'real x))))).
902 903 904 905 906
Proof.
  apply sqrt_finite_rev.
Qed.

(* Why3 assumption *)
907 908
Definition same_sign_real (x:t) (r:R) : Prop :=
  ((is_positive x) /\ (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R).
909 910

(* Why3 goal *)
911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928
Lemma add_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := add m x y in
  (((is_nan x) \/ (is_nan y)) -> is_nan r) /\
  ((((t'isFinite x) /\ (is_infinite y)) ->
    (is_infinite r) /\ (same_sign r y)) /\
   ((((is_infinite x) /\ (t'isFinite y)) ->
     (is_infinite r) /\ (same_sign r x)) /\
    ((((is_infinite x) /\ ((is_infinite y) /\ (same_sign x y))) ->
      (is_infinite r) /\ (same_sign r x)) /\
     ((((is_infinite x) /\ ((is_infinite y) /\ (diff_sign x y))) -> is_nan r) /\
      ((((t'isFinite x) /\
         ((t'isFinite y) /\ ~ (no_overflow m ((t'real x) + (t'real y))%R))) ->
        (same_sign_real r ((t'real x) + (t'real y))%R) /\
        (overflow_value m r)) /\
       (((t'isFinite x) /\ (t'isFinite y)) ->
        ((same_sign x y) -> same_sign r x) /\
        (~ (same_sign x y) -> sign_zero_result m r))))))).
929 930 931 932 933 934 935 936
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply add_special.
Qed.

(* Why3 goal *)
937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954
Lemma sub_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := sub m x y in
  (((is_nan x) \/ (is_nan y)) -> is_nan r) /\
  ((((t'isFinite x) /\ (is_infinite y)) ->
    (is_infinite r) /\ (diff_sign r y)) /\
   ((((is_infinite x) /\ (t'isFinite y)) ->
     (is_infinite r) /\ (same_sign r x)) /\
    ((((is_infinite x) /\ ((is_infinite y) /\ (same_sign x y))) -> is_nan r) /\
     ((((is_infinite x) /\ ((is_infinite y) /\ (diff_sign x y))) ->
       (is_infinite r) /\ (same_sign r x)) /\
      ((((t'isFinite x) /\
         ((t'isFinite y) /\ ~ (no_overflow m ((t'real x) - (t'real y))%R))) ->
        (same_sign_real r ((t'real x) - (t'real y))%R) /\
        (overflow_value m r)) /\
       (((t'isFinite x) /\ (t'isFinite y)) ->
        ((diff_sign x y) -> same_sign r x) /\
        (~ (diff_sign x y) -> sign_zero_result m r))))))).
955 956 957 958 959 960 961 962
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply sub_special.
Qed.

(* Why3 goal *)
963 964 965 966 967 968 969 970 971 972 973 974 975 976
Lemma mul_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := mul m x y in
  (((is_nan x) \/ (is_nan y)) -> is_nan r) /\
  ((((is_zero x) /\ (is_infinite y)) -> is_nan r) /\
   ((((t'isFinite x) /\ ((is_infinite y) /\ ~ (is_zero x))) -> is_infinite r) /\
    ((((is_infinite x) /\ (is_zero y)) -> is_nan r) /\
     ((((is_infinite x) /\ ((t'isFinite y) /\ ~ (is_zero y))) ->
       is_infinite r) /\
      ((((is_infinite x) /\ (is_infinite y)) -> is_infinite r) /\
       ((((t'isFinite x) /\
          ((t'isFinite y) /\ ~ (no_overflow m ((t'real x) * (t'real y))%R))) ->
         overflow_value m r) /\
        (~ (is_nan r) -> product_sign r x y))))))).
977 978 979 980 981 982 983 984
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply mul_special.
Qed.

(* Why3 goal *)
985 986 987 988 989 990 991 992 993 994 995 996 997 998
Lemma div_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  let r := div m x y in
  (((is_nan x) \/ (is_nan y)) -> is_nan r) /\
  ((((t'isFinite x) /\ (is_infinite y)) -> is_zero r) /\
   ((((is_infinite x) /\ (t'isFinite y)) -> is_infinite r) /\
    ((((is_infinite x) /\ (is_infinite y)) -> is_nan r) /\
     ((((t'isFinite x) /\
        ((t'isFinite y) /\
         (~ (is_zero y) /\ ~ (no_overflow m ((t'real x) / (t'real y))%R)))) ->
       overflow_value m r) /\
      ((((t'isFinite x) /\ ((is_zero y) /\ ~ (is_zero x))) -> is_infinite r) /\
       ((((is_zero x) /\ (is_zero y)) -> is_nan r) /\
        (~ (is_nan r) -> product_sign r x y))))))).
999 1000 1001 1002 1003 1004 1005 1006
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply div_special.
Qed.

(* Why3 goal *)
1007 1008
Lemma neg_special :
  forall (x:t),
1009 1010 1011
  ((is_nan x) -> is_nan (neg x)) /\
  (((is_infinite x) -> is_infinite (neg x)) /\
   (~ (is_nan x) -> diff_sign x (neg x))).
1012 1013 1014 1015 1016
Proof.
  apply neg_special.
Qed.

(* Why3 goal *)
1017 1018
Lemma abs_special :
  forall (x:t),
1019 1020 1021
  ((is_nan x) -> is_nan (abs x)) /\
  (((is_infinite x) -> is_infinite (abs x)) /\
   (~ (is_nan x) -> is_positive (abs x))).
1022 1023 1024 1025 1026
Proof.
  apply abs_special.
Qed.

(* Why3 goal *)
1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066
Lemma fma_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  let r := fma m x y z in
  (((is_nan x) \/ ((is_nan y) \/ (is_nan z))) -> is_nan r) /\
  ((((is_zero x) /\ (is_infinite y)) -> is_nan r) /\
   ((((is_infinite x) /\ (is_zero y)) -> is_nan r) /\
    ((((t'isFinite x) /\
       (~ (is_zero x) /\ ((is_infinite y) /\ (t'isFinite z)))) ->
      (is_infinite r) /\ (product_sign r x y)) /\
     ((((t'isFinite x) /\
        (~ (is_zero x) /\ ((is_infinite y) /\ (is_infinite z)))) ->
       ((product_sign z x y) -> (is_infinite r) /\ (same_sign r z)) /\
       (~ (product_sign z x y) -> is_nan r)) /\
      ((((is_infinite x) /\
         ((t'isFinite y) /\ (~ (is_zero y) /\ (t'isFinite z)))) ->
        (is_infinite r) /\ (product_sign r x y)) /\
       ((((is_infinite x) /\
          ((t'isFinite y) /\ (~ (is_zero y) /\ (is_infinite z)))) ->
         ((product_sign z x y) -> (is_infinite r) /\ (same_sign r z)) /\
         (~ (product_sign z x y) -> is_nan r)) /\
        ((((is_infinite x) /\ ((is_infinite y) /\ (t'isFinite z))) ->
          (is_infinite r) /\ (product_sign r x y)) /\
         ((((t'isFinite x) /\ ((t'isFinite y) /\ (is_infinite z))) ->
           (is_infinite r) /\ (same_sign r z)) /\
          ((((is_infinite x) /\ ((is_infinite y) /\ (is_infinite z))) ->
            ((product_sign z x y) -> (is_infinite r) /\ (same_sign r z)) /\
            (~ (product_sign z x y) -> is_nan r)) /\
           ((((t'isFinite x) /\
              ((t'isFinite y) /\
               ((t'isFinite z) /\
                ~ (no_overflow m
                   (((t'real x) * (t'real y))%R + (t'real z))%R)))) ->
             (same_sign_real r (((t'real x) * (t'real y))%R + (t'real z))%R) /\
             (overflow_value m r)) /\
            (((t'isFinite x) /\ ((t'isFinite y) /\ (t'isFinite z))) ->
             ((product_sign z x y) -> same_sign r z) /\
             (~ (product_sign z x y) ->
              ((((t'real x) * (t'real y))%R + (t'real z))%R = 0%R) ->
              ((m = ieee_float.RoundingMode.RTN) -> is_negative r) /\
              (~ (m = ieee_float.RoundingMode.RTN) -> is_positive r))))))))))))).
1067 1068 1069 1070 1071 1072 1073 1074
Proof.
  intros m x y z r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply fma_special.
Qed.

(* Why3 goal *)
1075 1076 1077 1078 1079 1080 1081 1082 1083
Lemma sqrt_special :
  forall (m:ieee_float.RoundingMode.mode) (x:t),
  let r := sqrt m x in
  ((is_nan x) -> is_nan r) /\
  (((is_plus_infinity x) -> is_plus_infinity r) /\
   (((is_minus_infinity x) -> is_nan r) /\
    ((((t'isFinite x) /\ ((t'real x) < 0%R)%R) -> is_nan r) /\
     (((is_zero x) -> same_sign r x) /\
      (((t'isFinite x) /\ (0%R < (t'real x))%R) -> is_positive r))))).
1084 1085 1086 1087 1088
Proof.
  apply sqrt_special.
Qed.

(* Why3 goal *)
1089 1090 1091 1092 1093 1094
Lemma of_int_add_exact :
  forall (m:ieee_float.RoundingMode.mode) (n:ieee_float.RoundingMode.mode)
    (i:Z) (j:Z),
  (in_safe_int_range i) -> (in_safe_int_range j) ->
  (in_safe_int_range (i + j)%Z) ->
  eq (of_int m (i + j)%Z) (add n (of_int m i) (of_int m j)).
1095 1096 1097 1098 1099