moved functions to a more logical place

1 files changed, 179 insertions, 165 deletions

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 7e0e7260..636ea1ff 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -28,6 +28,184 @@ Require Import Coq.Logic.FunctionalExtensionality.
 
 Local Open Scope Z_scope.
 
+
+Lemma Znearest_IZR :
+  forall choice n, (Znearest choice (IZR n)) = n.
+Proof.
+  intros.
+  unfold Znearest.
+  case Rcompare_spec ; intro ORDER.
+  - apply Zfloor_IZR.
+  - destruct choice.
+    + apply Zceil_IZR.
+    + apply Zfloor_IZR.
+  - apply Zceil_IZR.
+Qed.
+
+Lemma ZnearestE_IZR:
+  forall n, (ZnearestE (IZR n)) = n.
+Proof.
+  apply Znearest_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.
+Proof.
+  intro.
+  rewrite Znearest_opp.
+  f_equal.
+  f_equal.
+  apply functional_extensionality.
+  intro.
+  rewrite Z.even_opp.
+  fold (Z.succ x0).
+  rewrite Z.even_succ.
+  f_equal.
+  apply Z.negb_odd.
+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.
+
+(** more complicated way of proving
+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.
+ *)
+
+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.
+
+Theorem Znearest_le
+  : forall choice (x y : R), (x <= y)%R -> Znearest choice x <= Znearest choice y.
+Proof.
+  intros.
+  destruct (Z_le_gt_dec (Znearest choice x) (Znearest choice y)) as [LE | GT].
+  assumption.
+  exfalso.
+  assert (1 <= IZR (Znearest choice x) - IZR(Znearest choice y))%R as GAP.
+  { rewrite <- minus_IZR.
+    apply IZR_le.
+    lia.
+  }
+  pose proof (Znearest_imp2 choice x) as Rx.
+  pose proof (Znearest_imp2 choice y) as Ry.
+  apply Rabs_le_inv in Rx.
+  apply Rabs_le_inv in Ry.
+  assert (x = y) by lra.
+  subst y.
+  lia.
+Qed.
+
 Section Extra_ops.
 
 (** [prec] is the number of bits of the mantissa including the implicit one.
@@ -901,145 +1079,6 @@ Definition ZofB_ne (f: binary_float): option Z :=
     | _ => None
   end.
 
-Lemma Znearest_IZR :
-  forall choice n, (Znearest choice (IZR n)) = n.
-Proof.
-  intros.
-  unfold Znearest.
-  case Rcompare_spec ; intro ORDER.
-  - apply Zfloor_IZR.
-  - destruct choice.
-    + apply Zceil_IZR.
-    + apply Zfloor_IZR.
-  - apply Zceil_IZR.
-Qed.
-
-Lemma ZnearestE_IZR:
-  forall n, (ZnearestE (IZR n)) = n.
-Proof.
-  apply Znearest_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.
-Proof.
-  intro.
-  rewrite Znearest_opp.
-  f_equal.
-  f_equal.
-  apply functional_extensionality.
-  intro.
-  rewrite Z.even_opp.
-  fold (Z.succ x0).
-  rewrite Z.even_succ.
-  f_equal.
-  apply Z.negb_odd.
-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.
-
-(** more complicated way of proving
-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.
- *)
-
 Ltac field_simplify_den := field_simplify ; [idtac | lra].
 Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra].
 
@@ -1149,37 +1188,12 @@ Proof.
          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_ball:
   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).
+  pose proof (Rabs_le_inv _ _ ABS).
   lra.
 Qed.