Float32.v 37.3 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 29 30 31 32 33 34 35 36 37 38 39 40
(*                                                                  *)
(*  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.

Import Flocq.Core.Fcore.
Import Flocq.Appli.Fappli_IEEE.
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 55
Lemma t'axiom : forall (x:t), (t'isFinite x) ->
  (((-(16777215 * 20282409603651670423947251286016)%R)%R <= (t'real x))%R /\
  ((t'real x) <= (16777215 * 20282409603651670423947251286016)%R)%R).
56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
Proof.
intros x _.
apply Rabs_le_inv.
change (Rabs (B2R _ _ x) <= F2R (Float radix2 (Zpower radix2 24 - 1) (127 - 23)))%R.
destruct x as [s|s|s|s m e H] ;
  try (simpl ; rewrite Rabs_R0 ; now apply F2R_ge_0_compat).
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.
rewrite Fcore_digits.Zpos_digits2_pos in H1.
apply Rmult_le_compat.
now apply (Z2R_le 0).
apply bpow_ge_0.
apply Z2R_le.
apply (Z.lt_le_pred (Zabs (Zpos m)) (Zpower radix2 24)).
apply Fcore_digits.Zpower_gt_Zdigits.
revert H1.
generalize (Fcore_digits.Zdigits radix2 (Z.pos m)).
unfold FLT_exp, sb.
intros ; zify ; omega.
now apply bpow_le.
Qed.

(* Why3 goal *)
84
Definition zeroF : t.
85 86 87 88 89
Proof.
  apply zeroF.
Defined.

(* Why3 goal *)
90
Definition add : ieee_float.RoundingMode.mode -> t -> t -> t.
91 92 93 94 95
Proof.
  now apply add.
Defined.

(* Why3 goal *)
96
Definition sub : ieee_float.RoundingMode.mode -> t -> t -> t.
97 98 99 100 101
Proof.
  now apply sub.
Defined.

(* Why3 goal *)
102
Definition mul : ieee_float.RoundingMode.mode -> t -> t -> t.
103 104 105 106 107
Proof.
  now apply mul.
Defined.

(* Why3 goal *)
108
Definition div : ieee_float.RoundingMode.mode -> t -> t -> t.
109 110 111 112 113
Proof.
  now apply div.
Defined.

(* Why3 goal *)
114
Definition abs : t -> t.
115 116 117 118 119
Proof.
  apply abs.
Defined.

(* Why3 goal *)
120
Definition neg : t -> t.
121 122 123 124 125
Proof.
  apply neg.
Defined.

(* Why3 goal *)
126
Definition fma : ieee_float.RoundingMode.mode -> t -> t -> t -> t.
127 128 129 130 131
Proof.
  now apply fma.
Defined.

(* Why3 goal *)
132
Definition sqrt : ieee_float.RoundingMode.mode -> t -> t.
133 134 135 136 137
Proof.
  now apply GenericFloat.sqrt.
Defined.

(* Why3 goal *)
138
Definition roundToIntegral : ieee_float.RoundingMode.mode -> t -> t.
139 140 141 142 143
Proof.
  now apply roundToIntegral.
Defined.

(* Why3 goal *)
144
Definition min : t -> t -> t.
145 146 147 148 149
Proof.
  now apply min.
Defined.

(* Why3 goal *)
150
Definition max : t -> t -> t.
151 152 153 154 155
Proof.
  now apply max.
Defined.

(* Why3 goal *)
156
Definition le : t -> t -> Prop.
157 158 159 160 161
Proof.
  apply le.
Defined.

(* Why3 goal *)
162
Definition lt : t -> t -> Prop.
163 164 165 166 167
Proof.
  apply lt.
Defined.

(* Why3 goal *)
168
Definition eq : t -> t -> Prop.
169 170 171 172 173
Proof.
  apply eq.
Defined.

(* Why3 goal *)
174
Definition is_normal : t -> Prop.
175 176 177 178 179
Proof.
  apply is_normal.
