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_FLT.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_FLT.v')
-rw-r--r-- | flocq/Core/Fcore_FLT.v | 250 |
1 files changed, 250 insertions, 0 deletions
diff --git a/flocq/Core/Fcore_FLT.v b/flocq/Core/Fcore_FLT.v new file mode 100644 index 00000000..4ad47977 --- /dev/null +++ b/flocq/Core/Fcore_FLT.v @@ -0,0 +1,250 @@ +(** +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. +*) + +(** * Floating-point format with gradual underflow *) +Require Import Fcore_Raux. +Require Import Fcore_defs. +Require Import Fcore_rnd. +Require Import Fcore_generic_fmt. +Require Import Fcore_float_prop. +Require Import Fcore_FLX. +Require Import Fcore_FIX. +Require Import Fcore_rnd_ne. + +Section RND_FLT. + +Variable beta : radix. + +Notation bpow e := (bpow beta e). + +Variable emin prec : Z. + +Context { prec_gt_0_ : Prec_gt_0 prec }. + +(* floating-point format with gradual underflow *) +Definition FLT_format (x : R) := + exists f : float beta, + x = F2R f /\ (Zabs (Fnum f) < Zpower beta prec)%Z /\ (emin <= Fexp f)%Z. + +Definition FLT_exp e := Zmax (e - prec) emin. + +(** Properties of the FLT format *) +Global Instance FLT_exp_valid : Valid_exp FLT_exp. +Proof. +intros k. +unfold FLT_exp. +generalize (prec_gt_0 prec). +repeat split ; + intros ; zify ; omega. +Qed. + +Theorem generic_format_FLT : + forall x, FLT_format x -> generic_format beta FLT_exp x. +Proof. +clear prec_gt_0_. +intros x ((mx, ex), (H1, (H2, H3))). +simpl in H2, H3. +rewrite H1. +apply generic_format_F2R. +intros Zmx. +unfold canonic_exp, FLT_exp. +rewrite ln_beta_F2R with (1 := Zmx). +apply Zmax_lub with (2 := H3). +apply Zplus_le_reg_r with (prec - ex)%Z. +ring_simplify. +now apply ln_beta_le_Zpower. +Qed. + +Theorem FLT_format_generic : + forall x, generic_format beta FLT_exp x -> FLT_format x. +Proof. +intros x. +unfold generic_format. +set (ex := canonic_exp beta FLT_exp x). +set (mx := Ztrunc (scaled_mantissa beta FLT_exp x)). +intros Hx. +rewrite Hx. +eexists ; repeat split ; simpl. +apply lt_Z2R. +rewrite Z2R_Zpower. 2: now apply Zlt_le_weak. +apply Rmult_lt_reg_r with (bpow ex). +apply bpow_gt_0. +rewrite <- bpow_plus. +change (F2R (Float beta (Zabs mx) ex) < bpow (prec + ex))%R. +rewrite F2R_Zabs. +rewrite <- Hx. +destruct (Req_dec x 0) as [Hx0|Hx0]. +rewrite Hx0, Rabs_R0. +apply bpow_gt_0. +unfold canonic_exp in ex. +destruct (ln_beta beta x) as (ex', He). +simpl in ex. +specialize (He Hx0). +apply Rlt_le_trans with (1 := proj2 He). +apply bpow_le. +cut (ex' - prec <= ex)%Z. omega. +unfold ex, FLT_exp. +apply Zle_max_l. +apply Zle_max_r. +Qed. + +Theorem FLT_format_satisfies_any : + satisfies_any FLT_format. +Proof. +refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FLT_exp)). +intros x. +split. +apply FLT_format_generic. +apply generic_format_FLT. +Qed. + +Theorem canonic_exp_FLT_FLX : + forall x, x <> R0 -> + (bpow (emin + prec - 1) <= Rabs x)%R -> + canonic_exp beta FLT_exp x = canonic_exp beta (FLX_exp prec) x. +Proof. +intros x Hx0 Hx. +unfold canonic_exp. +apply Zmax_left. +destruct (ln_beta beta x) as (ex, He). +unfold FLX_exp. simpl. +specialize (He Hx0). +cut (emin + prec - 1 < ex)%Z. omega. +apply (lt_bpow beta). +apply Rle_lt_trans with (1 := Hx). +apply He. +Qed. + +(** Links between FLT and FLX *) +Theorem generic_format_FLT_FLX : + forall x : R, + (bpow (emin + prec - 1) <= Rabs x)%R -> + generic_format beta (FLX_exp prec) x -> + generic_format beta FLT_exp x. +Proof. +intros x Hx H. +destruct (Req_dec x 0) as [Hx0|Hx0]. +rewrite Hx0. +apply generic_format_0. +unfold generic_format, scaled_mantissa. +now rewrite canonic_exp_FLT_FLX. +Qed. + +Theorem generic_format_FLX_FLT : + forall x : R, + generic_format beta FLT_exp x -> generic_format beta (FLX_exp prec) x. +Proof. +clear prec_gt_0_. +intros x Hx. +unfold generic_format in Hx; rewrite Hx. +apply generic_format_F2R. +intros _. +rewrite <- Hx. +unfold canonic_exp, FLX_exp, FLT_exp. +apply Zle_max_l. +Qed. + +Theorem round_FLT_FLX : forall rnd x, + (bpow (emin + prec - 1) <= Rabs x)%R -> + round beta FLT_exp rnd x = round beta (FLX_exp prec) rnd x. +intros rnd x Hx. +unfold round, scaled_mantissa. +rewrite canonic_exp_FLT_FLX ; trivial. +contradict Hx. +rewrite Hx, Rabs_R0. +apply Rlt_not_le. +apply bpow_gt_0. +Qed. + +(** Links between FLT and FIX (underflow) *) +Theorem canonic_exp_FLT_FIX : + forall x, x <> R0 -> + (Rabs x < bpow (emin + prec))%R -> + canonic_exp beta FLT_exp x = canonic_exp beta (FIX_exp emin) x. +Proof. +intros x Hx0 Hx. +unfold canonic_exp. +apply Zmax_right. +unfold FIX_exp. +destruct (ln_beta beta x) as (ex, Hex). +simpl. +cut (ex - 1 < emin + prec)%Z. omega. +apply (lt_bpow beta). +apply Rle_lt_trans with (2 := Hx). +now apply Hex. +Qed. + +Theorem generic_format_FIX_FLT : + forall x : R, + generic_format beta FLT_exp x -> + generic_format beta (FIX_exp emin) x. +Proof. +clear prec_gt_0_. +intros x Hx. +rewrite Hx. +apply generic_format_F2R. +intros _. +rewrite <- Hx. +apply Zle_max_r. +Qed. + +Theorem generic_format_FLT_FIX : + forall x : R, + (Rabs x <= bpow (emin + prec))%R -> + generic_format beta (FIX_exp emin) x -> + generic_format beta FLT_exp x. +Proof with auto with typeclass_instances. +clear prec_gt_0_. +apply generic_inclusion_le... +intros e He. +unfold FIX_exp. +apply Zmax_lub. +omega. +apply Zle_refl. +Qed. + +(** FLT is a nice format: it has a monotone exponent... *) +Global Instance FLT_exp_monotone : Monotone_exp FLT_exp. +Proof. +intros ex ey. +unfold FLT_exp. +zify ; omega. +Qed. + +(** and it allows a rounding to nearest, ties to even. *) +Hypothesis NE_prop : Zeven beta = false \/ (1 < prec)%Z. + +Global Instance exists_NE_FLT : Exists_NE beta FLT_exp. +Proof. +destruct NE_prop as [H|H]. +now left. +right. +intros e. +unfold FLT_exp. +destruct (Zmax_spec (e - prec) emin) as [(H1,H2)|(H1,H2)] ; + rewrite H2 ; clear H2. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (e - prec + 1 - prec) emin). +omega. +generalize (Zmax_spec (e + 1 - prec) emin). +generalize (Zmax_spec (emin + 1 - prec) emin). +omega. +Qed. + +End RND_FLT. |