From 54e63022f92795ab9ffa5c67023a98b7d30ebc69 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 6 Dec 2021 19:34:23 +0100
Subject: Zdiv_ne

---
 lib/IEEE754_extra.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index b0d1944e..d2372f17 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -879,6 +879,17 @@ Proof.
   unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto.
 Qed.
 
+(** ZofB_ne : convert float to integer, round to nearest *)
+
+Definition Zdiv_ne (a b : Z) :=
+  let q := Z.div a b in
+  let q1 := Z.succ q in
+  match Z.compare (a-b*q) (b*q1-a) with
+  | Lt => q
+  | Gt => q1
+  | Eq => (if Z.even q then q else q1)
+  end.
+
 (** ** Algebraic identities *)
 
 (** Commutativity of addition and multiplication *)
-- 
cgit 


From c5e74c17f2ab7f40d314417f2b20b18d4d2d057b Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 6 Dec 2021 21:14:46 +0100
Subject: progress on ZofB_ne

---
 lib/IEEE754_extra.v | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

(limited to 'lib')

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 *)
-- 
cgit 


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 


From 0825b433dd2ebd947d5d4566ce8a3dfd8a98db88 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 | 124 ++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 121 insertions(+), 3 deletions(-)

(limited to 'lib')

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.
     
 
-- 
cgit 


From b08a818cbc7872b1a062a80ea478b2e32e3a3746 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Wed, 8 Dec 2021 22:32:41 +0100
Subject: ZofB_ne_correct unfinished

---
 lib/IEEE754_extra.v | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 56b90727..a0ae3089 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1038,7 +1038,24 @@ Proof.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt.
       split.
