Library Flocq.Core.FIX

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.

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.


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