Defined.

(* Why3 goal *)
180
Definition is_subnormal : t -> Prop.
181 182 183 184 185
Proof.
  apply is_subnormal.
Defined.

(* Why3 goal *)
186
Definition is_zero : t -> Prop.
187 188 189 190 191
Proof.
  apply is_zero.
Defined.

(* Why3 goal *)
192
Definition is_infinite : t -> Prop.
193 194 195 196 197
Proof.
  apply is_infinite.
Defined.

(* Why3 goal *)
198
Definition is_nan : t -> Prop.
199 200 201 202 203
Proof.
  apply is_nan.
Defined.

(* Why3 goal *)
204
Definition is_positive : t -> Prop.
205 206 207 208 209
Proof.
  apply is_positive.
Defined.

(* Why3 goal *)
210
Definition is_negative : t -> Prop.
211 212 213 214 215
Proof.
  apply is_negative.
Defined.

(* Why3 assumption *)
216 217
Definition is_plus_infinity (x:t) : Prop :=
  (is_infinite x) /\ (is_positive x).
218 219

(* Why3 assumption *)
220 221
Definition is_minus_infinity (x:t) : Prop :=
  (is_infinite x) /\ (is_negative x).
222 223

(* Why3 assumption *)
224
Definition is_plus_zero (x:t) : Prop := (is_zero x) /\ (is_positive x).
225 226

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

(* Why3 assumption *)
230
Definition is_not_nan (x:t) : Prop := (t'isFinite x) \/ (is_infinite x).
231 232

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

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

(* Why3 goal *)
246
Lemma zeroF_is_positive : is_positive zeroF.
247 248 249 250 251
Proof.
  apply zeroF_is_positive.
Qed.

(* Why3 goal *)
252
Lemma zeroF_is_zero : is_zero zeroF.
253 254 255 256 257
Proof.
  apply zeroF_is_zero.
Qed.

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

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

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

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

(* Why3 goal *)
284
Definition round : ieee_float.RoundingMode.mode -> R -> R.
285 286 287 288 289 290 291 292 293 294 295 296 297 298
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 *)
299
Definition max_int : Z.
300 301 302 303 304
Proof.
  exact (33554430 * 10141204801825835211973625643008)%Z.
Defined.

(* Why3 goal *)
305 306
Lemma max_real_int :
  ((33554430 * 10141204801825835211973625643008)%R = (BuiltIn.IZR max_int)).
307 308 309 310 311 312
Proof.
  unfold max_int.
  now rewrite mult_IZR, <- !Z2R_IZR.
Qed.

(* Why3 assumption *)
313
Definition in_range (x:R) : Prop :=
314 315
  ((-(33554430 * 10141204801825835211973625643008)%R)%R <= x)%R /\
  (x <= (33554430 * 10141204801825835211973625643008)%R)%R.
316 317

(* Why3 assumption *)
318 319
Definition in_int_range (i:Z) : Prop :=
  ((-max_int)%Z <= i)%Z /\ (i <= max_int)%Z.
320 321

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

(* Why3 assumption *)
331
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R) : Prop :=
332
  in_range (round m x).
333 334

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

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

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

(* Why3 goal *)
361 362
Lemma Round_to_real :
  forall (m:ieee_float.RoundingMode.mode) (x:t),
