From fbead38d40df6904dc0e446f673747b008c40022 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Tue, 7 Dec 2021 12:00:54 +0100
Subject: ZnearestE_opp

---
 lib/IEEE754_extra.v | 87 ++++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 83 insertions(+), 4 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 1ee9c2e0..db4fbec7 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -929,12 +929,91 @@ Proof.
   rewrite Ropp_involutive.
   reflexivity.
 Qed.
-  
-Lemma ZnearestE_opp
-     : forall x : R, ZnearestE (- x) = - ZnearestE x.
-Admitted.
 
+Lemma Zceil_non_floor:
+  forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x).
+Proof.
+  intros x BETWEEN.
+  unfold Z.succ.
+  apply Zceil_imp.
+  split.
+  { rewrite minus_IZR.
+    rewrite plus_IZR.
+    lra.
+  }
+  rewrite plus_IZR.
+  pose proof (Zfloor_ub x).
+  lra.
+Qed.
+
+Lemma Zceil_non_ceil:
+  forall x : R, (x < IZR(Zceil x))%R -> Zceil x = Z.succ(Zfloor x).
+Proof.
+  intros x BETWEEN.
+  unfold Z.succ.
+  cut (Zfloor x = (Zceil x) - 1). { intros; lia. }
+  apply Zfloor_imp.
+  split.
+  { rewrite minus_IZR.
+    pose proof (Zceil_lb x).
+    lra.
+  }
+  rewrite plus_IZR.
+  rewrite minus_IZR.
+  lra.
+Qed.    
 
+Lemma ZnearestE_opp
+     : forall x : R, ZnearestE (- x) = - ZnearestE x.
+Proof.
+  intro x.
+  unfold ZnearestE.
+  case (Rcompare_spec (x - IZR (Zfloor x)) (/ 2)); intro CMP.
+  - pose proof (Zfloor_lb x) as LB.
+    destruct (Rcompare_spec x (IZR (Zfloor x))) as [ ABSURD | EXACT | INEXACT].
+    lra.
+    { set (n := Zfloor x) in *.
+      rewrite EXACT.
+      rewrite <- opp_IZR.
+      rewrite Zfloor_IZR.
+      rewrite opp_IZR.
+      rewrite Rcompare_Lt by lra.
+      reflexivity.
+    }
+    rewrite Rcompare_Gt.
+    { apply Zceil_opp. }
+    rewrite Zfloor_opp.
+    rewrite opp_IZR.
+    rewrite Zceil_non_floor by assumption.
+    unfold Z.succ.
+    rewrite plus_IZR.
+    lra.
+  - rewrite Rcompare_Eq.
+    { rewrite Zceil_opp.
+      rewrite Zfloor_opp.
+      rewrite Z.even_opp.
+      rewrite Zceil_non_floor by lra.
+      rewrite Z.even_succ.
+      rewrite Z.negb_odd.
+      destruct (Z.even (Zfloor x)); reflexivity.
+    }
+    rewrite Zfloor_opp.
+    rewrite opp_IZR.
+    ring_simplify.
+    rewrite Zceil_non_floor by lra.
+    unfold Z.succ.
+    rewrite plus_IZR.
+    lra.
+  - rewrite Rcompare_Lt.
+    { apply Zfloor_opp. }
+    rewrite Zfloor_opp.
+    rewrite opp_IZR.
+    rewrite Zceil_non_floor by lra.
+    unfold Z.succ.
+    rewrite plus_IZR.
+    lra.
+Qed.
+    
 Theorem ZofB_ne_correct:
   forall f,
     ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None.
-- 
cgit