Library Flocq.Core.FLX
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
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) 2009-2018 Guillaume Melquiond
Floating-point format without underflow
From Coq Require Import ZArith Reals Psatz.
Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE.
Section RND_FLX.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable prec : Z.
Class Prec_gt_0 :=
prec_gt_0 : (0 < prec)%Z.
Context { prec_gt_0_ : Prec_gt_0 }.
Inductive FLX_format (x : R) : Prop :=
FLX_spec (f : float beta) :
x = F2R f → (Z.abs (Fnum f) < Zpower beta prec)%Z → FLX_format x.
Definition FLX_exp (e : Z) := (e - prec)%Z.
Properties of the FLX format
Global Instance FLX_exp_valid : Valid_exp FLX_exp.
Theorem FIX_format_FLX :
∀ x e,
(bpow (e - 1) ≤ Rabs x ≤ bpow e)%R →
FLX_format x →
FIX_format beta (e - prec) x.
Theorem FLX_format_generic :
∀ x, generic_format beta FLX_exp x → FLX_format x.
Theorem generic_format_FLX :
∀ x, FLX_format x → generic_format beta FLX_exp x.
Theorem FLX_format_satisfies_any :
satisfies_any FLX_format.
Theorem FLX_format_FIX :
∀ x e,
(bpow (e - 1) ≤ Rabs x ≤ bpow e)%R →
FIX_format beta (e - prec) x →
FLX_format x.
unbounded floating-point format with normal mantissas
Inductive FLXN_format (x : R) : Prop :=
FLXN_spec (f : float beta) :
x = F2R f →
(x ≠ 0%R → Zpower beta (prec - 1) ≤ Z.abs (Fnum f) < Zpower beta prec)%Z →
FLXN_format x.
Theorem generic_format_FLXN :
∀ x, FLXN_format x → generic_format beta FLX_exp x.
Theorem FLXN_format_generic :
∀ x, generic_format beta FLX_exp x → FLXN_format x.
Theorem FLXN_format_satisfies_any :
satisfies_any FLXN_format.
Lemma negligible_exp_FLX :
negligible_exp FLX_exp = None.
Theorem generic_format_FLX_1 :
generic_format beta FLX_exp 1.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Lemma ulp_FLX_1 : ulp beta FLX_exp 1 = bpow (-prec + 1).
Lemma succ_FLX_1 : (succ beta FLX_exp 1 = 1 + bpow (-prec + 1))%R.
Theorem eq_0_round_0_FLX :
∀ rnd {Vr: Valid_rnd rnd} x,
round beta FLX_exp rnd x = 0%R → x = 0%R.
Theorem gt_0_round_gt_0_FLX :
∀ rnd {Vr: Valid_rnd rnd} x,
(0 < x)%R → (0 < round beta FLX_exp rnd x)%R.
Theorem ulp_FLX_le :
∀ x, (ulp beta FLX_exp x ≤ Rabs x × bpow (1-prec))%R.
Theorem ulp_FLX_ge :
∀ x, (Rabs x × bpow (-prec) ≤ ulp beta FLX_exp x)%R.
Lemma ulp_FLX_exact_shift :
∀ x e,
(ulp beta FLX_exp (x × bpow e) = ulp beta FLX_exp x × bpow e)%R.
Lemma succ_FLX_exact_shift :
∀ x e,
(succ beta FLX_exp (x × bpow e) = succ beta FLX_exp x × bpow e)%R.
Lemma pred_FLX_exact_shift :
∀ x e,
(pred beta FLX_exp (x × bpow e) = pred beta FLX_exp x × bpow e)%R.
FLXN_spec (f : float beta) :
x = F2R f →
(x ≠ 0%R → Zpower beta (prec - 1) ≤ Z.abs (Fnum f) < Zpower beta prec)%Z →
FLXN_format x.
Theorem generic_format_FLXN :
∀ x, FLXN_format x → generic_format beta FLX_exp x.
Theorem FLXN_format_generic :
∀ x, generic_format beta FLX_exp x → FLXN_format x.
Theorem FLXN_format_satisfies_any :
satisfies_any FLXN_format.
Lemma negligible_exp_FLX :
negligible_exp FLX_exp = None.
Theorem generic_format_FLX_1 :
generic_format beta FLX_exp 1.
Theorem ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%R.
Lemma ulp_FLX_1 : ulp beta FLX_exp 1 = bpow (-prec + 1).
Lemma succ_FLX_1 : (succ beta FLX_exp 1 = 1 + bpow (-prec + 1))%R.
Theorem eq_0_round_0_FLX :
∀ rnd {Vr: Valid_rnd rnd} x,
round beta FLX_exp rnd x = 0%R → x = 0%R.
Theorem gt_0_round_gt_0_FLX :
∀ rnd {Vr: Valid_rnd rnd} x,
(0 < x)%R → (0 < round beta FLX_exp rnd x)%R.
Theorem ulp_FLX_le :
∀ x, (ulp beta FLX_exp x ≤ Rabs x × bpow (1-prec))%R.
Theorem ulp_FLX_ge :
∀ x, (Rabs x × bpow (-prec) ≤ ulp beta FLX_exp x)%R.
Lemma ulp_FLX_exact_shift :
∀ x e,
(ulp beta FLX_exp (x × bpow e) = ulp beta FLX_exp x × bpow e)%R.
Lemma succ_FLX_exact_shift :
∀ x e,
(succ beta FLX_exp (x × bpow e) = succ beta FLX_exp x × bpow e)%R.
Lemma pred_FLX_exact_shift :
∀ x e,
(pred beta FLX_exp (x × bpow e) = pred beta FLX_exp x × bpow e)%R.
FLX is a nice format: it has a monotone exponent...
and it allows a rounding to nearest, ties to even.