363
  (t'isFinite x) -> ((round m (t'real x)) = (t'real x)).
364 365 366 367 368
Proof.
  apply Round_to_real.
Qed.

(* Why3 goal *)
369 370
Lemma Round_down_le :
  forall (x:R), ((round ieee_float.RoundingMode.RTN x) <= x)%R.
371 372 373 374 375
Proof.
  apply Round_down_le.
Qed.

(* Why3 goal *)
376 377
Lemma Round_up_ge :
  forall (x:R), (x <= (round ieee_float.RoundingMode.RTP x))%R.
378 379 380 381 382
Proof.
  apply Round_up_ge.
Qed.

(* Why3 goal *)
383 384 385 386
Lemma Round_down_neg :
  forall (x:R),
  ((round ieee_float.RoundingMode.RTN (-x)%R) =
   (-(round ieee_float.RoundingMode.RTP x))%R).
387 388 389 390 391
Proof.
  apply Round_down_neg.
Qed.

(* Why3 goal *)
392 393 394 395
Lemma Round_up_neg :
  forall (x:R),
  ((round ieee_float.RoundingMode.RTP (-x)%R) =
   (-(round ieee_float.RoundingMode.RTN x))%R).
396 397 398 399 400
Proof.
  apply Round_up_neg.
Qed.

(* Why3 assumption *)
401 402
Definition in_safe_int_range (i:Z) : Prop :=
  ((-16777216%Z)%Z <= i)%Z /\ (i <= 16777216%Z)%Z.
403 404

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

(* Why3 assumption *)
414 415 416
Definition same_sign (x:t) (y:t) : Prop :=
  ((is_positive x) /\ (is_positive y)) \/
  ((is_negative x) /\ (is_negative y)).
417 418

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

(* Why3 goal *)
424 425 426
Lemma feq_eq :
  forall (x:t) (y:t),
  (t'isFinite x) -> (t'isFinite y) -> ~ (is_zero x) -> (eq x y) -> (x = y).
427 428 429 430 431
Proof.
  apply feq_eq.
Qed.

(* Why3 goal *)
432
Lemma eq_feq :
433
  forall (x:t) (y:t), (t'isFinite x) -> (t'isFinite y) -> (x = y) -> eq x y.
434 435 436 437 438
Proof.
  apply eq_feq.
Qed.

(* Why3 goal *)
439
Lemma eq_refl : forall (x:t), (t'isFinite x) -> eq x x.
440 441 442 443 444
Proof.
  apply eq_refl.
Qed.

(* Why3 goal *)
445
Lemma eq_sym : forall (x:t) (y:t), (eq x y) -> eq y x.
446 447 448 449 450
Proof.
  apply eq_sym.
Qed.

(* Why3 goal *)
451
Lemma eq_trans : forall (x:t) (y:t) (z:t), (eq x y) -> (eq y z) -> eq x z.
452 453 454 455 456
Proof.
  apply eq_trans.
Qed.

(* Why3 goal *)
457
Lemma eq_zero : eq zeroF (neg zeroF).
458 459 460 461 462
Proof.
  apply eq_zero.
Qed.

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

(* Why3 goal *)
472 473 474
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)))))).
475 476 477 478 479
Proof.
  apply eq_special.
Qed.

(* Why3 goal *)
480 481 482
Lemma lt_finite :
  forall (x:t) (y:t),
  ((t'isFinite x) /\ (t'isFinite y)) ->
483
  (lt x y) <-> ((t'real x) < (t'real y))%R.
484 485 486 487 488
Proof.
  apply lt_finite.
Qed.

(* Why3 goal *)
489 490 491
Lemma le_finite :
  forall (x:t) (y:t),
  ((t'isFinite x) /\ (t'isFinite y)) ->
492
  (le x y) <-> ((t'real x) <= (t'real y))%R.
493 494 495 496 497
Proof.
  apply le_finite.
Qed.

(* Why3 goal *)
498
Lemma le_lt_trans :
499
  forall (x:t) (y:t) (z:t), ((le x y) /\ (lt y z)) -> lt x z.
500 501 502 503 504
Proof.
  apply le_lt_trans.
Qed.

(* Why3 goal *)
505
Lemma lt_le_trans :
506
  forall (x:t) (y:t) (z:t), ((lt x y) /\ (le y z)) -> lt x z.
507 508 509 510 511
Proof.
  apply lt_le_trans.
Qed.

(* Why3 goal *)
512
Lemma le_ge_asym : forall (x:t) (y:t), ((le x y) /\ (le y x)) -> eq x y.
513 514 515 516 517
Proof.
  apply le_ge_asym.
Qed.

