ZnearestE_opp

1 files changed, 121 insertions, 3 deletions

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 1ee9c2e0..83cacb2b 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -929,15 +929,133 @@ Proof.
   rewrite Ropp_involutive.
   reflexivity.
 Qed.
-  
+
+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.    
+
+(* Can be also done with Znearest_opp and functional extensionality *)
 Lemma ZnearestE_opp
      : forall x : R, ZnearestE (- x) = - ZnearestE x.
-Admitted.
-
+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.
+Proof.
+  destruct f as [s|s|s p H|s m e H]; simpl; auto.
+- f_equal. symmetry. apply (ZnearestE_IZR 0).
+- destruct e; f_equal.
+  + unfold F2R; cbn. rewrite Rmult_1_r. rewrite ZnearestE_IZR. auto.
+  + unfold F2R; cbn. rewrite <- mult_IZR. rewrite ZnearestE_IZR. auto.
+  + unfold F2R; cbn. rewrite IZR_cond_Zopp. rewrite <- cond_Ropp_mult_l.
+    assert (EQ: forall x, ZnearestE (cond_Ropp s x) = cond_Zopp s (ZnearestE x)).
+    { intros. destruct s; cbn; auto. apply ZnearestE_opp. }
+    rewrite EQ. f_equal.
+    generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros.
+    set (p2p := (Z.pow_pos 2 p)) in *.
+    set (zm := Z.pos m) in *.
+    unfold Zdiv_ne, Z.succ in *.
+    case Z.compare_spec; intro CMP.
+    * admit.
+    * symmetry.
+      apply Znearest_imp with (n := zm / p2p).
+      apply Rabs_lt.
+      split.
+      { admit. }
+      assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT.
+      { rewrite <- mult_IZR.
+        rewrite <- minus_IZR.
+        rewrite <- mult_IZR.
+        rewrite <- plus_IZR.
+        apply IZR_lt.
+        lia. }
+      assert (0 < IZR p2p)%R.
+      { apply IZR_lt. assumption. }
+      assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT.
+      2: lra.
+      field_simplify.
+      2: lra.
+      apply Rdiv_lt_0_compat.
+      2: lra.
+      lra.
+    * admit.
 Admitted.