From 4fb3896a10dac9137157262f532a6a5b6e390cf4 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 23:24:28 +0100
Subject: more properties on Znearest

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

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 761f218a..ed3d9f1f 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -954,7 +954,6 @@ Proof.
   apply Z.negb_odd.
 Qed.
 
-(** more complicated way of proving
 Lemma Zceil_non_floor:
   forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x).
 Proof.
@@ -971,6 +970,7 @@ Proof.
   lra.
 Qed.
 
+(** more complicated way of proving
 Lemma Zceil_non_ceil:
   forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x).
 Proof.
@@ -1148,7 +1148,40 @@ Proof.
          pose proof (Z_mod_lt zm p2p POS) as MOD.
          lia.
 Qed.
-    
+
+
+Lemma Znearest_imp2:
+  forall choice x, (Rabs (IZR (Znearest choice x) - x) <= /2)%R.
+Proof.
+  intros.
+  unfold Znearest.
+  pose proof (Zfloor_lb x) as FL.
+  pose proof (Zceil_ub x) as CU.
+  pose proof (Zceil_non_floor x) as NF.
+  case Rcompare_spec; intro CMP; apply Rabs_le; split; try lra.
+  - destruct choice; lra.
+  - destruct choice. 2: lra.
+    rewrite NF. 2: lra.
+    unfold Z.succ. rewrite plus_IZR. lra.
+  - rewrite NF. 2: lra.
+    unfold Z.succ. rewrite plus_IZR. lra.
+Qed.
+
+Lemma Rabs_le_rev : forall {a} {b}, (Rabs a <= b -> -b <= a <= b)%R.
+Proof.
+  intros a b ABS.
+  unfold Rabs in ABS.
+  destruct Rcase_abs in ABS; lra.
+Qed.
+
+Theorem ZofB_ne_range:
+  forall f n, ZofB_ne f = Some n -> (IZR n-1/2 <= B2R _ _ f <= IZR n+1/2)%R.
+Proof.
+  intros. rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; inversion H.
+  pose proof (Znearest_imp2  (fun x => negb (Z.even x)) (B2R prec emax f)) as ABS.
+  pose proof (Rabs_le_rev ABS).
+  lra.
+Qed.
 
 (** ** Algebraic identities *)
 
-- 
cgit