(* Why3 goal *)
518 519
Lemma not_lt_ge :
  forall (x:t) (y:t),
520
  (~ (lt x y) /\ ((is_not_nan x) /\ (is_not_nan y))) -> le y x.
521 522 523 524 525
Proof.
  apply not_lt_ge.
Qed.

(* Why3 goal *)
526 527
Lemma not_gt_le :
  forall (x:t) (y:t),
528
  (~ (lt y x) /\ ((is_not_nan x) /\ (is_not_nan y))) -> le x y.
529 530 531 532 533
Proof.
 apply not_gt_le.
Qed.

(* Why3 goal *)
534 535 536
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)))).
537 538 539 540 541
Proof.
  apply le_special.
Qed.

(* Why3 goal *)
542 543 544 545
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))))).
546 547 548 549 550
Proof.
  apply lt_special.
Qed.

(* Why3 goal *)
551
Lemma lt_lt_finite :
552
  forall (x:t) (y:t) (z:t), (lt x y) -> (lt y z) -> t'isFinite y.
553 554 555 556 557
Proof.
  apply lt_lt_finite.
Qed.

(* Why3 goal *)
558
Lemma positive_to_real :
559
  forall (x:t), (t'isFinite x) -> (is_positive x) -> (0%R <= (t'real x))%R.
560 561 562 563 564
Proof.
  apply positive_to_real.
Qed.

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

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

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

(* Why3 goal *)
586 587
Lemma negative_xor_positive :
  forall (x:t), ~ ((is_positive x) /\ (is_negative x)).
588 589 590 591 592
Proof.
  apply negative_xor_positive.
Qed.

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

(* Why3 goal *)
600 601
Lemma diff_sign_trans :
  forall (x:t) (y:t) (z:t),
602
  ((diff_sign x y) /\ (diff_sign y z)) -> same_sign x z.
603 604 605 606 607
Proof.
  apply diff_sign_trans.
Qed.

(* Why3 goal *)
608 609
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).
610 611 612 613 614
Proof.
  apply diff_sign_product.
Qed.

(* Why3 goal *)
615 616 617 618
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.
619 620 621 622 623
Proof.
  apply same_sign_product.
Qed.

(* Why3 assumption *)
624
Definition product_sign (z:t) (x:t) (y:t) : Prop :=
625
  ((same_sign x y) -> is_positive z) /\ ((diff_sign x y) -> is_negative z).
626 627

(* Why3 assumption *)
628
Definition overflow_value (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
629
  match m with
630 631 632 633 634 635 636 637 638 639
  | 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)))
640 641 642 643 644
  | (ieee_float.RoundingMode.RNA|ieee_float.RoundingMode.RNE) => (is_infinite
      x)
  end.

(* Why3 assumption *)
645
Definition sign_zero_result (m:ieee_float.RoundingMode.mode) (x:t) : Prop :=
646 647
  (is_zero x) ->
  match m with
648 649
  | ieee_float.RoundingMode.RTN => is_negative x
  | _ => is_positive x
650 651 652
  end.

(* Why3 goal *)
653 654 655 656
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))))).
657 658 659 660 661 662 663 664
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 *)
665 666
Lemma add_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
667
  (t'isFinite (add m x y)) -> ((t'isFinite x) /\ (t'isFinite y)).
668 669 670 671 672
Proof.
  apply add_finite_rev.
Qed.

(* Why3 goal *)
673 674 675 676
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)))).
677 678 679 680 681 682 683 684
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 *)
685 686 687 688
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))))).
689 690 691 692 693 694 695 696
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 *)
697 698
Lemma sub_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
699
  (t'isFinite (sub m x y)) -> (t'isFinite x) /\ (t'isFinite y).
700 701 702 703 704
Proof.
  apply sub_finite_rev.
Qed.

(* Why3 goal *)
705 706 707 708
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)))).
709 710 711 712 713 714 715 716
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 *)
717 718 719 720
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))))).
721 722 723 724 725 726 727 728
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 *)
729 730
Lemma mul_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
731
  (t'isFinite (mul m x y)) -> (t'isFinite x) /\ (t'isFinite y).
732 733 734 735 736
Proof.
  apply mul_finite_rev.
Qed.

(* Why3 goal *)
737 738 739 740
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)))).
741 742 743 744 745 746 747 748
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 *)
749 750 751 752
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)))))).
753 754 755 756 757 758 759 760
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 *)
761 762 763
Lemma div_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t),
  (t'isFinite (div m x y)) ->
764 765
  ((t'isFinite x) /\ ((t'isFinite y) /\ ~ (is_zero y))) \/
  ((t'isFinite x) /\ ((is_infinite y) /\ ((t'real (div m x y)) = 0%R))).
