Library Flocq.Core.FLT

This file is part of the Flocq formalization of floating-point arithmetic in Coq: https://flocq.gitlabpages.inria.fr/

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

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.

FLT is a nice format: it has a monotone exponent...

Global Instance FLT_exp_monotone : Monotone_exp FLT_exp.

and it allows a rounding to nearest, ties to even.

Global Instance exists_NE_FLT :
(Z.even beta = false ∨ (1 < prec)%Z) →
Exists_NE beta FLT_exp.

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.

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.

Lemma pred_FLT_exact_shift :
  ∀ x e,
  (x ≠ 0)%R →
  (emin + prec + 1 ≤ mag beta x)%Z →
  (emin + prec - mag beta x + 1 ≤ e)%Z →
  (pred beta FLT_exp (x × bpow e) = pred 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.