diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-28 07:59:03 +0000 |
commit | 5312915c1b29929f82e1f8de80609a277584913f (patch) | |
tree | 0f7ee475743f0eb05d352148a9e1f0b861ee9d34 /flocq/Core/Fcore_FIX.v | |
parent | f3250c32ff42ae18fd03a5311c1f0caec3415aba (diff) | |
download | compcert-5312915c1b29929f82e1f8de80609a277584913f.tar.gz compcert-5312915c1b29929f82e1f8de80609a277584913f.zip |
Use Flocq for floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1939 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'flocq/Core/Fcore_FIX.v')
-rw-r--r-- | flocq/Core/Fcore_FIX.v | 87 |
1 files changed, 87 insertions, 0 deletions
diff --git a/flocq/Core/Fcore_FIX.v b/flocq/Core/Fcore_FIX.v new file mode 100644 index 00000000..f185ddf1 --- /dev/null +++ b/flocq/Core/Fcore_FIX.v @@ -0,0 +1,87 @@ +(** +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 +#<br /># +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. + +(* fixed-point format with exponent emin *) +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. +Proof. +intros k. +unfold FIX_exp. +split ; intros H. +now apply Zlt_le_weak. +split. +apply Zle_refl. +now intros _ _. +Qed. + +Theorem generic_format_FIX : + forall x, FIX_format x -> generic_format beta FIX_exp x. +Proof. +intros x ((xm, xe), (Hx1, Hx2)). +rewrite Hx1. +now apply generic_format_canonic. +Qed. + +Theorem FIX_format_generic : + forall x, generic_format beta FIX_exp x -> FIX_format x. +Proof. +intros x H. +rewrite H. +eexists ; repeat split. +Qed. + +Theorem FIX_format_satisfies_any : + satisfies_any FIX_format. +Proof. +refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)). +intros x. +split. +apply FIX_format_generic. +apply generic_format_FIX. +Qed. + +Global Instance FIX_exp_monotone : Monotone_exp FIX_exp. +Proof. +intros ex ey H. +apply Zle_refl. +Qed. + +End RND_FIX. |