From 7159e8142480fd0d851f3fd54b07dc8890f5b610 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan Date: Tue, 7 Oct 2014 15:28:21 +0200 Subject: Upgrade to flocq 2.4.0 --- flocq/Prop/Fprop_plus_error.v | 35 +++++++++++++++++++++++++++++++++++ 1 file changed, 35 insertions(+) (limited to 'flocq/Prop/Fprop_plus_error.v') 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. -- cgit