Library Flocq.Core.FIX

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.

Fixed-point format

From Coq Require Import ZArith Reals Lia.

Require Import Zaux Raux Defs Round_pred Generic_fmt Ulp Round_NE.

Section RND_FIX.

Variable beta : radix.

Notation bpow := (bpow beta).

Variable emin : Z.

Inductive FIX_format (x : R) : Prop :=
FIX_spec (f : float beta) :
x = F2R f → (Fexp f = emin)%Z → FIX_format x.

Definition FIX_exp (e : Z) := emin.

Properties of the FIX format

Global Instance FIX_exp_valid : Valid_exp FIX_exp.

Theorem generic_format_FIX :
  ∀ x, FIX_format x → generic_format beta FIX_exp x.

Theorem FIX_format_generic :
  ∀ x, generic_format beta FIX_exp x → FIX_format x.

Theorem FIX_format_satisfies_any :
  satisfies_any FIX_format.

Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.

Theorem ulp_FIX :
  ∀ x, ulp beta FIX_exp x = bpow emin.

Global Instance exists_NE_FIX :
      Exists_NE beta FIX_exp.

End RND_FIX.

Theorem round_FIX_IZR :
  ∀ f x,
  round radix2 (FIX_exp 0) f x = IZR (f x).