-      { admit. }
+      { assert (p2p > 0) as POS by lia.
+        pose proof (Z_mult_div_ge zm p2p POS).
+        assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R.
+        2: lra.
+        assert (0 < IZR p2p)%R as POS2.
+        { apply IZR_lt. lia. }
+        field_simplify.
+        2: lra.
+        apply Rmult_le_pos.
+        { rewrite <- mult_IZR.
+          rewrite <- minus_IZR.
+          apply IZR_le.
+          lia.
+        }
+        assert (0 < / IZR p2p)%R.
+        2: lra.
+        apply Rinv_0_lt_compat. assumption.
+      }
       assert (0 < 2*(IZR p2p * IZR (zm / p2p) - IZR zm) + (IZR p2p))%R as LT.
       { rewrite <- mult_IZR.
         rewrite <- minus_IZR.
-- 
cgit 


From bfbcc770319a0d3b8935314b16f1e0c205436685 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 15:19:01 +0100
Subject: progress on ZnearestE

---
 lib/IEEE754_extra.v | 78 ++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 54 insertions(+), 24 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index a0ae3089..edb3f105 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1031,19 +1031,18 @@ Proof.
     generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros.
     set (p2p := (Z.pow_pos 2 p)) in *.
     set (zm := Z.pos m) in *.
+    assert (p2p > 0) as POS by lia.
+    assert (0 < IZR p2p)%R as POS2.
+    { apply IZR_lt. assumption. }
     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.
-      { assert (p2p > 0) as POS by lia.
-        pose proof (Z_mult_div_ge zm p2p POS).
+      apply Rabs_lt. split.
+     ** pose proof (Z_mult_div_ge zm p2p POS).
         assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R.
         2: lra.
-        assert (0 < IZR p2p)%R as POS2.
-        { apply IZR_lt. lia. }
         field_simplify.
         2: lra.
         apply Rmult_le_pos.
@@ -1055,24 +1054,55 @@ Proof.
         assert (0 < / IZR p2p)%R.
         2: lra.
         apply Rinv_0_lt_compat. assumption.
-      }
-      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.
+     ** 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 zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT.
+        2: lra.
+        field_simplify.
+        2: lra.
+        apply Rdiv_lt_0_compat.
+        2: lra.
+        lra.
+    * symmetry.
+      apply Znearest_imp.
+      apply Rabs_lt. split.
+      ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R.
+         { ring_simplify.
+           rewrite <- mult_IZR.
+           rewrite <- mult_IZR.
+           rewrite <- mult_IZR.
+           rewrite <- minus_IZR.
+           rewrite <- minus_IZR.
+           apply IZR_lt.
+           lia.
+         }
+         assert (0 < (/ 2) + IZR zm * / IZR p2p - IZR (zm / p2p + 1))%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite plus_IZR.
+         lra.
+      ** assert (0 < IZR (zm / p2p + 1) - (IZR zm * / IZR p2p))%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite <- mult_IZR.
+         rewrite <- minus_IZR.
+         apply IZR_lt.
+         pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE.
+         ring_simplify.
+         set (q := (zm / p2p)) in *.
+         pose proof (Z_mod_lt zm p2p POS) as MOD.
+         lia.
 Admitted.
     
 
-- 
cgit 


From d3f9053b783714151aab27eb153f1b727e843ad1 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 19:02:35 +0100
Subject: ZofB_ne_correct

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

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index edb3f105..d9329960 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1036,7 +1036,36 @@ Proof.
     { apply IZR_lt. assumption. }
     unfold Zdiv_ne, Z.succ in *.
     case Z.compare_spec; intro CMP.
-    * admit.
+    * pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE.
+      destruct (Z_mod_lt zm p2p POS) as [MOD1 MOD2].
+      set (q := zm / p2p) in *.
+      set (r := zm mod p2p) in *.
+      rewrite inbetween_int_NE with (m := q) (l := loc_Inexact Eq).
+      { cbn. unfold cond_incr.
+        destruct Z.even; reflexivity.
+      }
+      constructor.
+      split.
+      ** assert (0 < IZR zm / IZR p2p - IZR q)%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite <- mult_IZR.
+         rewrite <- minus_IZR.
+         apply IZR_lt.
+         lia.
+      ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R.
+         2: lra.
+         field_simplify.
+         2: lra.
+         apply Rdiv_lt_0_compat.
+         2: lra.
+         rewrite <- mult_IZR.
+         rewrite <- minus_IZR.
+         apply IZR_lt.
+         lia.
     * symmetry.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt. split.
@@ -1103,7 +1132,7 @@ Proof.
          set (q := (zm / p2p)) in *.
          pose proof (Z_mod_lt zm p2p POS) as MOD.
          lia.
-Admitted.
+Qed.
     
 
 (** ** Algebraic identities *)
-- 
cgit 


From 75ae1bbac93b1f3cdbdd16a266c5658a28bde90c Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 19:53:15 +0100
Subject: ZofB_ne_correct

---
 lib/IEEE754_extra.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index d9329960..28da42ee 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1066,6 +1066,16 @@ Proof.
          rewrite <- minus_IZR.
          apply IZR_lt.
          lia.
+      ** apply Rcompare_Eq.
+         assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra].
+         field_simplify; [idtac | lra].
+         rewrite <- mult_IZR.
+         rewrite <- mult_IZR.
+         rewrite <- mult_IZR.
+         rewrite <- plus_IZR.
+         rewrite <- minus_IZR.
+         replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia.
+         field. lra.
     * symmetry.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt. split.
-- 
cgit 


From 0be6b3d13d2e8920653dde8cf8f7e27af608d812 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 21:47:42 +0100
Subject: beautify proof

---
 lib/IEEE754_extra.v | 40 ++++++++++++++++------------------------
 1 file changed, 16 insertions(+), 24 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 28da42ee..2806e572 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1014,7 +1014,10 @@ Proof.
     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].
+
 Theorem ZofB_ne_correct:
   forall f,
     ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None.
@@ -1048,27 +1051,23 @@ Proof.
       split.
       ** assert (0 < IZR zm / IZR p2p - IZR q)%R.
          2: lra.
-         field_simplify.
-         2: lra.
-         apply Rdiv_lt_0_compat.
-         2: lra.
+         field_simplify_den.
+         Rdiv_lt_0_den.
          rewrite <- mult_IZR.
          rewrite <- minus_IZR.
          apply IZR_lt.
          lia.
       ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R.
          2: lra.
-         field_simplify.
-         2: lra.
-         apply Rdiv_lt_0_compat.
-         2: lra.
+         field_simplify_den.
+         Rdiv_lt_0_den.
          rewrite <- mult_IZR.
          rewrite <- minus_IZR.
          apply IZR_lt.
          lia.
       ** apply Rcompare_Eq.
          assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra].
-         field_simplify; [idtac | lra].
+         field_simplify_den.
          rewrite <- mult_IZR.
          rewrite <- mult_IZR.
          rewrite <- mult_IZR.
