From 54e63022f92795ab9ffa5c67023a98b7d30ebc69 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 6 Dec 2021 19:34:23 +0100
Subject: Zdiv_ne

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

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index b0d1944e..d2372f17 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -879,6 +879,17 @@ Proof.
   unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto.
 Qed.
 
+(** ZofB_ne : convert float to integer, round to nearest *)
+
+Definition Zdiv_ne (a b : Z) :=
+  let q := Z.div a b in
+  let q1 := Z.succ q in
+  match Z.compare (a-b*q) (b*q1-a) with
+  | Lt => q
+  | Gt => q1
+  | Eq => (if Z.even q then q else q1)
+  end.
+
 (** ** Algebraic identities *)
 
 (** Commutativity of addition and multiplication *)
-- 
cgit