progress on ZofB_ne

1 files changed, 51 insertions, 0 deletions

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index d2372f17..1ee9c2e0 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -890,6 +890,57 @@ Definition Zdiv_ne (a b : Z) :=
   | Eq => (if Z.even q then q else q1)
   end.
 
+Definition ZofB_ne (f: binary_float): option Z :=
+  match f with
+    | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Z.pow_pos radix2 e)%Z
+    | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m))
+    | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zdiv_ne (Zpos m)  (Z.pow_pos radix2 e)))%Z
+    | B754_zero _ _ _ => Some 0%Z
+    | _ => None
+  end.
+
+Lemma ZnearestE_IZR:
+  forall n, (ZnearestE (IZR n)) = n.
+Proof.
+  intro n.
+  unfold ZnearestE.
+  case Rcompare_spec ; intro ORDER.
+  - apply Zfloor_IZR.
+  - destruct negb.
+    + apply Zceil_IZR.
+    + apply Zfloor_IZR.
+  - apply Zceil_IZR.
+Qed.
+
+Lemma Zfloor_opp :
+  forall x : R, (Zfloor (- x)) = - (Zceil x).
+Proof.
+  unfold Zceil, Zfloor.
+  intro x.
+  rewrite Z.opp_involutive.
+  reflexivity.
+Qed.
+
+Lemma Zceil_opp :
+  forall x : R, (Zceil (- x)) = - (Zfloor x).
+Proof.
+  unfold Zceil, Zfloor.
+  intro x.
+  rewrite Ropp_involutive.
+  reflexivity.
+Qed.
+  
+Lemma ZnearestE_opp
+     : forall x : R, ZnearestE (- x) = - ZnearestE x.
+Admitted.
+
+
+Theorem ZofB_ne_correct:
+  forall f,
+    ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None.
+Admitted.
+    
+
 (** ** Algebraic identities *)
 
 (** Commutativity of addition and multiplication *)