Library Flocq.Core.FLT
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.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 with gradual underflow
From Coq Require Import ZArith Reals Psatz.
Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FLX FIX Ulp Round_NE.
Section RND_FLT.
Variable beta : radix.
Notation bpow e := (bpow beta e).
Variable emin prec : Z.
Context { prec_gt_0_ : Prec_gt_0 prec }.
Inductive FLT_format (x : R) : Prop :=
FLT_spec (f : float beta) :
x = F2R f → (Z.abs (Fnum f) < Zpower beta prec)%Z →
(emin ≤ Fexp f)%Z → FLT_format x.
Definition FLT_exp e := Z.max (e - prec) emin.
Properties of the FLT format
Global Instance FLT_exp_valid : Valid_exp FLT_exp.
Theorem generic_format_FLT :
∀ x, FLT_format x → generic_format beta FLT_exp x.
Theorem FLT_format_generic :
∀ x, generic_format beta FLT_exp x → FLT_format x.
Theorem generic_format_FLT_bpow :
∀ e, (emin ≤ e)%Z → generic_format beta FLT_exp (bpow e).
Theorem FLT_format_bpow :
∀ e, (emin ≤ e)%Z → FLT_format (bpow e).
Theorem FLT_format_satisfies_any :
satisfies_any FLT_format.
Theorem cexp_FLT_FLX :
∀ x,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x.
Theorem generic_format_FLT :
∀ x, FLT_format x → generic_format beta FLT_exp x.
Theorem FLT_format_generic :
∀ x, generic_format beta FLT_exp x → FLT_format x.
Theorem generic_format_FLT_bpow :
∀ e, (emin ≤ e)%Z → generic_format beta FLT_exp (bpow e).
Theorem FLT_format_bpow :
∀ e, (emin ≤ e)%Z → FLT_format (bpow e).
Theorem FLT_format_satisfies_any :
satisfies_any FLT_format.
Theorem cexp_FLT_FLX :
∀ x,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
cexp beta FLT_exp x = cexp beta (FLX_exp prec) x.
FLT is a nice format: it has a monotone exponent...
and it allows a rounding to nearest, ties to even.
Links between FLT and FLX
Theorem generic_format_FLT_FLX :
∀ x : R,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
generic_format beta (FLX_exp prec) x →
generic_format beta FLT_exp x.
Theorem generic_format_FLX_FLT :
∀ x : R,
generic_format beta FLT_exp x → generic_format beta (FLX_exp prec) x.
Theorem round_FLT_FLX : ∀ rnd x,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
∀ x : R,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
generic_format beta (FLX_exp prec) x →
generic_format beta FLT_exp x.
Theorem generic_format_FLX_FLT :
∀ x : R,
generic_format beta FLT_exp x → generic_format beta (FLX_exp prec) x.
Theorem round_FLT_FLX : ∀ rnd x,
(bpow (emin + prec - 1) ≤ Rabs x)%R →
round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x.
Links between FLT and FIX (underflow)
Theorem cexp_FLT_FIX :
∀ x, x ≠ 0%R →
(Rabs x < bpow (emin + prec))%R →
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.
Theorem generic_format_FIX_FLT :
∀ x : R,
generic_format beta FLT_exp x →
generic_format beta (FIX_exp emin) x.
Theorem generic_format_FLT_FIX :
∀ x : R,
(Rabs x ≤ bpow (emin + prec))%R →
generic_format beta (FIX_exp emin) x →
generic_format beta FLT_exp x.
Lemma negligible_exp_FLT :
∃ n, negligible_exp FLT_exp = Some n ∧ (n ≤ emin)%Z.
Theorem generic_format_FLT_1 :
(emin ≤ 0)%Z →
generic_format beta FLT_exp 1.
Theorem ulp_FLT_0 :
ulp beta FLT_exp 0 = bpow emin.
Theorem ulp_FLT_small :
∀ x, (Rabs x < bpow (emin + prec))%R →
ulp beta FLT_exp x = bpow emin.
Theorem ulp_FLT_le :
∀ x, (bpow (emin + prec - 1) ≤ Rabs x)%R →
(ulp beta FLT_exp x ≤ Rabs x × bpow (1 - prec))%R.
Theorem ulp_FLT_gt :
∀ x, (Rabs x × bpow (-prec) < ulp beta FLT_exp x)%R.
Lemma ulp_FLT_exact_shift :
∀ x e,
(x ≠ 0)%R →
(emin + prec ≤ mag beta x)%Z →
(emin + prec - mag beta x ≤ e)%Z →
(ulp beta FLT_exp (x × bpow e) = ulp beta FLT_exp x × bpow e)%R.
Lemma succ_FLT_exact_shift_pos :
∀ x e,
(0 < x)%R →
(emin + prec ≤ mag beta x)%Z →
(emin + prec - mag beta x ≤ e)%Z →
(succ beta FLT_exp (x × bpow e) = succ beta FLT_exp x × bpow e)%R.
Lemma succ_FLT_exact_shift :
∀ x e,
(x ≠ 0)%R →
(emin + prec + 1 ≤ mag beta x)%Z →
(emin + prec - mag beta x + 1 ≤ e)%Z →
(succ beta FLT_exp (x × bpow e) = succ beta FLT_exp x × bpow e)%R.
Theorem ulp_FLT_pred_pos :
∀ x,
generic_format beta FLT_exp x →
(0 ≤ x)%R →
ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x ∨
(x = bpow (mag beta x - 1) ∧ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R).
End RND_FLT.
∀ x, x ≠ 0%R →
(Rabs x < bpow (emin + prec))%R →
cexp beta FLT_exp x = cexp beta (FIX_exp emin) x.
Theorem generic_format_FIX_FLT :
∀ x : R,
generic_format beta FLT_exp x →
generic_format beta (FIX_exp emin) x.
Theorem generic_format_FLT_FIX :
∀ x : R,
(Rabs x ≤ bpow (emin + prec))%R →
generic_format beta (FIX_exp emin) x →
generic_format beta FLT_exp x.
Lemma negligible_exp_FLT :
∃ n, negligible_exp FLT_exp = Some n ∧ (n ≤ emin)%Z.
Theorem generic_format_FLT_1 :
(emin ≤ 0)%Z →
generic_format beta FLT_exp 1.
Theorem ulp_FLT_0 :
ulp beta FLT_exp 0 = bpow emin.
Theorem ulp_FLT_small :
∀ x, (Rabs x < bpow (emin + prec))%R →
ulp beta FLT_exp x = bpow emin.
Theorem ulp_FLT_le :
∀ x, (bpow (emin + prec - 1) ≤ Rabs x)%R →
(ulp beta FLT_exp x ≤ Rabs x × bpow (1 - prec))%R.
Theorem ulp_FLT_gt :
∀ x, (Rabs x × bpow (-prec) < ulp beta FLT_exp x)%R.
Lemma ulp_FLT_exact_shift :
∀ x e,
(x ≠ 0)%R →
(emin + prec ≤ mag beta x)%Z →
(emin + prec - mag beta x ≤ e)%Z →
(ulp beta FLT_exp (x × bpow e) = ulp beta FLT_exp x × bpow e)%R.
Lemma succ_FLT_exact_shift_pos :
∀ x e,
(0 < x)%R →
(emin + prec ≤ mag beta x)%Z →
(emin + prec - mag beta x ≤ e)%Z →
(succ beta FLT_exp (x × bpow e) = succ beta FLT_exp x × bpow e)%R.
Lemma succ_FLT_exact_shift :
∀ x e,
(x ≠ 0)%R →
(emin + prec + 1 ≤ mag beta x)%Z →
(emin + prec - mag beta x + 1 ≤ e)%Z →
(succ beta FLT_exp (x × bpow e) = succ beta FLT_exp x × bpow e)%R.
Theorem ulp_FLT_pred_pos :
∀ x,
generic_format beta FLT_exp x →
(0 ≤ x)%R →
ulp beta FLT_exp (pred beta FLT_exp x) = ulp beta FLT_exp x ∨
(x = bpow (mag beta x - 1) ∧ ulp beta FLT_exp (pred beta FLT_exp x) = (ulp beta FLT_exp x / IZR beta)%R).
End RND_FLT.