finish proof but some admitted stuff

1 files changed, 27 insertions, 4 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index afa31a72..b71c8990 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -35,7 +35,7 @@ Definition approx_inv b :=
   let x := Eop Ofmaddf (invb_d_var ::: alpha ::: invb_d_var ::: Enil) in
   Elet b (Elet invb_d x).
 
-Definition approx_inv_thresh := (1/10)%R.
+Definition approx_inv_thresh := (1/4294967296)%R.
 
 (*
 Lemma BofZ_exact_zero:
@@ -192,11 +192,34 @@ Proof.
   set (bi := IZR b') in *.
   set (invb0 := rd (rs (1/ rs bi))%R) in *.
   set (alpha := (- invb0 * bi + 1)%R) in *.
-  assert (-1/IZR (2^21)%Z <= ((1 / bi) - rd (rs(1/ rs bi)))/(1/bi) <= 1/IZR(2^21)%Z)%R.
-  { unfold rd, rs.
-    cbn.
+  set (alpha' := ((1/bi - rd (rs (1/ rs bi)))/(1/bi))%R) in *.
+  assert (alpha = alpha')%R as expand_alpha.
+  {
+    unfold alpha, alpha', invb0.
+    field.
+    lra.
+  }
+  assert(-1/2097152 <= alpha' <= 1/2097152)%R as alpha_BOUND.
+  { unfold alpha', rd, rs.
     gappa.
   }
+  set (delta := (rd (rd alpha * invb0 + invb0) - (alpha * invb0 + invb0))%R).
+  assert(-1/1125899906842624 <= delta <= 1/1125899906842624)%R as delta_BOUND.
+  { unfold delta, invb0. rewrite expand_alpha. unfold rd, rs.
+    gappa.
+  }
+  replace (rd (rd alpha * invb0 + invb0) - 1/bi)%R with
+    (delta + ((alpha * invb0 + invb0)-1/bi))%R by (unfold delta; ring).
+  replace (alpha * invb0 + invb0 - 1 / bi)%R with (alpha * (invb0 - 1/bi) + (alpha * (1/bi) + invb0 - 1 / bi))%R by ring.
+  replace (alpha * (1 / bi) + invb0 - 1 / bi)%R with 0%R; cycle 1.
+  { unfold alpha.
+    field.
+    lra.
+  }
+  rewrite expand_alpha.
+  unfold invb0, rd, rs, approx_inv_thresh.
+  apply Rabs_le.
+  gappa.
 Admitted.
 
 Definition approx_div a b :=