766 767 768 769 770
Proof.
  apply div_finite_rev.
Qed.

(* Why3 goal *)
771 772 773 774
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))))).
775 776 777 778 779 780 781 782
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 *)
783 784 785
Lemma neg_finite :
  forall (x:t),
  (t'isFinite x) ->
786
  (t'isFinite (neg x)) /\ ((t'real (neg x)) = (-(t'real x))%R).
787 788 789 790 791
Proof.
  apply neg_finite.
Qed.

(* Why3 goal *)
792 793 794
Lemma neg_finite_rev :
  forall (x:t),
  (t'isFinite (neg x)) ->
795
  (t'isFinite x) /\ ((t'real (neg x)) = (-(t'real x))%R).
796 797 798 799 800
Proof.
  apply neg_finite_rev.
Qed.

(* Why3 goal *)
801 802 803
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)))).
804 805 806 807 808
Proof.
  apply abs_finite.
Qed.

(* Why3 goal *)
809 810 811
Lemma abs_finite_rev :
  forall (x:t),
  (t'isFinite (abs x)) ->
812
  (t'isFinite x) /\ ((t'real (abs x)) = (Reals.Rbasic_fun.Rabs (t'real x))).
813 814 815 816 817
Proof.
  apply abs_finite_rev.
Qed.

(* Why3 goal *)
818
Lemma abs_universal : forall (x:t), ~ (is_negative (abs x)).
819 820 821 822 823
Proof.
  apply abs_universal.
Qed.

(* Why3 goal *)
824 825 826 827 828
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)))))).
829 830 831 832 833 834 835 836
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 *)
837 838 839 840
Lemma fma_finite_rev :
  forall (m:ieee_float.RoundingMode.mode) (x:t) (y:t) (z:t),
  (t'isFinite (fma m x y z)) ->
  ((t'isFinite x) /\ ((t'isFinite y) /\ (t'isFinite z))).
841 842 843 844 845
Proof.
  apply fma_finite_rev.
Qed.

(* Why3 goal *)
846 847 848 849 850
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)))).
851 852 853 854 855 856 857 858
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 *)
859 860 861
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)))))).
862 863 864 865 866
Proof.
  apply sqrt_finite.
Qed.

(* Why3 goal *)
867 868 869
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)))))).
870 871 872 873 874
Proof.
  apply sqrt_finite_rev.
Qed.

(* Why3 assumption *)
875 876
Definition same_sign_real (x:t) (r:R) : Prop :=
  ((is_positive x) /\ (0%R < r)%R) \/ ((is_negative x) /\ (r < 0%R)%R).
877 878 879 880 881 882 883 884 885 886 887 888 889 890

(* Why3 goal *)
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)))))))))).
891 892 893 894 895 896 897 898
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply add_special.
Qed.

(* Why3 goal *)
899 900 901 902 903 904 905 906 907 908 909 910
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)))))))))).
911 912 913 914 915 916 917 918
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply sub_special.
Qed.

(* Why3 goal *)
919 920 921 922 923 924 925 926 927
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))))))))).
928 929 930 931 932 933 934 935
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply mul_special.
Qed.

