Library Flocq.Core.FLX

This file is part of the Flocq formalization of floating-point arithmetic in Coq:
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

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
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.

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.