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.

Floating-point format with gradual underflow

Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import 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 (Zabs (Fnum f) < Zpower beta prec)%Z
    (emin Fexp f)%Z FLT_format x.

Definition FLT_exp e := Zmax (e - prec) emin.

Properties of the FLT format
Links between FLT and FLX
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.

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.

FLT is a nice format: it has a monotone exponent...
and it allows a rounding to nearest, ties to even.
Hypothesis NE_prop : Z.even beta = false (1 < prec)%Z.

Global Instance exists_NE_FLT : Exists_NE beta FLT_exp.

End RND_FLT.