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

---
 lib/IEEE754_extra.v | 33 +++++++++++++++++++++++++++++++--
 1 file changed, 31 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index edb3f105..d9329960 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1036,7 +1036,36 @@ Proof.
     { apply IZR_lt. assumption. }
     unfold Zdiv_ne, Z.succ in *.
     case Z.compare_spec; intro CMP.
-    * admit.
+    * pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE.
+      destruct (Z_mod_lt zm p2p POS) as [MOD1 MOD2].
+      set (q := zm / p2p) in *.
+      set (r := zm mod p2p) in *.
+      rewrite inbetween_int_NE with (m := q) (l := loc_Inexact Eq).
+      { cbn. unfold cond_incr.
+        destruct Z.even; reflexivity.
+      }
+      constructor.
+      split.
+      ** assert (0 < IZR zm / IZR p2p - IZR q)%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite <- mult_IZR.
+         rewrite <- minus_IZR.
+         apply IZR_lt.
+         lia.
+      ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite <- mult_IZR.
+         rewrite <- minus_IZR.
+         apply IZR_lt.
+         lia.
     * symmetry.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt. split.
@@ -1103,7 +1132,7 @@ Proof.
          set (q := (zm / p2p)) in *.
          pose proof (Z_mod_lt zm p2p POS) as MOD.
          lia.
-Admitted.
+Qed.
     
 
 (** ** Algebraic identities *)
-- 
cgit