GenericFloat.v 158 KB
Newer Older
MARCHE Claude's avatar
MARCHE Claude committed
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  *)
MARCHE Claude's avatar
MARCHE Claude committed
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

Clément Fumex's avatar
Clément Fumex committed
12 13 14 15 16 17 18 19 20 21 22 23 24
(* 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.
25
Require bv.Pow2int.
26
Require ieee_float.RoundingMode.
Clément Fumex's avatar
Clément Fumex committed
27 28 29 30 31

Require Import Flocq.Core.Fcore.
Require Import Flocq.Appli.Fappli_IEEE.
Require Import Flocq.Calc.Fcalc_bracket.
Require Import Flocq.Calc.Fcalc_round.
32
Require Import Flocq.Prop.Fprop_plus_error.
Clément Fumex's avatar
Clément Fumex committed
33 34
Require Import ZArith.
Require Import Fourier.
35 36
Import real.Truncate.
Import ieee_float.RoundingMode.
Clément Fumex's avatar
Clément Fumex committed
37

38 39 40 41 42 43 44
(* extra arguments _ below are needed for Coq prior to 8.6
   keep them until support for Coq 8.5 is dropped *)

Arguments B754_zero {prec} {emax} _ .
Arguments B754_infinity {prec} {emax} _.
Arguments B754_nan {prec} {emax} _ _ .
Arguments B754_finite {prec} {emax} _ _ _ _ .
45

Clément Fumex's avatar
Clément Fumex committed
46 47 48 49 50 51 52 53 54 55 56 57 58
Definition mode_to_IEEE : mode -> Fappli_IEEE.mode.
  exact (fun m =>
           match m with
           | RNE => mode_NE
           | RNA => mode_NA
           | RTP => mode_UP
           | RTN => mode_DN
           | RTZ => mode_ZR
           end).
Defined.

Coercion mode_to_IEEE : mode >-> Fappli_IEEE.mode.

59 60 61
Section GenericFloat.

Variable eb_pos sb_pos : positive.
Clément Fumex's avatar
Clément Fumex committed
62 63 64

(* Why3 goal *)
Definition eb: Z.
65
Proof.
Clément Fumex's avatar
Clément Fumex committed
66 67 68 69 70
  exact (Z.pos eb_pos).
Defined.

(* Why3 goal *)
Definition sb: Z.
71
Proof.
Clément Fumex's avatar
Clément Fumex committed
72 73 74
  exact (Z.pos sb_pos).
Defined.

75 76
Hypothesis Heb : Zlt_bool 1 eb = true.
Hypothesis Hsbb : Zlt_bool 1 sb = true.
Clément Fumex's avatar
Clément Fumex committed
77 78 79

(* Why3 goal *)
Lemma eb_gt_1 : (1%Z < eb)%Z.
80
Proof.
Clément Fumex's avatar
Clément Fumex committed
81 82 83 84 85 86
  rewrite Zlt_is_lt_bool.
  apply Heb.
Qed.

(* Why3 goal *)
Lemma sb_gt_1 : (1%Z < sb)%Z.
87
Proof.
Clément Fumex's avatar
Clément Fumex committed
88 89 90 91 92 93
  rewrite Zlt_is_lt_bool.
  apply Hsbb.
Qed.

(* power of infinities *)
Definition emax : Z.
94
Proof.
Clément Fumex's avatar
Clément Fumex committed
95 96 97 98 99
  exact (radix2 ^ (eb - 1))%Z.
Defined.

(* Why3 goal *)
Definition t : Type.
100
Proof.
Clément Fumex's avatar
Clément Fumex committed
101 102 103 104 105
  exact (binary_float sb emax).
Defined.

(* Why3 goal *)
Definition zeroF: t.
106
Proof.
107
  exact (B754_zero false).
Clément Fumex's avatar
Clément Fumex committed
108 109
Defined.

110
Definition emin := (3 - emax - sb)%Z.
Clément Fumex's avatar
Clément Fumex committed
111 112
Notation fexp := (FLT_exp emin sb).

113 114 115 116 117 118 119 120 121
Lemma Hsb : Zlt_bool 0 sb = true.
Proof.
  auto with zarith.
Qed.

Lemma Hsb': (0 < sb)%Z.
Proof.
  unfold sb; auto with zarith.
Qed.
Clément Fumex's avatar
Clément Fumex committed
122

123
Hypothesis Hemax : Zlt_bool sb emax = true.
Clément Fumex's avatar
Clément Fumex committed
124 125

Lemma Hemax': (sb < emax)%Z.
126
Proof.
Clément Fumex's avatar
Clément Fumex committed
127
  rewrite Zlt_is_lt_bool.
128 129
  apply Hemax.
Qed.
Clément Fumex's avatar
Clément Fumex committed
130 131 132 133

Instance Hsb'' : Prec_gt_0 sb := Hsb'.

Lemma fexp_Valid : Valid_exp fexp.
134
Proof.
Clément Fumex's avatar
Clément Fumex committed
135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
  apply (fexp_correct _ _ Hsb'').
Qed.

Definition r_to_fp rnd x : binary_float sb emax :=
  let r := round radix2 fexp (round_mode rnd) x in
  let m := Ztrunc (scaled_mantissa radix2 fexp r) in
  let e := canonic_exp radix2 fexp r in
  binary_normalize sb emax Hsb' Hemax' rnd m e false.

Theorem r_to_fp_correct :
  forall rnd x,
  let r := round radix2 fexp (round_mode rnd) x in
  (Rabs r < bpow radix2 emax)%R ->
  is_finite sb emax (r_to_fp rnd x) = true /\
  B2R sb emax (r_to_fp rnd x) = r.
Proof with auto with typeclass_instances.
intros rnd x r Bx.
unfold r_to_fp. fold r.
generalize (binary_normalize_correct sb emax Hsb' Hemax' rnd (Ztrunc (scaled_mantissa radix2 fexp r)) (canonic_exp radix2 fexp r) false).
unfold r.
elim generic_format_round...
fold emin r.
rewrite round_generic...
rewrite Rlt_bool_true with (1 := Bx).
now split.
apply generic_format_round...
Qed.

Theorem r_to_fp_format :
  forall rnd x,
  FLT_format radix2 emin sb x ->
  (Rabs x < bpow radix2 emax)%R ->
  B2R sb emax (r_to_fp rnd x) = x.
Proof with auto with typeclass_instances.
intros rnd x Fx Bx.
assert (Gx: generic_format radix2 fexp x).
apply generic_format_FLT.
apply Fx.
pattern x at 2 ; rewrite <- round_generic with (rnd := round_mode rnd) (2 := Gx)...
refine (proj2 (r_to_fp_correct _ _ _)).
rewrite round_generic...
Qed.

Lemma max_eb_bounded : bounded sb emax (2 ^ sb_pos - 1) (emax - sb) = true.
179
Proof.
Clément Fumex's avatar
Clément Fumex committed
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
  assert (0 <= sb - 1)%Z.
  apply Zlt_0_le_0_pred, Hsb'.
  unfold bounded; apply Bool.andb_true_iff; split.
  unfold canonic_mantissa, FLT_exp.
  apply Zeq_bool_true.
  rewrite Fcore_digits.Zpos_digits2_pos.
  rewrite (Fcore_digits.Zdigits_unique radix2 _ sb).
  assert (sb + (emax - sb) - sb = emax - sb)%Z by omega; rewrite H0.
  apply Zmax_left.
  assert (1 < emax)%Z.
  apply Z.le_lt_trans with (m := sb).
  change (Z.succ 0 <= sb)%Z; apply Zgt_le_succ; easy.
  apply Hemax'.
  auto with zarith.
  rewrite Z.abs_eq by auto with zarith.
  change ((2 ^ (sb - 1) <= Z.pos (2 ^ sb_pos - 1) < 2 ^ sb)%Z).
  assert (Z.pos (2 ^ sb_pos - 1) = 2 ^ sb -1)%Z.
  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow.
  fold sb; reflexivity.
  apply Pos.pow_gt_1; easy.
  rewrite H0.
  split; auto with zarith.
  assert (sb = Z.succ (sb - 1)) by auto with zarith.
  rewrite H1 at 2.
  rewrite Z.pow_succ_r by trivial.
  assert (1 <= 2 ^ (sb - 1))%Z.
  apply Z.lt_pred_le, (Zpower_gt_0 radix2 (sb - 1)); trivial.
  omega.
208
  apply Zle_bool_true; auto with zarith.
Clément Fumex's avatar
Clément Fumex committed
209 210
Qed.

211
Definition max_value: t.
212
Proof.
213
  exact (B754_finite false (2 ^ sb_pos - 1) (emax - sb) max_eb_bounded).
214 215
Defined.

Clément Fumex's avatar
Clément Fumex committed
216
Definition One_Nan_pl: nan_pl sb.
217
Proof.
Clément Fumex's avatar
Clément Fumex committed
218 219 220 221 222
  unfold nan_pl, Fcore_digits.digits2_pos.
  exists 1%positive.
  apply Hsbb.
Qed.

223
Definition One_Nan: t := B754_nan false One_Nan_pl.
Clément Fumex's avatar
Clément Fumex committed
224 225

Definition nan_bf: binary_float sb emax -> binary_float sb emax -> bool * nan_pl sb.
226
Proof.
Clément Fumex's avatar
Clément Fumex committed
227
  exact (fun b nan => (true,One_Nan_pl)).
228
Qed.
Clément Fumex's avatar
Clément Fumex committed
229 230

(* Why3 goal *)
231 232 233 234
Definition add: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bplus sb emax _ Hemax' nan_bf).
Defined.
Clément Fumex's avatar
Clément Fumex committed
235 236

(* Why3 goal *)
237 238 239 240
Definition sub: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bminus sb emax _ Hemax' nan_bf).
Defined.
Clément Fumex's avatar
Clément Fumex committed
241 242

(* Why3 goal *)
243 244 245 246
Definition mul: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bmult sb emax _ Hemax' nan_bf).
Defined.
Clément Fumex's avatar
Clément Fumex committed
247 248

(* Why3 goal *)
249 250 251 252
Definition div: ieee_float.RoundingMode.mode -> t -> t -> t.
Proof.
  exact (Bdiv sb emax _ Hemax' nan_bf).
Defined.
Clément Fumex's avatar
Clément Fumex committed
253

MARCHE Claude's avatar
MARCHE Claude committed
254
(* Why3 goal *)
255 256 257 258
Definition abs: t -> t.
Proof.
  exact (Babs sb emax pair).
Defined.
MARCHE Claude's avatar
MARCHE Claude committed
259 260

(* Why3 goal *)
261 262 263 264
Definition neg: t -> t.
Proof.
  exact (Bopp sb emax pair).
Defined.
MARCHE Claude's avatar
MARCHE Claude committed
265

Clément Fumex's avatar
Clément Fumex committed
266
(* Why3 goal *)
267
Definition fma: ieee_float.RoundingMode.mode -> t -> t -> t -> t.
Clément Fumex's avatar
Clément Fumex committed
268 269 270
Admitted.

(* Why3 goal *)
271 272 273 274
Definition sqrt: ieee_float.RoundingMode.mode -> t -> t.
Proof.
  exact (Bsqrt sb emax Hsb' Hemax' (fun b => (true,One_Nan_pl))).
Defined.
Clément Fumex's avatar
Clément Fumex committed
275

276
Definition z_to_fp m x := binary_normalize sb emax Hsb' Hemax' (mode_to_IEEE m) x 0 false.
Clément Fumex's avatar
Clément Fumex committed
277 278

Definition fp_to_z: mode -> t -> Z.
279
Proof.
Clément Fumex's avatar
Clément Fumex committed
280 281 282 283 284 285 286 287 288 289
  exact (fun m x => match m with
         | RNA => ZnearestA (B2R sb emax x)
         | RNE => ZnearestE (B2R sb emax x)
         | RTP => Zceil (B2R sb emax x)
         | RTN => Zfloor (B2R sb emax x)
         | RTZ => Ztrunc (B2R sb emax x)
         end).
Defined.

(* Why3 goal *)
290 291
Definition roundToIntegral: ieee_float.RoundingMode.mode -> t -> t.
Proof.
Clément Fumex's avatar
Clément Fumex committed
292 293
  exact (fun m x =>
           match x with
294 295 296 297
             | B754_zero b => B754_zero b
             | B754_infinity b => B754_infinity b
             | B754_nan b n => B754_nan b n
             | B754_finite b ma e _ =>
Clément Fumex's avatar
Clément Fumex committed
298 299
               let x_int := fp_to_z m x in
               match Z.eq_dec x_int 0%Z with
300
               | left _ => B754_zero b
Clément Fumex's avatar
Clément Fumex committed
301 302 303 304 305 306 307
               | right _ => z_to_fp RTZ x_int
               end
           end).
Defined.

(* Why3 goal *)
Definition min: t -> t -> t.
308
Proof.
Clément Fumex's avatar
Clément Fumex committed
309 310 311 312 313 314 315 316 317
  exact (fun x y => match Bcompare _ _ x y with
           | Some Lt => x
           | Some Gt | Some Eq => y
           | None => One_Nan
         end).
Defined.

(* Why3 goal *)
Definition max: t -> t -> t.
318
Proof.
Clément Fumex's avatar
Clément Fumex committed
319 320 321 322 323 324 325 326 327
  exact (fun x y => match Bcompare _ _ x y with
           | Some Lt => y
           | Some Gt | Some Eq => x
           | None => One_Nan
         end).
Defined.

(* Why3 goal *)
Definition le: t -> t -> Prop.
328
Proof.
Clément Fumex's avatar
Clément Fumex committed
329 330 331 332 333 334 335
  exact (fun a b => Bcompare _ _ a b = Some Lt \/ Bcompare _ _ a b = Some Eq).
Defined.

Hint Unfold le.

(* Why3 goal *)
Definition lt: t -> t -> Prop.
336
Proof.
Clément Fumex's avatar
Clément Fumex committed
337 338 339 340 341
  exact (fun a b => Bcompare _ _ a b = Some Lt).
Defined.

Hint Unfold lt.

342 343
Lemma gt_bcompare : forall {x y}, lt y x <-> Bcompare _ _ x y = Some Gt.
Proof.
Clément Fumex's avatar
Clément Fumex committed
344 345 346 347 348 349 350 351
  intros x y.
  rewrite Bcompare_swap.
  unfold lt.
  destruct Bcompare.
  destruct c; simpl; split; intro h; inversion h; auto.
  split; intro h; inversion h; auto.
Qed.

352 353
Lemma ge_bcompare : forall {x y}, le y x <-> Bcompare _ _ x y = Some Gt \/ Bcompare _ _ x y = Some Eq.
Proof.
Clément Fumex's avatar
Clément Fumex committed
354 355 356 357 358 359 360 361 362 363 364 365
  intros x y.
  unfold le.
  rewrite <-gt_bcompare.
  assert (Bcompare _ _ y x = Some Eq <-> Bcompare _ _ x y = Some Eq).
  rewrite Bcompare_swap.
  destruct Bcompare; try (split; now auto).
  destruct c; simpl; split; intro h; inversion h; auto.
  rewrite H; reflexivity.
Qed.

(* Why3 goal *)
Definition eq: t -> t -> Prop.
366
Proof.
Clément Fumex's avatar
Clément Fumex committed
367 368 369 370 371 372
  exact (fun a b => Bcompare _ _ a b = Some Eq).
Defined.

Hint Unfold eq.

Lemma le_correct: forall x y, le x y <-> lt x y \/ eq x y.
373
Proof.
Clément Fumex's avatar
Clément Fumex committed
374 375 376 377
  intros x y; split; intro h; destruct h; auto.
Qed.

Lemma lt_le: forall {x y}, lt x y -> le x y.
378
Proof.
Clément Fumex's avatar
Clément Fumex committed
379 380 381 382 383
  intros x y.
  rewrite le_correct; auto.
Qed.

Lemma eq_zero_iff: forall {x}, eq zeroF x <-> x = zeroF \/ x = neg zeroF.
384
Proof.
385
  intro; unfold eq; destruct x ; destruct b; simpl.
Clément Fumex's avatar
Clément Fumex committed
386 387 388 389 390 391 392 393 394 395 396 397
  split; auto.
  split; auto.
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
  split; [easy| intro h; destruct h; easy].
Qed.

(* Why3 goal *)
Definition is_normal: t -> Prop.
398
Proof.
Clément Fumex's avatar
Clément Fumex committed
399
  exact (fun x => match x with
400 401
                    | B754_zero _ => True
                    | B754_finite _ _ e _ => (emin < e)%Z
Clément Fumex's avatar
Clément Fumex committed
402 403 404 405 406 407
                    | _ => False
        end).
Defined.

(* Why3 goal *)
Definition is_subnormal: t -> Prop.
408
Proof.
Clément Fumex's avatar
Clément Fumex committed
409
  exact (fun x => match x with
410
                    | B754_finite _ _ e _ => (emin = e)%Z
Clément Fumex's avatar
Clément Fumex committed
411 412 413 414 415 416
                    | _ => False
        end).
Defined.

(* Why3 goal *)
Definition is_zero: t -> Prop.
417
Proof.
Clément Fumex's avatar
Clément Fumex committed
418 419 420
  exact (fun x => eq zeroF x).
Defined.

421
Lemma zero_is_zero: forall {b}, is_zero (B754_zero b).
422
Proof.
423 424 425 426
  easy.
Qed.

Lemma is_zero_B754_zero :
427
  forall x, is_zero x <-> exists b, x = B754_zero b.
428
Proof.
429 430 431 432 433 434 435 436 437 438 439
  intro.
  unfold is_zero; rewrite eq_zero_iff.
  unfold zeroF.
  simpl neg.
  split; intro h; destruct h; auto; try easy.
  exists false; assumption.
  exists true; assumption.
  destruct x0;[right|left];auto.
Qed.

Lemma zero_or_not : forall x, ~ is_zero x \/ is_zero x.
440
Proof.
441
  destruct x ; destruct b; try (right; easy); left; simpl; try easy.
442 443
Qed.

Clément Fumex's avatar
Clément Fumex committed
444 445
(* Why3 goal *)
Definition is_infinite: t -> Prop.
446
Proof.
Clément Fumex's avatar
Clément Fumex committed
447
  exact (fun x => match x with
448
                  | B754_infinity _ => True
Clément Fumex's avatar
Clément Fumex committed
449 450 451 452 453 454
                  | _ => False
                  end).
Defined.

Coercion is_true : bool >-> Sortclass.

455
Lemma eq_infinite_dist: forall {x y}, eq x y -> is_infinite x -> is_infinite y.
456
Proof.
457 458 459
  intros; destruct x, y; try easy; destruct b,b0; easy.
Qed.

Clément Fumex's avatar
Clément Fumex committed
460
(* Why3 goal *)
461 462 463 464
Definition is_nan: t -> Prop.
Proof.
  exact (is_nan sb emax).
Defined.
Clément Fumex's avatar
Clément Fumex committed
465 466

Lemma is_infinite_not_nan: forall {x}, is_infinite x -> ~ is_nan x.
467
Proof.
Clément Fumex's avatar
Clément Fumex committed
468 469 470
  intro x; destruct x; easy.
Qed.

471
Lemma le_infinity: forall {x}, ~ is_nan x -> le x (B754_infinity false).
472
Proof.
473 474 475 476 477 478 479 480 481
  intros.
  unfold le.
  destruct x; try easy.
  + left; easy.
  + destruct b; unfold Bcompare; [left|right]; easy.
  + contradict H; easy.
  + destruct b; left; easy.
Qed.

Clément Fumex's avatar
Clément Fumex committed
482
Lemma is_nan_dec: forall x, {is_nan x} + {~ is_nan x}.
483 484
Proof.
  intro; destruct x; compute; intuition.
Clément Fumex's avatar
Clément Fumex committed
485 486 487
Qed.

Lemma eq_not_nan_refl: forall {x : t}, ~ is_nan x -> eq x x.
488
Proof.
Clément Fumex's avatar
Clément Fumex committed
489 490 491 492 493 494 495
  intros; destruct x; auto.
  destruct b; auto.
  destruct H; easy.
  destruct b; unfold eq; simpl; rewrite Z.compare_refl, Pcompare_refl; easy.
Qed.

Lemma eq_not_nan: forall {x y}, eq x y -> ~ is_nan x /\ ~ is_nan y.
496
Proof.
497
  intros; destruct x; destruct y; try easy; intuition; destruct b; easy.
Clément Fumex's avatar
Clément Fumex committed
498 499 500
Qed.

Lemma lt_not_nan: forall {x y}, lt x y -> ~ is_nan x /\ ~ is_nan y.
501
Proof.
502
  intros; destruct x, y; try easy; intuition; destruct b; easy.
Clément Fumex's avatar
Clément Fumex committed
503 504 505
Qed.

Lemma le_or_lt_or_nan: forall x y, le x y \/ lt y x \/ is_nan x \/ is_nan y.
506 507
Proof.
  unfold is_nan.
Clément Fumex's avatar
Clément Fumex committed
508 509 510
  destruct x, y; auto; try easy;
    try (destruct b, b0; auto; easy).
  unfold le, lt.
511 512
  set (x:=(B754_finite b m e e0)).
  set (y:=(B754_finite b0 m0 e1 e2)).
Clément Fumex's avatar
Clément Fumex committed
513 514 515 516 517 518 519 520 521
  rewrite (Bcompare_correct sb emax x y), (Bcompare_correct sb emax y x); auto.
  destruct (Rtotal_order (B2R sb emax x) (B2R sb emax y)) as [h|[h|h]].
  rewrite (Rcompare_Lt _ _ h), (Rcompare_Gt _ _ h); auto.
  rewrite Rcompare_Eq; auto.
  rewrite (Rcompare_Lt _ _ (Rfourier_gt_to_lt _ _  h)), (Rcompare_Gt _ _ (Rfourier_gt_to_lt _ _ h)); auto.
Qed.

(* Why3 goal *)
Definition is_positive: t -> Prop.
522
Proof.
Clément Fumex's avatar
Clément Fumex committed
523
  exact (fun x => match x with
524 525 526
                    | B754_zero false => True
                    | B754_finite false _ e _ => True
                    | B754_infinity false => True
Clément Fumex's avatar
Clément Fumex committed
527 528 529 530 531 532
                    | _ => False
        end).
Defined.

Hint Unfold is_positive.

533
Lemma is_positive_Bsign: forall x, ~ is_nan x -> (is_positive x <-> Bsign sb emax x = false).
534
Proof.
Clément Fumex's avatar
Clément Fumex committed
535
  split.
536 537
  destruct x ; destruct b; try easy.
  destruct x ; destruct b; try easy.
Clément Fumex's avatar
Clément Fumex committed
538 539 540
  contradict H; easy.
Qed.

541
Lemma is_positive_correct: forall x, is_positive x <-> lt zeroF x \/ x = B754_zero false.
542
Proof.
Clément Fumex's avatar
Clément Fumex committed
543
  split.
544 545
  intro h; destruct x ; destruct b; auto; easy.
  intro h; destruct h; destruct x ; destruct b; easy.
Clément Fumex's avatar
Clément Fumex committed
546 547 548 549
Qed.

(* Why3 goal *)
Definition is_negative: t -> Prop.
550
Proof.
Clément Fumex's avatar
Clément Fumex committed
551
  exact (fun x => match x with
552 553 554
                    | B754_zero true => True
                    | B754_finite true _ e _ => True
                    | B754_infinity true => True
Clément Fumex's avatar
Clément Fumex committed
555 556 557 558 559 560
                    | _ => False
        end).
Defined.

Hint Unfold is_negative.

561
Lemma is_negative_Bsign: forall x, ~ is_nan x -> (is_negative x <-> Bsign sb emax x = true).
562
Proof.
Clément Fumex's avatar
Clément Fumex committed
563
  split.
564 565
  destruct x ; destruct b; easy.
  destruct x ; destruct b; easy.
Clément Fumex's avatar
Clément Fumex committed
566 567
Qed.

568 569
Lemma is_negative_correct: forall x, is_negative x <-> lt x zeroF \/ x = B754_zero true.
Proof.
Clément Fumex's avatar
Clément Fumex committed
570
  split.
571 572
  intro h; destruct x ; destruct b; auto; easy.
  intro h; destruct h; destruct x ; destruct b; easy.
Clément Fumex's avatar
Clément Fumex committed
573 574 575
Qed.

(* Why3 goal *)
576 577 578
Definition is_finite: t -> Prop.
  exact (is_finite sb emax).
Defined.
Clément Fumex's avatar
Clément Fumex committed
579 580

Lemma not_nan: forall x, ~ (is_nan x) -> {is_finite x} + {is_infinite x}.
581 582
Proof.
  unfold is_nan, is_finite.
Clément Fumex's avatar
Clément Fumex committed
583 584 585 586
  intro x; destruct x; simpl; intro; auto.
Qed.

Lemma is_finite_not_nan: forall {x}, is_finite x -> ~ is_nan x.
587
Proof.
Clément Fumex's avatar
Clément Fumex committed
588 589 590 591
  intro x; destruct x; easy.
Qed.

Lemma Finite_Infinite_Nan_dec: forall x:t, {is_finite x} + {is_infinite x} + {is_nan x}.
592
Proof.
Clément Fumex's avatar
Clément Fumex committed
593 594 595 596 597 598 599 600
  intro x; destruct x; simpl.
  left; left; easy.
  left; right; easy.
  right; easy.
  left; left; easy.
Qed.

Lemma eq_finite_dist: forall {x y}, eq x y -> is_finite x -> is_finite y.
601
Proof.
Clément Fumex's avatar
Clément Fumex committed
602 603 604
  intros; destruct x, y; try easy; destruct b,b0; easy.
Qed.

605 606 607 608
Lemma bounded_floats :
  forall x:t, (is_finite x) ->
              Bcompare sb emax (abs x) max_value = Some Lt
           \/ Bcompare sb emax (abs x) max_value = Some Eq.
609
Proof.
610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649
  destruct x; try easy; auto; (* simpl; *) intros.
  destruct (andb_prop _ _ e0) as (H1,H2).
  generalize (Zeq_bool_eq _ _ H1); clear H1; intro H1.
  generalize (Zle_bool_imp_le _ _ H2); clear H2; intro H2.
  destruct (Z_le_lt_eq_dec _ _ H2); clear H2.
  simpl; rewrite (Zcompare_Lt _ _ l); auto.
  simpl; rewrite (Zcompare_Eq _ _ e1).
  unfold FLT_exp in H1.
  rewrite Fcore_digits.Zpos_digits2_pos in H1.
  assert (3 - emax - sb <= Fcore_digits.Zdigits radix2 (Z.pos m) + e - sb)%Z.
  rewrite e1.
  pose sb_gt_1. pose Hemax'.
  assert (Z.pos m <> 0)%Z. pose (Pos2Z.is_pos m); auto with zarith.
  pose (Fcore_digits.Zdigits_gt_0 radix2 (Z.pos m) H0).
  auto with zarith.
  rewrite <-Z.max_l_iff in H0.
  rewrite H0 in H1; clear H0.
  assert (Fcore_digits.Zdigits radix2 (Z.pos m) = sb) by auto with zarith; clear H1.
  pose (Fcore_digits.Zdigits_correct radix2 (Z.pos m)).
  rewrite H0 in a.
  replace (Z.abs (Z.pos m)) with (Z.pos m) in a by auto with zarith.
  destruct a. clear H1.
  assert (Z.pos m = radix2 ^ sb - 1 \/ Z.pos m < radix2 ^ sb - 1)%Z by omega.
  destruct H1.
  right.
  replace (radix2 ^ sb)%Z with (Z.pos 2 ^ Z.pos sb_pos)%Z in H1 by auto.
  rewrite <-Pos2Z.inj_pow, <-Pos2Z.inj_sub, <-Zpos_eq_iff in H1.
  rewrite H1.
  rewrite Pcompare_refl; reflexivity.
  apply Pos.pow_gt_1; easy.
  left.
  rewrite nat_of_P_lt_Lt_compare_complement_morphism. reflexivity.
  apply Pos2Nat.inj_lt.
  replace (radix2 ^ sb)%Z with (Z.pos 2 ^ Z.pos sb_pos)%Z in H1 by auto.
  rewrite <-Pos2Z.inj_pow, <-Pos2Z.inj_sub in H1.
  auto with zarith.
  apply Pos.pow_gt_1; easy.
Qed.

Lemma bounded_floats_le: forall x, is_finite x -> le (abs x) max_value.
650
Proof.
651 652 653 654 655
  apply bounded_floats.
Qed.

Lemma is_finite_B: forall (x:t),
    is_finite x ->
656
    exists b, x = B754_zero b \/ exists b m e p, x = B754_finite b m e p.
657
Proof.
658
  intro x.
659
  destruct x; try easy; intros.
660 661 662
  exists b; auto.
  exists b; right.
  exists b, m, e, e0; trivial.
Clément Fumex's avatar
Clément Fumex committed
663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683
Qed.

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

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

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

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

(* Why3 assumption *)
Definition is_not_nan (x:t): Prop := (is_finite x) \/ (is_infinite x).

(* Why3 goal *)
Lemma is_not_nan1 : forall (x:t), (is_not_nan x) <-> ~ (is_nan x).
684
Proof.
Clément Fumex's avatar
Clément Fumex committed
685 686 687 688 689 690 691 692
  unfold is_not_nan; split; intro H.
  destruct H; [apply is_finite_not_nan|apply is_infinite_not_nan];trivial.
  destruct (not_nan _ H); auto.
Qed.

(* Why3 goal *)
Lemma is_not_finite : forall (x:t), (~ (is_finite x)) <-> ((is_infinite x) \/
  (is_nan x)).
693
Proof.
Clément Fumex's avatar
Clément Fumex committed
694 695 696 697 698 699 700 701 702 703 704
intros x.
destruct x; split; intro h; try easy.
contradict h; easy.
destruct h as [h|h]; contradict h; easy.
left; easy.
right; easy.
contradict h; easy.
destruct h as [h|h]; contradict h; easy.
Qed.

(* Why3 goal *)
705 706 707 708
Definition to_real: t -> R.
Proof.
  exact (B2R sb emax).
Defined.
Clément Fumex's avatar
Clément Fumex committed
709 710

Lemma Some_ext: forall {T} (a b:T), Some a = Some b <-> a = b.
711
Proof.
Clément Fumex's avatar
Clément Fumex committed
712 713 714 715
  intros; split; intro H;[inversion H|rewrite H]; reflexivity.
Qed.

Lemma to_real_eq: forall {x:t} {y:t}, is_finite x -> is_finite y ->
716
                                      (eq x y <-> to_real x = to_real y).
717
Proof.
Clément Fumex's avatar
Clément Fumex committed
718 719 720 721 722 723 724 725
  intros x y h1 h2.
  unfold eq.
  rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext.
  split; intro H; [apply (Rcompare_Eq_inv _ _ H)|
                   apply (Rcompare_Eq _ _ H)].
Qed.

Lemma to_real_eq_alt: forall {x y}, eq x y -> to_real x = to_real y.
726
Proof.
Clément Fumex's avatar
Clément Fumex committed
727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748
  destruct x, y; destruct b, b0; unfold eq, Bcompare; try easy.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      rewrite <-ZC4 in H1.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
Qed.

Lemma le_to_real: forall (x:t) (y:t), is_finite x -> is_finite y ->
  (le x y <-> (to_real x <= to_real y)).
749
Proof.
Clément Fumex's avatar
Clément Fumex committed
750 751 752 753 754 755 756 757 758 759 760 761
intros x y h1 h2.
unfold le.
rewrite (Bcompare_correct _ _ x y h1 h2), Some_ext, Some_ext.
split; intro H.
destruct H; [apply Rlt_le; apply (Rcompare_Lt_inv _ _ H)|
             apply Req_le; apply (Rcompare_Eq_inv _ _ H)].
destruct H; [left; apply (Rcompare_Lt _ _ H)|
             right; apply (Rcompare_Eq _ _ H)].
Qed.

(* Why3 goal *)
Lemma zeroF_is_positive : (is_positive zeroF).
762
Proof.
Clément Fumex's avatar
Clément Fumex committed
763 764 765 766 767
easy.
Qed.

(* Why3 goal *)
Lemma zeroF_is_zero : (is_zero zeroF).
768
Proof.
Clément Fumex's avatar
Clément Fumex committed
769 770 771 772
  apply eq_refl; easy.
Qed.

Lemma zeroF_to_real : ((to_real zeroF) = 0%R).
773
Proof.
Clément Fumex's avatar
Clément Fumex committed
774 775 776
easy.
Qed.

777
Lemma B754_zero_to_real: forall {b}, to_real (B754_zero b) = 0.
778
Proof.
779 780 781 782 783
  intro b.
  rewrite <-(to_real_eq_alt zero_is_zero).
  apply zeroF_to_real.
Qed.

Clément Fumex's avatar
Clément Fumex committed
784 785 786
(* Why3 goal *)
Lemma zero_to_real : forall (x:t), (is_zero x) <-> ((is_finite x) /\
  ((to_real x) = 0%R)).
787
Proof.
Clément Fumex's avatar
Clément Fumex committed
788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804
  unfold is_zero.
  assert (is_finite zeroF) by easy.
  intros x; split; intro H0.
  assert (is_finite x) by apply (eq_finite_dist H0 H).
  split; auto.
  symmetry.
  rewrite <-(to_real_eq H H1); auto.
  destruct H0.
  rewrite to_real_eq; auto.
Qed.

(* Why3 goal *)
Notation of_int := z_to_fp.

(* Why3 goal *)
Notation to_int := fp_to_z.

805
Lemma to_int_zeroF: forall m, to_int m zeroF = 0%Z.
806
Proof.
807 808 809 810 811 812 813 814
  intro m.
  destruct (valid_rnd_round_mode m) as (_,b).
  pose proof (b 0%Z) as H; simpl in H.
  destruct m; simpl; auto.
Qed.

(* add to theory ? *)
Lemma to_int_eq: forall {m x y}, eq x y -> to_int m x = to_int m y.
815
Proof.
816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835
  destruct x, y; destruct b, b0; unfold eq, Bcompare; try easy.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      rewrite <-ZC4 in H1.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
  - destruct (Z_dec e e1) as [[s|s]|s].
    + rewrite Zcompare_Lt by auto; intro; easy.
    + apply Z.gt_lt in s.
      rewrite Zcompare_Gt by auto; intro; easy.
    + rewrite Zcompare_Eq by auto; intro.
      inversion H.
      apply Pcompare_Eq_eq in H1.
      destruct m; simpl; subst; auto.
Qed.

836
Lemma to_int_B754_zero: forall {b m}, to_int m (B754_zero b) = 0%Z.
837
Proof.
838 839 840 841 842 843 844
  intros b m.
  rewrite <-(to_int_eq zero_is_zero).
  apply to_int_zeroF.
Qed.

(* add to theory ? *)
Lemma to_int_le: forall {x y m}, is_finite x -> is_finite y -> le x y -> (to_int m x <= to_int m y)%Z.
845
Proof.
846 847 848 849 850 851 852 853 854 855 856 857
  intros.
  destruct m;

  [destruct (valid_rnd_round_mode mode_NE)|
   destruct (valid_rnd_NA)|
   destruct (valid_rnd_UP)|
   destruct (valid_rnd_DN)|
   destruct (valid_rnd_ZR)];
  apply Zrnd_le;
  apply le_to_real; auto.
Qed.

Clément Fumex's avatar
Clément Fumex committed
858
(* Why3 goal *)
859 860 861
Lemma zero_of_int : forall (m:ieee_float.RoundingMode.mode),
  (zeroF = (of_int m 0%Z)).
Proof.
Clément Fumex's avatar
Clément Fumex committed
862 863 864 865
auto.
Qed.

(* Why3 goal *)
866 867 868 869
Definition round: ieee_float.RoundingMode.mode -> R -> R.
Proof.
  exact (fun m => round radix2 fexp (round_mode m)).
Defined.
Clément Fumex's avatar
Clément Fumex committed
870

871 872
(* Why3 goal *)
Definition max_real: R.
873
Proof.
874 875
  exact ((1 - bpow radix2 (- sb)) * bpow radix2 emax).
Defined.
Clément Fumex's avatar
Clément Fumex committed
876

877
Lemma max_real_is_F2R: @F2R radix2 {| Fnum := Z.pos (2 ^ sb_pos - 1); Fexp := emax - sb |} = max_real.
878
Proof.
879 880 881 882 883 884 885 886 887 888 889 890 891
  unfold F2R.
  unfold Fnum, Fexp.
  rewrite Pos2Z.inj_sub, Pos2Z.inj_pow, Z2R_minus.
  fold sb.
  simpl (Z2R 1).
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower by easy.
  rewrite Int.infix_mn_def, bpow_plus.
  rewrite Rmult_comm, Rmult_assoc, Rmult_comm, Rmult_minus_distr_l.
  rewrite <-bpow_plus.
  replace (- sb + sb)%Z with 0%Z by auto with zarith.
  replace (bpow radix2 0) with 1 by auto.
  rewrite Rmult_1_r.
Clément Fumex's avatar
Clément Fumex committed
892
  reflexivity.
893
  apply Pos.pow_gt_1; easy.
Clément Fumex's avatar
Clément Fumex committed
894 895
Qed.

896
Lemma min_real_is_F2R: @F2R radix2 {| Fnum := Z.neg (2 ^ sb_pos - 1); Fexp := emax - sb |} = - max_real.
897
Proof.
898 899 900
  rewrite <-max_real_is_F2R.
  rewrite <-Fcalc_ops.F2R_opp.
  unfold Fcalc_ops.Fopp.
Clément Fumex's avatar
Clément Fumex committed
901 902 903
  reflexivity.
Qed.

904
Lemma max_value_to_real: to_real max_value = max_real.
905
Proof.
906
  unfold B2R; simpl.
907 908
  apply max_real_is_F2R.
Qed.
Clément Fumex's avatar
Clément Fumex committed
909 910

Lemma max_real_alt : max_real = bpow radix2 emax - bpow radix2 (emax - sb).
911
Proof.
Clément Fumex's avatar
Clément Fumex committed
912 913 914 915 916 917 918 919
  unfold max_real.
  rewrite Rmult_minus_distr_r, Rmult_1_l.
  rewrite <-bpow_plus.
  replace (- sb + emax)%Z with (emax - sb)%Z by auto with zarith.
  reflexivity.
Qed.

Lemma max_real_lt_bpow_radix2_emax: max_real < bpow radix2 emax.
920
Proof.
Clément Fumex's avatar
Clément Fumex committed
921 922 923 924 925 926
  rewrite max_real_alt.
  assert (0 < bpow radix2 (emax - sb)) by apply bpow_gt_0.
  fourier.
Qed.

Lemma max_real_ge_6: 6 <= max_real.
927
Proof.
Clément Fumex's avatar
Clément Fumex committed
928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948
  rewrite max_real_alt.
  assert (2 <= sb)%Z by (pose proof sb_gt_1; auto with zarith).
  assert (sb + 1 <= emax)%Z by (pose proof Hemax'; auto with zarith).
  assert (3 <= emax)%Z by auto with zarith.
  assert (8 <= bpow radix2 emax).
  assert (8 = bpow radix2 3) by easy.
  rewrite H2.
  apply bpow_le; assumption.
  change (6 <= bpow radix2 emax - bpow radix2 (emax + (- sb))).
  rewrite bpow_plus.
  assert (bpow radix2 (- sb) <= /4).
  assert (/4 = bpow radix2 (-2)) by easy.
  rewrite H3.
  apply bpow_le.
  rewrite <-(Z.opp_le_mono 2 sb); assumption.
  assert (bpow radix2 emax * bpow radix2 (-sb) <= bpow radix2 emax * / 4).
  apply Rfourier_le; auto; fourier.
  fourier.
Qed.

Lemma max_real_generic_format: generic_format radix2 fexp max_real.
949
Proof.
Clément Fumex's avatar
Clément Fumex committed
950 951 952 953 954 955
  rewrite <-max_value_to_real.
  apply generic_format_B2R.
Qed.

(* Why3 goal *)
Definition max_int: Z.
956
Proof.
Clément Fumex's avatar
Clément Fumex committed
957 958 959
  exact (2 ^ emax - 2 ^ (emax - sb))%Z.
Defined.

960 961
(* Why3 goal *)
Lemma max_int1 : (max_int = ((bv.Pow2int.pow2 (bv.Pow2int.pow2 (eb - 1%Z)%Z)) - (bv.Pow2int.pow2 ((bv.Pow2int.pow2 (eb - 1%Z)%Z) - sb)%Z))%Z).
962
Proof.
963 964 965 966
  rewrite two_p_equiv, two_p_equiv, two_p_equiv.
  now unfold max_int, emax.
Qed.

Clément Fumex's avatar
Clément Fumex committed
967
(* Why3 goal *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
968 969
Lemma max_real_int : (max_real = (BuiltIn.IZR max_int)).
Proof.
Clément Fumex's avatar
Clément Fumex committed
970 971 972 973 974 975 976 977 978 979 980
  unfold max_int.
  rewrite <-Z2R_IZR, Z2R_minus.
  change 2%Z with (radix_val radix2).
  rewrite Z2R_Zpower, Z2R_Zpower by (pose Hsb'; pose Hemax'; auto with zarith).
  apply max_real_alt.
Qed.

(* Why3 assumption *)
Definition in_range (x:R): Prop := ((-max_real)%R <= x)%R /\
  (x <= max_real)%R.

981 982 983 984
(* Why3 assumption *)
Definition in_int_range (i:Z): Prop := ((-max_int)%Z <= i)%Z /\
  (i <= max_int)%Z.

Clément Fumex's avatar
Clément Fumex committed
985
Lemma in_range_bpow_radix2_emax: forall x, in_range x -> Rabs x < bpow radix2 emax.
986
Proof.
Clément Fumex's avatar
Clément Fumex committed
987 988 989 990 991 992 993
  unfold in_range; intros.
  apply Rle_lt_trans with (r2:= max_real).
  apply Abs.Abs_le; apply H.
  apply max_real_lt_bpow_radix2_emax.
Qed.

Lemma is_finite_abs : forall x:t, is_finite x -> is_finite (abs x).
994
Proof.
Clément Fumex's avatar
Clément Fumex committed
995 996 997 998 999
  destruct x; try easy.
Qed.

(* Why3 goal *)
Lemma is_finite1 : forall (x:t), (is_finite x) -> (in_range (to_real x)).
1000
Proof.
Clément Fumex's avatar
Clément Fumex committed
1001 1002 1003 1004 1005 1006 1007
  intros x h1.
  apply Rabs_le_inv.
  rewrite <-max_value_to_real.
  apply Rcompare_not_Lt_inv.
  pose (is_finite_abs x h1).
  pose (bounded_floats x h1).
  rewrite Bcompare_correct in o; try easy.
1008
  unfold abs in o.
Clément Fumex's avatar
Clément Fumex committed
1009
  rewrite B2R_Babs in o.
1010
  unfold to_real.
Clément Fumex's avatar
Clément Fumex committed
1011 1012 1013 1014 1015 1016 1017
  intro H0.
  destruct o as [H|H]; inversion H as (H1);
  rewrite Rcompare_sym in H1; apply CompOpp_iff in H1;
  simpl in H0; rewrite H0 in H1;
  inversion H1.
Qed.

1018 1019
Lemma Rabs_round_max_real_emax:
  forall {m} {x}, Rabs (round m x) <= max_real <-> Rabs (round m x) < bpow radix2 emax.
1020
Proof.
Clément Fumex's avatar
Clément Fumex committed
1021 1022 1023 1024 1025
  intros m x; split; intro h.
  - apply Rle_lt_trans with (r2 := max_real).
    apply h.
    apply max_real_lt_bpow_radix2_emax.
  - destruct (r_to_fp_correct m x h).
1026
    unfold round.
Clément Fumex's avatar
Clément Fumex committed
1027 1028 1029 1030 1031
    rewrite <-H0, Abs.Abs_le.
    apply (is_finite1 _ H).
Qed.

(* Why3 assumption *)
1032 1033
Definition no_overflow (m:ieee_float.RoundingMode.mode) (x:R): Prop :=
  (in_range (round m x)).
Clément Fumex's avatar
Clément Fumex committed
1034 1035

Lemma no_overflow_Rabs_round_max_real: forall {m} {x}, no_overflow m x <-> Rabs (round m x) <= max_real.
1036
Proof.
Clément Fumex's avatar
Clément Fumex committed
1037 1038 1039 1040 1041
  intro x.
  split; intro h; apply Abs.Abs_le; easy.
Qed.

Lemma no_overflow_Rabs_round_emax: forall {m} {x}, no_overflow m x <-> Rabs (round m x) < bpow radix2 emax.
1042
Proof.
Clément Fumex's avatar
Clément Fumex committed
1043 1044 1045 1046
  intros m x.
  apply (iff_trans no_overflow_Rabs_round_max_real Rabs_round_max_real_emax).
Qed.

1047
Lemma IZR_alt: forall {x}, @F2R radix2 {| Fnum := x; Fexp := 0 |} = IZR x.
1048
Proof.
1049 1050 1051 1052
  intros; unfold F2R, Fnum, Fexp, FLT_exp.
  assert (bpow radix2 0 = 1) as bpow_0 by easy.
  rewrite bpow_0, Rmult_1_r, Z2R_IZR.
  reflexivity.
Clément Fumex's avatar
Clément Fumex committed
1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064
Qed.

Lemma of_int_correct :
  forall {m} {x},
    no_overflow m (IZR x) ->
      to_real (of_int m x) = round m (IZR x) /\ is_finite (of_int m x) /\
      Bsign sb emax (of_int m x) =
      match (x ?= 0)%Z with
      | Eq => false
      | Lt => true
      | Gt => false
      end.
1065
Proof.
Clément Fumex's avatar
Clément Fumex committed
1066 1067 1068
  intros m x h1.
  generalize (binary_normalize_correct sb emax Hsb' Hemax' m x 0 false).
  rewrite Rlt_bool_true.
1069
  - intro; destruct H; destruct H0.
Clément Fumex's avatar
Clément Fumex committed
1070 1071
    rewrite IZR_alt in H1.
    split.
1072
    rewrite IZR_alt in H; auto.
Clément Fumex's avatar
Clément Fumex committed
1073 1074 1075 1076 1077 1078 1079 1080 1081
    split; auto.
    rewrite <-Rcompare_Z2R.
    rewrite Z2R_IZR; auto.

  - apply no_overflow_Rabs_round_emax.
    rewrite IZR_alt; apply h1.
Qed.

(* Why3 goal *)
1082 1083 1084
Lemma Bounded_real_no_overflow : forall (m:ieee_float.RoundingMode.mode)
  (x:R), (in_range x) -> (no_overflow m x).
Proof.
Clément Fumex's avatar
Clément Fumex committed
1085 1086 1087 1088 1089 1090 1091 1092 1093 1094
intros m x h1.
rewrite no_overflow_Rabs_round_max_real.
apply abs_round_le_generic.
apply fexp_Valid.
apply valid_rnd_round_mode.
apply max_real_generic_format.
rewrite Abs.Abs_le; easy.
Qed.

(* Why3 goal *)
1095 1096 1097
Lemma Round_monotonic : forall (m:ieee_float.RoundingMode.mode) (x:R) (y:R),
  (x <= y)%R -> ((round m x) <= (round m y))%R.
Proof.
Clément Fumex's avatar
Clément Fumex committed
1098 1099 1100 1101 1102 1103 1104
  intros m x y h1.
  apply round_le.
  apply fexp_Valid.
  apply valid_rnd_round_mode.
  apply h1.
Qed.

1105
Lemma round_lt : forall {x y} {m:mode}, round m x < round m y -> x < y.
1106
Proof.
1107 1108 1109 1110 1111 1112 1113 1114 1115
  intros x y m h.
  case (Rlt_dec x y); auto.
  intro.
  apply Rnot_lt_le in n.
  apply (Round_monotonic m) in n.
  apply RIneq.Rle_not_lt in n.
  contradict h; assumption.
Qed.

Clément Fumex's avatar
Clément Fumex committed
1116
(* Why3 goal *)