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