From 4ee0544a157090ddd087b36109d292cd174bae7c Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 2 Aug 2013 08:05:18 +0000 Subject: Merge of Flocq version 2.2.0. More precise modeling of NaNs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- flocq/Core/Fcore_rnd_ne.v | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) (limited to 'flocq/Core/Fcore_rnd_ne.v') diff --git a/flocq/Core/Fcore_rnd_ne.v b/flocq/Core/Fcore_rnd_ne.v index 0b0776ec..6829c0c8 100644 --- a/flocq/Core/Fcore_rnd_ne.v +++ b/flocq/Core/Fcore_rnd_ne.v @@ -2,9 +2,9 @@ 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 +Copyright (C) 2010-2013 Sylvie Boldo #
# -Copyright (C) 2010-2011 Guillaume Melquiond +Copyright (C) 2010-2013 Guillaume Melquiond This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public @@ -499,6 +499,25 @@ rewrite Zeven_plus. now rewrite eqb_sym. Qed. +Lemma round_NE_abs: + forall x : R, + round beta fexp ZnearestE (Rabs x) = Rabs (round beta fexp ZnearestE x). +Proof with auto with typeclass_instances. +intros x. +apply sym_eq. +unfold Rabs at 2. +destruct (Rcase_abs x) as [Hx|Hx]. +rewrite round_NE_opp. +apply Rabs_left1. +rewrite <- (round_0 beta fexp ZnearestE). +apply round_le... +now apply Rlt_le. +apply Rabs_pos_eq. +rewrite <- (round_0 beta fexp ZnearestE). +apply round_le... +now apply Rge_le. +Qed. + Theorem round_NE_pt : forall x, Rnd_NE_pt x (round beta fexp ZnearestE x). -- cgit