From 75ae1bbac93b1f3cdbdd16a266c5658a28bde90c Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 19:53:15 +0100
Subject: ZofB_ne_correct

---
 lib/IEEE754_extra.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index d9329960..28da42ee 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1066,6 +1066,16 @@ Proof.
          rewrite <- minus_IZR.
          apply IZR_lt.
          lia.
+      ** apply Rcompare_Eq.
+         assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra].
+         field_simplify; [idtac | lra].
+         rewrite <- mult_IZR.
+         rewrite <- mult_IZR.
+         rewrite <- mult_IZR.
+         rewrite <- plus_IZR.
+         rewrite <- minus_IZR.
+         replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia.
+         field. lra.
     * symmetry.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt. split.
-- 
cgit