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