From 9bb316c0f32cd88cd95895111401ff7995938fec Mon Sep 17 00:00:00 2001
From: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Mon, 24 Jan 2022 15:47:56 +0100
Subject: progress

---
 kvx/FPDivision64.v | 42 +++++++++++++++++++++++++++++++-----------
 1 file changed, 31 insertions(+), 11 deletions(-)

(limited to 'kvx/FPDivision64.v')

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 23cf73e3..0d11c3cb 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1269,7 +1269,8 @@ Qed.
 Lemma step2_div_long_smalla_correct :
     forall a b
       (a_SMALL : (Z.abs (Int64.signed a) <= smalla_thresh)%Z)
-      (b_NOT0 : (0 < Int64.unsigned b)%Z),
+      (b_NOT0 : (0 < Int64.unsigned b)%Z)
+      (b_NOT_VERY_BIG : (Int64.unsigned b <= Int64.max_signed)%Z),
       step2_div_long (Vlong a) (Vlong b) = Vlong (Int64.repr (Int64.signed a / Int64.unsigned b))%Z.
 Proof.
   intros.
@@ -1344,20 +1345,39 @@ Proof.
   fold a'.
   rewrite signed_repr_sub.
 
-  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.
-  
-  destruct (Z_lt_dec 0).
-  - replace ( _ >? _ )%Z with true by lia. reflexivity.
-  - replace ( _ >? _ )%Z with false by lia. reflexivity.
+  pose proof (find_quotient a' b' b_NOT0 q' HALF) as QUOTIENT.
+  fold q'' in QUOTIENT.
+  cbn zeta in QUOTIENT.
+
+  assert (b' <> 0)%Z as NONZ by lia.
+  pose proof (Zmod_eq_full a' b' NONZ) as MOD.
+  assert (b' > 0)%Z as b_GT0 by lia.
+  pose proof (Z_mod_lt a' b' b_GT0) as MOD_LT.
+  destruct (Z_lt_dec a' (b' * q'')) as [LT | GE].
+  { replace (b' * q'' >? a')%Z with true in QUOTIENT by lia.
+    replace q'' with (1 + (a' / b'))%Z by lia.
+    replace ((1 + a' / b') * b' - a')%Z
+      with (-(a' - a' / b' * b')+b')%Z by ring.
+    rewrite <- MOD.
+    rewrite Int64.signed_repr; cycle 1.
+    { admit.
+    }
+    rewrite zlt_true by lia.
+    ring.
+  }
+  replace (b' * q'' >? a')%Z with false in QUOTIENT by lia.
+  rewrite <- QUOTIENT.
+  replace (a' / b' * b' - a')%Z with (-(a' - a' / b' * b'))%Z by ring.
+  rewrite <- MOD.
+  rewrite Int64.signed_repr ; cycle 1.
+  { admit.
+  }
+  rewrite zlt_false by lia.
+  reflexivity.
 Admitted.
-- 
cgit