Library Flocq.Core.Fcore_FIX

This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 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

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_rnd.
Require Import Fcore_generic_fmt.
Require Import Fcore_rnd_ne.

Section RND_FIX.

Variable beta : radix.

Notation bpow := (bpow beta).

Variable emin : Z.

Definition FIX_format (x : R) :=
  exists f : float beta,
  x = F2R f /\ (Fexp f = emin)%Z.

Definition FIX_exp (e : Z) := emin.

Properties of the FIX format

Global Instance FIX_exp_valid : Valid_exp FIX_exp.

Theorem generic_format_FIX :
  forall x, FIX_format x -> generic_format beta FIX_exp x.

Theorem FIX_format_generic :
  forall 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.

End RND_FIX.