Library Flocq.Core.FLX

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 without underflow

Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import 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 (Zabs (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) Zabs (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 ulp_FLX_0: (ulp beta FLX_exp 0 = 0)%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.

FLX 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_FLX : Exists_NE beta FLX_exp.

End RND_FLX.