diff options
author | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2014-10-07 15:28:21 +0200 |
---|---|---|
committer | Jacques-Henri Jourdan <jacques-henri.jourdan@inria.fr> | 2014-10-07 15:28:21 +0200 |
commit | 7159e8142480fd0d851f3fd54b07dc8890f5b610 (patch) | |
tree | 1259927d05b3e82846bbef014d864816f8a19a91 /flocq/Prop/Fprop_plus_error.v | |
parent | fe29750c851cf41d37cab764b1c4d0f0ee68f0d5 (diff) | |
download | compcert-7159e8142480fd0d851f3fd54b07dc8890f5b610.tar.gz compcert-7159e8142480fd0d851f3fd54b07dc8890f5b610.zip |
Upgrade to flocq 2.4.0
Diffstat (limited to 'flocq/Prop/Fprop_plus_error.v')
-rw-r--r-- | flocq/Prop/Fprop_plus_error.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/flocq/Prop/Fprop_plus_error.v b/flocq/Prop/Fprop_plus_error.v index ddae698c..950ca267 100644 --- a/flocq/Prop/Fprop_plus_error.v +++ b/flocq/Prop/Fprop_plus_error.v @@ -23,8 +23,12 @@ Require Import Fcore_Raux. Require Import Fcore_defs. Require Import Fcore_float_prop. Require Import Fcore_generic_fmt. +Require Import Fcore_FIX. +Require Import Fcore_FLX. +Require Import Fcore_FLT. Require Import Fcalc_ops. + Section Fprop_plus_error. Variable beta : radix. @@ -232,3 +236,34 @@ apply Ropp_involutive. Qed. End Fprop_plus_zero. + +Section Fprop_plus_FLT. +Variable beta : radix. + +Notation bpow e := (bpow beta e). + +Variable emin prec : Z. +Context { prec_gt_0_ : Prec_gt_0 prec }. + +Theorem FLT_format_plus_small: forall x y, + generic_format beta (FLT_exp emin prec) x -> + generic_format beta (FLT_exp emin prec) y -> + (Rabs (x+y) <= bpow (prec+emin))%R -> + generic_format beta (FLT_exp emin prec) (x+y). +Proof with auto with typeclass_instances. +intros x y Fx Fy H. +apply generic_format_FLT_FIX... +rewrite Zplus_comm; assumption. +apply generic_format_FIX_FLT, FIX_format_generic in Fx. +apply generic_format_FIX_FLT, FIX_format_generic in Fy. +destruct Fx as (nx,(H1x,H2x)). +destruct Fy as (ny,(H1y,H2y)). +apply generic_format_FIX. +exists (Float beta (Fnum nx+Fnum ny)%Z emin). +split;[idtac|reflexivity]. +rewrite H1x,H1y; unfold F2R; simpl. +rewrite H2x, H2y. +rewrite Z2R_plus; ring. +Qed. + +End Fprop_plus_FLT. |