From 74dec8e174e1a49facaf68d45b3c920c5547123d Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 14:48:59 +0100
Subject: progress

---
 kvx/FPDivision64.v | 24 +++++++++++++++++-------
 1 file changed, 17 insertions(+), 7 deletions(-)

(limited to 'kvx/FPDivision64.v')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 766ff80f..23cf73e3 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1045,8 +1045,7 @@ Qed.
 
 Lemma find_quotient:
   forall (a b : Z)
-         (b_POS : (b > 0)%Z)
-         (invb : R)
+         (b_POS : (0 < b)%Z)
          (qr : R)
          (GAP : (Rabs (IZR a / IZR b - qr) < /2)%R),
     (a / b)%Z =
@@ -1345,9 +1344,20 @@ Proof.
   fold a'.
   rewrite signed_repr_sub.
 
-   
-  
-  Check Int64.signed_repr.
+  rewrite Int64.signed_repr; cycle 1.
+  { admit. }
+
+  assert ((Rabs (IZR a' / IZR b' - q') < / 2)%R) as HALF.
+  { replace (IZR a' / IZR b' - q')%R with
+      (-(q' - IZR a' / IZR b'))%R by ring.
+    rewrite Rabs_Ropp.
+    lra.
+  }
+  rewrite (find_quotient a' b' b_NOT0 q' HALF).
+  fold q''.
+  unfold zlt.
   
-  rewrite find_quotient with (qr := q').
-  cbn.
+  destruct (Z_lt_dec 0).
+  - replace ( _ >? _ )%Z with true by lia. reflexivity.
+  - replace ( _ >? _ )%Z with false by lia. reflexivity.
+Admitted.
-- 
cgit