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.
Copyright (C) 2018-2019 Érik Martin-Dorel
Copyright (C) 2018-2019 Pierre Roux
Interface Flocq with Coq (>= 8.11) primitive floating-point numbers.
Require Import Int63Compat.
From Coq Require Import ZArith Reals Floats SpecFloat.
Require Import Zaux BinarySingleNaN.
Definition ldexp f (_ : Z) : float := f.
Definition frexp (f : float) := (f, Z0).
Import FloatOps.
Module Import Z.
Notation ldexp := ldexp.
Notation frexp := frexp.
End Z.
Import Floats.
Import Zaux BinarySingleNaN.
Lemma Z_ldexp_spec f e :
Prim2SF (Z.ldexp f e) = SFldexp prec emax (Prim2SF f) e.
Lemma Z_frexp_spec f :
let (m, e) := Z.frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f).
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,
to_Z (normfr_mantissa x) = Z.of_N (Bnormfr_mantissa (Prim2B x)).
Theorem ldexp_equiv :
∀ x e,
Prim2B (Z.ldexp x e) = Bldexp mode_NE (Prim2B x) e.
Theorem ldshiftexp_equiv :
∀ x e,
Prim2B (ldshiftexp x e) = Bldexp mode_NE (Prim2B x) (to_Z e - shift).
Theorem frexp_equiv :
∀ x : float,
let (m, e) := Z.frexp x in
(Prim2B m, e) = Bfrexp (Prim2B x).
Theorem frshiftexp_equiv :
∀ x : float,
let (m, e) := frshiftexp x in
(Prim2B m, (to_Z e - shift)%Z) = Bfrexp (Prim2B x).
Theorem infinity_equiv : infinity = B2Prim (B754_infinity false).
Theorem neg_infinity_equiv : neg_infinity = B2Prim (B754_infinity true).
Theorem nan_equiv : nan = B2Prim B754_nan.
Theorem zero_equiv : zero = B2Prim (B754_zero false).
Theorem neg_zero_equiv : neg_zero = B2Prim (B754_zero true).
Theorem one_equiv : one = B2Prim Bone.
Theorem two_equiv : two = B2Prim (Bplus mode_NE Bone 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 (to_Z i) 0 false.
Theorem eqb_equiv :
∀ x y,
eqb x y = Beqb (Prim2B x) (Prim2B y).
Theorem ltb_equiv :
∀ x y,
ltb x y = Bltb (Prim2B x) (Prim2B y).
Theorem leb_equiv :
∀ x y,
leb x y = Bleb (Prim2B x) (Prim2B y).