one less admit

1 files changed, 27 insertions, 2 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index e4e881d0..38f30696 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -529,8 +529,33 @@ Proof.
       rewrite Int64.unsigned_repr by (cbn; lia).
       reflexivity.
   }
-  fold prod'.
-  admit.
+  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.
+  rewrite Rlt_bool_true in C2 by admit.
+  destruct C2 as (C2E & C2F & _).
+  rewrite C2E.
+  fold inv_b_r a' b'.
+  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. }
+  replace ((round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (IZR a' * inv_b_r)) -
+             (IZR a' / IZR b'))%R with
+    (((round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) (IZR a' * inv_b_r)) -
+       (IZR a' * inv_b_r)) +
+       (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.
+  unfold approx_inv_thresh in *.
+  assert (Rabs(IZR a' * delta) <= 3/8)%R as R2.
+  { apply Rabs_le.
+    split; nra.
+  }
+  pose proof (Rabs_triang (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a' * inv_b_r) - IZR a' * inv_b_r)  (IZR a' * delta))%R.
+  lra.
 Admitted.