(* Why3 goal *)
936 937 938 939 940 941 942 943 944
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))))))))).
945 946 947 948 949 950 951 952
Proof.
  intros m x y r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply div_special.
Qed.

(* Why3 goal *)
953 954
Lemma neg_special :
  forall (x:t),
955 956 957
  ((is_nan x) -> is_nan (neg x)) /\
  (((is_infinite x) -> is_infinite (neg x)) /\
   (~ (is_nan x) -> diff_sign x (neg x))).
958 959 960 961 962
Proof.
  apply neg_special.
Qed.

(* Why3 goal *)
963 964
Lemma abs_special :
  forall (x:t),
965 966 967
  ((is_nan x) -> is_nan (abs x)) /\
  (((is_infinite x) -> is_infinite (abs x)) /\
   (~ (is_nan x) -> is_positive (abs x))).
968 969 970 971 972
Proof.
  apply abs_special.
Qed.

(* Why3 goal *)
973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999
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)))))))))))))))))).
1000 1001 1002 1003 1004 1005 1006 1007
Proof.
  intros m x y z r.
  unfold no_overflow, in_range, overflow_value.
  rewrite <- max_real_cst.
  apply fma_special.
Qed.

(* Why3 goal *)
1008 1009 1010 1011 1012 1013
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))))))).
1014 1015 1016 1017 1018
Proof.
  apply sqrt_special.
Qed.

(* Why3 goal *)
1019 1020 1021 1022
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))))).
1023 1024 1025 1026 1027 1028
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_add_exact.
Qed.

(* Why3 goal *)
1029 1030 1031 1032
Lemma of_int_sub_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) (sub n (of_int m i) (of_int m j))))).
1033 1034 1035 1036 1037 1038
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_sub_exact.
Qed.

(* Why3 goal *)
1039 1040 1041 1042
Lemma of_int_mul_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) (mul n (of_int m i) (of_int m j))))).
1043 1044 1045 1046 1047 1048
Proof.
  intros m n i j h1 h2 h3.
  now apply of_int_mul_exact.
Qed.

(* Why3 goal *)
1049
Lemma Min_r : forall (x:t) (y:t), (le y x) -> eq (min x y) y.
1050 1051 1052 1053 1054
Proof.
  apply Min_r.
Qed.

(* Why3 goal *)
1055
Lemma Min_l : forall (x:t) (y:t), (le x y) -> eq (min x y) x.
1056 1057 1058 1059 1060
Proof.
  apply Min_l.
Qed.

(* Why3 goal *)
1061
Lemma Max_r : forall (x:t) (y:t), (le y x) -> eq (max x y) x.
1062 1063 1064 1065 1066
Proof.
  apply Max_r.
Qed.

(* Why3 goal *)
1067
Lemma Max_l : forall (x:t) (y:t), (le x y) -> eq (max x y) y.
1068 1069 1070 1071 1072
Proof.
  apply Max_l.
Qed.

(* Why3 goal *)
1073
Definition is_int : t -> Prop.
1074 1075 1076 1077 1078
Proof.
  apply is_int.
Defined.

(* Why3 goal *)
1079
Lemma zeroF_is_int : is_int zeroF.
1080 1081 1082 1083 1084
Proof.
  apply zeroF_is_int.
Qed.

(* Why3 goal *)
1085 1086
Lemma of_int_is_int :
  forall (m:ieee_float.RoundingMode.mode) (x:Z),
1087
  (in_int_range x) -> is_int (of_int m x).
1088 1089 1090 1091 1092 1093
Proof.
  intros m x h1.
  now apply of_int_is_int.
Qed.

(* Why3 goal *)
1094 1095 1096
Lemma big_float_is_int :
  forall (m:ieee_float.RoundingMode.mode) (i:t),
  (t'isFinite i) ->
1097 1098
  ((le i (neg (of_int m 16777216%Z))) \/ (le (of_int m 16777216%Z) i)) ->
  is_int i.
1099 1100 1101 1102 1103
Proof.
  now apply big_float_is_int.