Library Flocq.Core.FLT

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 with gradual underflow

Require Import Raux Defs Round_pred Generic_fmt Float_prop.
Require Import FLX FIX Ulp Round_NE.
Require Import Psatz.

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

Lemma negligible_exp_FLT :
   n, negligible_exp FLT_exp = Some n (n emin)%Z.

Theorem generic_format_FLT_1 (Hemin : (emin 0)%Z) :
  generic_format beta FLT_exp 1.

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.

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.