one less admit

1 files changed, 35 insertions, 7 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index 6b0a0ce8..05d6cee7 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -416,6 +416,10 @@ Proof.
   unfold Float.mul, Float.of_intu in prod.
   set (a' := Int.unsigned a) in *.
   set (b' := Int.unsigned b) in *.
+  assert (IZR_a' : (0 <= IZR a' <= 4294967295)%R).
+  { split; apply IZR_le; lia. }
+  assert (IZR_b' : (1 <= IZR b' <= 4294967295)%R).
+  { split; apply IZR_le; lia. }
   assert (SILLY : -2^53 <= a' <= 2^53).
   { cbn; lia. }
   destruct (BofZ_exact 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) a' SILLY) as (C0E  & C0F & _).
@@ -504,12 +508,40 @@ Proof.
     unfold Int64.sub.
     rewrite Int64.unsigned_repr by (cbn; lia).
     rewrite Int64.unsigned_repr by (cbn; nia).
+    assert(Rabs
+           (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa.
     case Z.ltb_spec; intro CMP.
     - replace (Int64.lt (Int64.repr (a' - prod_r * b')) Int64.zero) with true; cycle 1.
       { unfold Int64.lt.
         change (Int64.signed Int64.zero) with 0.
         rewrite Int64.signed_repr; cycle 1.
-        admit.
+        { cbn.
+          unfold prod_r.
+          rewrite <- C1E in R1.
+          assert (IZR (-9223372036854775808) <= IZR (a' - ZnearestE prod' * b') <= IZR 9223372036854775807)%R.
+          2: split; apply le_IZR; lra.
+          rewrite minus_IZR.
+          rewrite mult_IZR.
+          replace (IZR (ZnearestE prod')) with (prod' + (IZR (ZnearestE prod') - prod'))%R by ring.
+          pose proof (Znearest_imp2 (fun x => negb (Z.even x)) prod') as R2.
+          set (delta1 := (IZR (ZnearestE prod') - prod')%R) in *.
+          replace prod' with ((prod' - IZR a' * inv_b_r) + IZR a' * (inv_b_r - 1 / IZR b')
+                              + IZR a' / IZR b')%R by (field; lra).
+          set (delta2 :=  (inv_b_r - 1 / IZR b')%R) in *.
+          set (delta3 := (prod' - IZR a' * inv_b_r)%R) in *.
+          replace (IZR a' - (delta3 + IZR a' * delta2 + IZR a' / IZR b' + delta1) * IZR b')%R with
+            (- (delta3 + IZR a' * delta2 + delta1) * IZR b')%R by (field; lra).
+          unfold approx_inv_thresh in *.
+          assert (Rabs(IZR a' * delta2) <= 1/4)%R as R4.
+          { apply Rabs_le.
+            split; 
+              nra. }
+          set (delta4 := (IZR a' * delta2)%R) in *.
+          apply Rabs_def2b in R1.
+          apply Rabs_def2b in R2.
+          apply Rabs_def2b in R4.
+          split; nra.
+        }
         rewrite zlt_true by lia.
         reflexivity.
       }
@@ -532,10 +564,6 @@ Proof.
   unfold prod.
   pose proof (Bmult_correct 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) Float.binop_nan mode_NE (BofZ 53 1024 (@eq_refl _ Lt) (@eq_refl _ Lt) a') inv_b) as C2.
   rewrite C0E in C2.
-  assert (IZR_a' : (0 <= IZR a' <= 4294967295)%R).
-  { split; apply IZR_le; lia. }
-  assert (IZR_b' : (1 <= IZR b' <= 4294967295)%R).
-  { split; apply IZR_le; lia. }
   rewrite Rlt_bool_true in C2; cycle 1.
   { clear C2.
     apply (Rabs_relax (bpow radix2 64)).
@@ -557,8 +585,8 @@ Proof.
        (IZR a' * (inv_b_r - 1 / IZR b')))%R by (field ; lra).
   set(delta :=  (inv_b_r - 1 / IZR b')%R) in *.
   cbn. 
-  assert(Rabs
-           (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa.
+  (* assert(Rabs
+           (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - (IZR a' * inv_b_r)) <= 1/512)%R as R1 by gappa. *)
   unfold approx_inv_thresh in *.
   assert (Rabs(IZR a' * delta) <= 3/8)%R as R2.
   { apply Rabs_le.