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/Calc/Fcalc_ops.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/Calc/Fcalc_ops.v')
-rw-r--r-- | flocq/Calc/Fcalc_ops.v | 161 |
1 files changed, 161 insertions, 0 deletions
diff --git a/flocq/Calc/Fcalc_ops.v b/flocq/Calc/Fcalc_ops.v new file mode 100644 index 00000000..15bb2111 --- /dev/null +++ b/flocq/Calc/Fcalc_ops.v @@ -0,0 +1,161 @@ +(** +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. +*) + +(** Basic operations on floats: alignment, addition, multiplication *) +Require Import Fcore_Raux. +Require Import Fcore_defs. +Require Import Fcore_float_prop. + +Section Float_ops. + +Variable beta : radix. + +Notation bpow e := (bpow beta e). + +Definition Falign (f1 f2 : float beta) := + let '(Float m1 e1) := f1 in + let '(Float m2 e2) := f2 in + if Zle_bool e1 e2 + then (m1, (m2 * Zpower beta (e2 - e1))%Z, e1) + else ((m1 * Zpower beta (e1 - e2))%Z, m2, e2). + +Theorem Falign_spec : + forall f1 f2 : float beta, + let '(m1, m2, e) := Falign f1 f2 in + F2R f1 = F2R (Float beta m1 e) /\ F2R f2 = F2R (Float beta m2 e). +Proof. +unfold Falign. +intros (m1, e1) (m2, e2). +generalize (Zle_cases e1 e2). +case (Zle_bool e1 e2) ; intros He ; split ; trivial. +now rewrite <- F2R_change_exp. +rewrite <- F2R_change_exp. +apply refl_equal. +omega. +Qed. + +Theorem Falign_spec_exp: + forall f1 f2 : float beta, + snd (Falign f1 f2) = Zmin (Fexp f1) (Fexp f2). +Proof. +intros (m1,e1) (m2,e2). +unfold Falign; simpl. +generalize (Zle_cases e1 e2);case (Zle_bool e1 e2); intros He. +case (Zmin_spec e1 e2); intros (H1,H2); easy. +case (Zmin_spec e1 e2); intros (H1,H2); easy. +Qed. + +Definition Fopp (f1: float beta) := + let '(Float m1 e1) := f1 in + Float beta (-m1)%Z e1. + +Theorem F2R_opp : + forall f1 : float beta, + (F2R (Fopp f1) = -F2R f1)%R. +intros (m1,e1). +apply F2R_Zopp. +Qed. + +Definition Fabs (f1: float beta) := + let '(Float m1 e1) := f1 in + Float beta (Zabs m1)%Z e1. + +Theorem F2R_abs : + forall f1 : float beta, + (F2R (Fabs f1) = Rabs (F2R f1))%R. +intros (m1,e1). +apply F2R_Zabs. +Qed. + +Definition Fplus (f1 f2 : float beta) := + let '(m1, m2 ,e) := Falign f1 f2 in + Float beta (m1 + m2) e. + +Theorem F2R_plus : + forall f1 f2 : float beta, + F2R (Fplus f1 f2) = (F2R f1 + F2R f2)%R. +Proof. +intros f1 f2. +unfold Fplus. +generalize (Falign_spec f1 f2). +destruct (Falign f1 f2) as ((m1, m2), e). +intros (H1, H2). +rewrite H1, H2. +unfold F2R. simpl. +rewrite Z2R_plus. +apply Rmult_plus_distr_r. +Qed. + +Theorem Fplus_same_exp : + forall m1 m2 e, + Fplus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 + m2) e. +Proof. +intros m1 m2 e. +unfold Fplus. +simpl. +now rewrite Zle_bool_refl, Zminus_diag, Zmult_1_r. +Qed. + +Theorem Fexp_Fplus : + forall f1 f2 : float beta, + Fexp (Fplus f1 f2) = Zmin (Fexp f1) (Fexp f2). +Proof. +intros f1 f2. +unfold Fplus. +rewrite <- Falign_spec_exp. +now destruct (Falign f1 f2) as ((p,q),e). +Qed. + +Definition Fminus (f1 f2 : float beta) := + Fplus f1 (Fopp f2). + +Theorem F2R_minus : + forall f1 f2 : float beta, + F2R (Fminus f1 f2) = (F2R f1 - F2R f2)%R. +Proof. +intros f1 f2; unfold Fminus. +rewrite F2R_plus, F2R_opp. +ring. +Qed. + +Theorem Fminus_same_exp : + forall m1 m2 e, + Fminus (Float beta m1 e) (Float beta m2 e) = Float beta (m1 - m2) e. +Proof. +intros m1 m2 e. +unfold Fminus. +apply Fplus_same_exp. +Qed. + +Definition Fmult (f1 f2 : float beta) := + let '(Float m1 e1) := f1 in + let '(Float m2 e2) := f2 in + Float beta (m1 * m2) (e1 + e2). + +Theorem F2R_mult : + forall f1 f2 : float beta, + F2R (Fmult f1 f2) = (F2R f1 * F2R f2)%R. +Proof. +intros (m1, e1) (m2, e2). +unfold Fmult, F2R. simpl. +rewrite Z2R_mult, bpow_plus. +ring. +Qed. + +End Float_ops. |