@@ -1082,8 +1081,7 @@ Proof.
      ** pose proof (Z_mult_div_ge zm p2p POS).
         assert (0 <= IZR zm * / IZR p2p - IZR (zm / p2p))%R.
         2: lra.
-        field_simplify.
-        2: lra.
+        field_simplify_den.
         apply Rmult_le_pos.
         { rewrite <- mult_IZR.
           rewrite <- minus_IZR.
@@ -1102,10 +1100,8 @@ Proof.
           lia. }
         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.
+        field_simplify_den.
+        Rdiv_lt_0_den.
         lra.
     * symmetry.
       apply Znearest_imp.
@@ -1122,18 +1118,14 @@ Proof.
          }
          assert (0 < (/ 2) + IZR zm * / IZR p2p - IZR (zm / p2p + 1))%R.
          2: lra.
-         field_simplify.
-         2: lra.
-         apply Rdiv_lt_0_compat.
-         2: lra.
+         field_simplify_den.
+         Rdiv_lt_0_den.
          rewrite plus_IZR.
          lra.
       ** assert (0 < IZR (zm / p2p + 1) - (IZR zm * / IZR p2p))%R.
          2: lra.
-         field_simplify.
-         2: lra.
-         apply Rdiv_lt_0_compat.
-         2: lra.
+         field_simplify_den.
+         Rdiv_lt_0_den.
          rewrite <- mult_IZR.
          rewrite <- minus_IZR.
          apply IZR_lt.
-- 
cgit 


From 9d4528e4edaa2b968d52628e6b5c10e6640f5e03 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 21:59:10 +0100
Subject: factorize proof

