From a5df0e05f97f5ce4ee35723089cbd4a83435d37f Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri, 14 Jan 2022 11:39:22 +0100
Subject: some more proof

---
 kvx/FPDivision64.v | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'kvx')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 767e7ae0..6d82ae67 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -953,6 +953,7 @@ Proof.
   gappa.
 Qed.
 
+(*
 Lemma range_up_le :
   forall a x b,
     (IZR a <= IZR x <= (IZR b) - 1)%R ->
@@ -965,6 +966,7 @@ Proof.
   { apply le_IZR. rewrite minus_IZR. lra. }
   lia.
 Qed.
+ *)
 
 Lemma find_quotient:
   forall (a b : Z)
@@ -1015,13 +1017,20 @@ Proof.
   { admit. }
   apply Zdiv_unique with (b := (a - q*b)%Z).
   ring.
-  apply range_up_le.
-  rewrite minus_IZR.
-  rewrite mult_IZR.
-  fold a' b' q'.
   
-  
-  Search (Rabs _ * Rabs _)%R.
+  split.
+  { rewrite Z.mul_comm. lia. }
+  rewrite <- Rabs_Ropp in DELTA.
+  unfold b', q', a' in DELTA.
+  rewrite <- mult_IZR in DELTA.
+  rewrite <- minus_IZR in DELTA.
+  rewrite <- opp_IZR in DELTA.
+  rewrite Rabs_Zabs in DELTA.
+  apply lt_IZR in DELTA.
+  rewrite Z.abs_eq in DELTA by lia.
+  lia.
+Admitted.
+
 Definition step2_real_div_long a b :=
   Val.mulf (Val.maketotal (Val.floatoflong a)) (step1_real_inv_longu b).
 
-- 
cgit