Library Flocq.IEEE754.PrimFloat

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2018-2019 Guillaume Bertholon
Copyright (C) 2018-2019 Érik Martin-Dorel
Copyright (C) 2018-2019 Pierre Roux
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Interface Flocq with Coq (>= 8.11) primitive floating-point numbers.


From Coq Require Import ZArith Reals Floats SpecFloat.
Require Import Zaux BinarySingleNaN.

Conversions from/to Flocq binary_float

Definition Prim2B (x : float) : binary_float prec emax :=
  SF2B (Prim2SF x) (Prim2SF_valid x).

Definition B2Prim (x : binary_float prec emax) : float :=
  SF2Prim (B2SF x).

Lemma B2Prim_Prim2B : x, B2Prim (Prim2B x) = x.

Lemma Prim2B_B2Prim : x, Prim2B (B2Prim x) = x.

Lemma Prim2B_inj : x y, Prim2B x = Prim2B y x = y.

Lemma B2Prim_inj : x y, B2Prim x = B2Prim y x = y.

Lemma B2SF_Prim2B : x, B2SF (Prim2B x) = Prim2SF x.

Lemma Prim2SF_B2Prim : x, Prim2SF (B2Prim x) = B2SF x.

Basic properties of the Binary64 format



Equivalence between prim_float and Flocq binary_float operations

Theorem opp_equiv : x, Prim2B (- x) = Bopp (Prim2B x).

Theorem abs_equiv : x, Prim2B (abs x) = Babs (Prim2B x).

Theorem compare_equiv :
   x y,
  (x ?= y)%float = flatten_cmp_opt (Bcompare (Prim2B x) (Prim2B y)).

Lemma round_nearest_even_equiv s m l :
  round_nearest_even m l = choice_mode mode_NE s m l.

Lemma binary_round_aux_equiv sx mx ex lx :
  SpecFloat.binary_round_aux prec emax sx mx ex lx
  = binary_round_aux prec emax mode_NE sx mx ex lx.

Theorem mul_equiv :
   x y,
  Prim2B (x × y) = Bmult mode_NE (Prim2B x) (Prim2B y).

Lemma binary_round_equiv s m e :
  SpecFloat.binary_round prec emax s m e =
  binary_round prec emax mode_NE s m e.

Lemma binary_normalize_equiv m e szero :
  SpecFloat.binary_normalize prec emax m e szero
  = B2SF (binary_normalize prec emax Hprec Hmax mode_NE m e szero).

Theorem add_equiv :
   x y,
  Prim2B (x + y) = Bplus mode_NE (Prim2B x) (Prim2B y).

Theorem sub_equiv :
   x y,
  Prim2B (x - y) = Bminus mode_NE (Prim2B x) (Prim2B y).

Theorem div_equiv :
   x y,
  Prim2B (x / y) = Bdiv mode_NE (Prim2B x) (Prim2B y).

Theorem sqrt_equiv :
   x, Prim2B (sqrt x) = Bsqrt mode_NE (Prim2B x).

Theorem normfr_mantissa_equiv :
   x,
  Int63.to_Z (normfr_mantissa x) = Z.of_N (Bnormfr_mantissa (Prim2B x)).

Theorem ldexp_equiv :
   x e,
  Prim2B (ldexp x e) = Bldexp mode_NE (Prim2B x) e.

Theorem frexp_equiv :
   x : float,
  let (m, e) := frexp x in
  (Prim2B m, e) = Bfrexp (Prim2B x).

Theorem one_equiv : one = B2Prim Bone.

Theorem ulp_equiv :
   x, Prim2B (ulp x) = Bulp' (Prim2B x).

Theorem next_up_equiv :
   x, Prim2B (next_up x) = Bsucc (Prim2B x).

Theorem next_down_equiv :
   x, Prim2B (next_down x) = Bpred (Prim2B x).

Theorem is_nan_equiv :
   x, PrimFloat.is_nan x = is_nan (Prim2B x).

Theorem is_zero_equiv :
   x,
  is_zero x = match Prim2B x with B754_zero _true | _false end.

Theorem is_infinity_equiv :
   x,
  is_infinity x = match Prim2B x with B754_infinity _true | _false end.

Theorem get_sign_equiv : x, get_sign x = Bsign (Prim2B x).

Theorem is_finite_equiv :
   x, PrimFloat.is_finite x = is_finite (Prim2B x).

Theorem of_int63_equiv :
   i,
  Prim2B (of_int63 i)
  = binary_normalize prec emax Hprec Hmax mode_NE (Int63.to_Z i) 0 false.