---
 lib/IEEE754_extra.v | 50 ++++++++++++++++++++++----------------------------
 1 file changed, 22 insertions(+), 28 deletions(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 2806e572..b8397210 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -899,19 +899,25 @@ Definition ZofB_ne (f: binary_float): option Z :=
     | _ => None
   end.
 
-Lemma ZnearestE_IZR:
-  forall n, (ZnearestE (IZR n)) = n.
+Lemma Znearest_IZR :
+  forall choice n, (Znearest choice (IZR n)) = n.
 Proof.
-  intro n.
-  unfold ZnearestE.
+  intros.
+  unfold Znearest.
   case Rcompare_spec ; intro ORDER.
   - apply Zfloor_IZR.
-  - destruct negb.
+  - 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.
@@ -1018,6 +1024,9 @@ Qed.
 Ltac field_simplify_den := field_simplify ; [idtac | lra].
 Ltac Rdiv_lt_0_den := apply Rdiv_lt_0_compat ; [idtac | lra].
 
+Hint Rewrite <- plus_IZR minus_IZR opp_IZR mult_IZR : l_IZR.
+Ltac l_IZR := autorewrite with l_IZR.
+
 Theorem ZofB_ne_correct:
   forall f,
     ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None.
@@ -1053,28 +1062,22 @@ Proof.
          2: lra.
          field_simplify_den.
          Rdiv_lt_0_den.
-         rewrite <- mult_IZR.
-         rewrite <- minus_IZR.
+         l_IZR.
          apply IZR_lt.
          lia.
       ** assert (0 < IZR (q + 1) - (IZR zm * / IZR p2p))%R.
          2: lra.
          field_simplify_den.
          Rdiv_lt_0_den.
-         rewrite <- mult_IZR.
-         rewrite <- minus_IZR.
+         l_IZR.
          apply IZR_lt.
          lia.
       ** apply Rcompare_Eq.
          assert ((IZR q + IZR (q + 1))/2 - (IZR zm * / IZR p2p) = 0)%R; [idtac|lra].
          field_simplify_den.
-         rewrite <- mult_IZR.
-         rewrite <- mult_IZR.
-         rewrite <- mult_IZR.
-         rewrite <- plus_IZR.
-         rewrite <- minus_IZR.
+         l_IZR.
          replace (q * p2p + (q + 1) * p2p - 2 * zm) with 0 by lia.
-         field. lra.
+         field. apply IZR_neq. lia.
     * symmetry.
       apply Znearest_imp with (n := zm / p2p).
       apply Rabs_lt. split.
@@ -1083,8 +1086,7 @@ Proof.
         2: lra.
         field_simplify_den.
         apply Rmult_le_pos.
-        { rewrite <- mult_IZR.
-          rewrite <- minus_IZR.
+        { l_IZR.
           apply IZR_le.
           lia.
         }
@@ -1092,10 +1094,7 @@ Proof.
         2: lra.
         apply Rinv_0_lt_compat. assumption.
      ** 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.
+        { l_IZR.
           apply IZR_lt.
           lia. }
         assert (0 < -(IZR zm * / IZR p2p - IZR (zm / p2p) - / 2))%R as GT.
@@ -1108,11 +1107,7 @@ Proof.
       apply Rabs_lt. split.
       ** assert (0 < (IZR zm - IZR p2p * IZR (zm / p2p)) - (IZR p2p * (IZR (zm / p2p) + 1) - IZR zm))%R.
          { ring_simplify.
-           rewrite <- mult_IZR.
-           rewrite <- mult_IZR.
-           rewrite <- mult_IZR.
-           rewrite <- minus_IZR.
-           rewrite <- minus_IZR.
+           l_IZR.
            apply IZR_lt.
            lia.
          }
@@ -1126,8 +1121,7 @@ Proof.
          2: lra.
          field_simplify_den.
          Rdiv_lt_0_den.
-         rewrite <- mult_IZR.
-         rewrite <- minus_IZR.
+         l_IZR.
          apply IZR_lt.
          pose proof (Z_div_mod_eq_full zm p2p) as DECOMPOSE.
          ring_simplify.
-- 
cgit 


From d2669ab4948104c85b795c15a47df98f0b81a40c Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 22:37:29 +0100
Subject: factor proofs

---
 lib/IEEE754_extra.v | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index b8397210..761f218a 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -24,6 +24,8 @@ Require Import Psatz.
 Require Import Bool.
 Require Import Eqdep_dec.
 
+Require Import Coq.Logic.FunctionalExtensionality.
+
 Local Open Scope Z_scope.
 
 Section Extra_ops.
@@ -936,6 +938,23 @@ Proof.
   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.
+
+(** more complicated way of proving
 Lemma Zceil_non_floor:
   forall x : R, (x > IZR(Zfloor x))%R -> Zceil x = Z.succ(Zfloor x).
 Proof.
@@ -969,7 +988,6 @@ Proof.
   lra.
 Qed.    
 
-(* Can be also done with Znearest_opp and functional extensionality *)
 Lemma ZnearestE_opp
      : forall x : R, ZnearestE (- x) = - ZnearestE x.
 Proof.
@@ -1020,6 +1038,7 @@ Proof.
     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].
-- 
cgit 


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 


From 1c77deb420e626aa79d5b7db15231c887cd7d870 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Dec 2021 23:29:25 +0100
Subject: minor implicit issue

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

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index ed3d9f1f..a76daab4 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1167,7 +1167,7 @@ Proof.
     unfold Z.succ. rewrite plus_IZR. lra.
 Qed.
 
-Lemma Rabs_le_rev : forall {a} {b}, (Rabs a <= b -> -b <= a <= b)%R.
+Lemma Rabs_le_rev : forall a b, (Rabs a <= b -> -b <= a <= b)%R.
 Proof.
   intros a b ABS.
   unfold Rabs in ABS.
@@ -1179,7 +1179,7 @@ Theorem ZofB_ne_range:
 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_rev _ _ ABS).
   lra.
 Qed.
 
-- 
cgit 


From 841fff988e26eb44f7aceeab1d77be5833873625 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Sun, 12 Dec 2021 13:11:59 +0100
Subject: progress on lemmas

---
 lib/IEEE754_extra.v | 82 ++++++++++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 81 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index a76daab4..7e0e7260 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -1174,7 +1174,7 @@ Proof.
   destruct Rcase_abs in ABS; lra.
 Qed.
 
-Theorem ZofB_ne_range:
+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.
@@ -1183,6 +1183,86 @@ Proof.
   lra.
 Qed.
 
+(*
+Theorem ZofB_ne_minus:
+  forall minus_nan m f p q,
+  ZofB_ne f = Some p -> 0 <= p < 2*q -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
+  ZofB_ne (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) = Some (p - q).
+Proof.
+  intros.
+  assert (Q: -2^prec <= q <= 2^prec).
+  { split; auto.  generalize (Zpower_ge_0 radix2 prec); simpl; lia. }
+  assert (RANGE: (IZR p -1/2 <= B2R _ _ f <= IZR p + 1/2)%R) by ( apply ZofB_ne_ball; auto ).    
+  rewrite ZofB_ne_correct in H. destruct (is_finite prec emax f) eqn:FIN; try discriminate.
+  assert (PQ2: (IZR p + 1 <= IZR q * 2)%R).
+  { l_IZR. apply IZR_le. lia. }
+  assert (EXACT: round radix2 fexp (round_mode m) (B2R _ _ f - IZR q)%R = (B2R _ _ f - IZR q)%R).
+  { apply round_generic. apply valid_rnd_round_mode.
+    apply sterbenz_aux. now apply FLT_exp_valid. apply FLT_exp_monotone. apply generic_format_B2R.
+    apply integer_representable_n. auto. lra. }
+  destruct (BofZ_exact q Q) as (A & B & C).
+  generalize (Bminus_correct _ _ _ Hmax minus_nan m f (BofZ q) FIN B).
+  rewrite Rlt_bool_true.
+- fold emin; fold fexp. intros (D & E & F).
+  rewrite ZofB_ne_correct. rewrite E. rewrite D. rewrite A. rewrite EXACT.
+  inversion H. f_equal.
+  rewrite ! Ztrunc_floor. apply Zfloor_minus.
+  lra. lra.
+- rewrite A. fold emin; fold fexp. rewrite EXACT.
+  apply Rle_lt_trans with (bpow radix2 prec).
+  apply Rle_trans with (IZR q). apply Rabs_le. lra.
+  rewrite <- IZR_Zpower. apply IZR_le; auto. red in prec_gt_0_; lia.
+  apply bpow_lt. auto.
+Qed.
+ *)
+
+Definition ZofB_ne_range (f: binary_float) (zmin zmax: Z): option Z :=
+  match ZofB_ne f with
+  | None => None
+  | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None
+  end.
+
+Theorem ZofB_ne_range_correct:
+  forall f min max,
+  let n := ZnearestE (B2R _ _ f) in
+  ZofB_ne_range f min max =
+  if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None.
+Proof.
+  intros. unfold ZofB_ne_range. rewrite ZofB_ne_correct. fold n.
+  destruct (is_finite prec emax f); auto.
+Qed.
+
+Lemma ZofB_ne_range_inversion:
+  forall f min max n,
+  ZofB_ne_range f min max = Some n ->
+  min <= n /\ n <= max /\ ZofB_ne f = Some n.
+Proof.
+  intros. rewrite ZofB_ne_range_correct in H. rewrite ZofB_ne_correct.
+  destruct (is_finite prec emax f); try discriminate.
+  set (n1 := ZnearestE (B2R _ _ f)) in *.
+  destruct (min <=? n1) eqn:MIN; try discriminate.
+  destruct (n1 <=? max) eqn:MAX; try discriminate.
+  simpl in H. inversion H. subst n.
+  split. apply Zle_bool_imp_le; auto.
+  split. apply Zle_bool_imp_le; auto.
+  auto.
+Qed.
+
+
+(*
+Theorem ZofB_ne_range_minus:
+  forall minus_nan m f p q,
+  ZofB_ne_range f 0 (2 * q - 1) = Some p -> q <= 2^prec -> (IZR q <= B2R _ _ f)%R ->
+  ZofB_ne_range (Bminus _ _ _ Hmax minus_nan m f (BofZ q)) (-q) (q - 1) = Some (p - q).
+Proof.
+  intros. destruct (ZofB_ne_range_inversion _ _ _ _ H) as (A & B & C).
+  set (f' := Bminus prec emax prec_gt_0_ Hmax minus_nan m f (BofZ q)).
+  assert (D: ZofB_ne f' = Some (p - q)).
+  { apply ZofB_ne_minus. auto. lia. auto. auto. }
+  unfold ZofB_range. rewrite D. rewrite Zle_bool_true by lia. rewrite Zle_bool_true by lia. auto.
+Qed.
+ *)
+
 (** ** Algebraic identities *)
 
 (** Commutativity of addition and multiplication *)
-- 
cgit 


From 5e83a412e68916f02d86f6e7b719cd93d50c152d Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Sun, 12 Dec 2021 13:13:09 +0100
Subject: _ne conversions

---
 lib/Floats.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib')

diff --git a/lib/Floats.v b/lib/Floats.v
index 9ee5302d..bc066b20 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -360,6 +360,15 @@ Definition to_long (f:float): option int64 := (**r conversion to signed 64-bit i
 Definition to_longu (f:float): option int64 := (**r conversion to unsigned 64-bit int *)
   option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned).
 
+Definition to_int_ne (f:float): option int := (**r conversion to signed 32-bit int *)
+  option_map Int.repr (ZofB_ne_range _ _ f Int.min_signed Int.max_signed).
+Definition to_intu_ne (f:float): option int := (**r conversion to unsigned 32-bit int *)
+  option_map Int.repr (ZofB_ne_range _ _ f 0 Int.max_unsigned).
+Definition to_long_ne (f:float): option int64 := (**r conversion to signed 64-bit int *)
+  option_map Int64.repr (ZofB_ne_range _ _ f Int64.min_signed Int64.max_signed).
+Definition to_longu_ne (f:float): option int64 := (**r conversion to unsigned 64-bit int *)
+  option_map Int64.repr (ZofB_ne_range _ _ f 0 Int64.max_unsigned).
+
 Definition of_int (n:int): float := (**r conversion from signed 32-bit int *)
   BofZ 53 1024 __ __ (Int.signed n).
 Definition of_intu (n:int): float:= (**r conversion from unsigned 32-bit int *)
-- 
cgit 


From 1ecddb62bc5aa8e6a1f6c1a1a2da2e2a8e2b100f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Sun, 12 Dec 2021 15:18:18 +0100
Subject: Values: conversions to nearest int

---
 lib/Floats.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib')

diff --git a/lib/Floats.v b/lib/Floats.v
index bc066b20..b12c6585 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -1145,6 +1145,15 @@ Definition to_long (f:float32): option int64 := (**r conversion to signed 64-bit
 Definition to_longu (f:float32): option int64 := (**r conversion to unsigned 64-bit int *)
   option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned).
 
+Definition to_int_ne (f:float32): option int := (**r conversion to signed 32-bit int *)
+  option_map Int.repr (ZofB_ne_range _ _ f Int.min_signed Int.max_signed).
+Definition to_intu_ne (f:float32): option int := (**r conversion to unsigned 32-bit int *)
+  option_map Int.repr (ZofB_ne_range _ _ f 0 Int.max_unsigned).
+Definition to_long_ne (f:float32): option int64 := (**r conversion to signed 64-bit int *)
+  option_map Int64.repr (ZofB_ne_range _ _ f Int64.min_signed Int64.max_signed).
+Definition to_longu_ne (f:float32): option int64 := (**r conversion to unsigned 64-bit int *)
+  option_map Int64.repr (ZofB_ne_range _ _ f 0 Int64.max_unsigned).
+
 Definition of_int (n:int): float32 := (**r conversion from signed 32-bit int to single-precision float *)
   BofZ 24 128 __ __ (Int.signed n).
 Definition of_intu (n:int): float32 := (**r conversion from unsigned 32-bit int to single-precision float *)
-- 
cgit 


From ff28b8ca5249e8c4ff0ec519673f71a382e816ad Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Thu, 13 Jan 2022 00:07:39 +0100
Subject: moved functions to a more logical place

---
 lib/IEEE754_extra.v | 344 +++++++++++++++++++++++++++-------------------------
 1 file changed, 179 insertions(+), 165 deletions(-)

(limited to 'lib')

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.
 
-- 
cgit 


From df6918762b58dcda4913d7f15b61bd64673af567 Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 11 Feb 2022 17:56:31 +0100
Subject: moved stuff to appropriate places and removed irrelevant content

---
 lib/IEEE754_extra.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'lib')

diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v
index 636ea1ff..35feb29d 100644
--- a/lib/IEEE754_extra.v
+++ b/lib/IEEE754_extra.v
@@ -29,6 +29,24 @@ Require Import Coq.Logic.FunctionalExtensionality.
 Local Open Scope Z_scope.
 
 
+Lemma Znearest_lub :
+  forall choice (n : Z) (x : R), (IZR n <= x)%R -> (n <= Znearest choice x)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zfloor_lub n x BND).
+  pose proof (Znearest_ge_floor choice x).
+  lia.
+Qed.
+
+Lemma Znearest_glb :
+  forall choice (n : Z) (x : R), (x <= IZR n)%R -> (Znearest choice x <= n)%Z.
+Proof.
+  intros until x. intro BND.
+  pose proof (Zceil_glb n x BND).
+  pose proof (Znearest_le_ceil choice x).
+  lia.
+Qed.
+
 Lemma Znearest_IZR :
   forall choice n, (Znearest choice (IZR n)) = n.
 Proof.
-- 
cgit