progress in proofs

1 files changed, 25 insertions, 0 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 9baa3f94..e025fa94 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -406,4 +406,29 @@ Theorem rough_approx_div_longu_correct :
       (rough_approx_div_longu (Vlong a) (Vlong b)) = Vlong q /\
         (Z.abs ((Int64.unsigned a) - (Int64.unsigned q) * (Int64.unsigned b)) <= rough_approx_div_thresh)%Z.
 Proof.
+  intros a b b_RANGE.
+  unfold rough_approx_div_longu.
+  destruct (rough_approx_inv_longu_correct b b_RANGE) as (f & C1R & C1F & C1D).
+  rewrite C1R.
+  cbn.
+  Local Transparent Float.to_longu Float.mul.
+  unfold Float.to_longu, Float.mul, Float.of_longu.
+  set (re := (@eq_refl Datatypes.comparison Lt)).
+
+  pose proof (Int64.unsigned_range a) as a_RANGE.
+  change Int64.modulus with 18446744073709551616%Z in a_RANGE.
+  set (a' := Int64.unsigned a) in *.
+  assert (0 <= IZR a' <= 18446744073709551615)%R as IZR_a_RANGE.
+  { split ; apply IZR_le; lia.
+  }
+
+  pose proof (BofZ_correct 53 1024 re re a') as C2.
+  rewrite Rlt_bool_true in C2; cycle 1.
+  { clear C2.
+    apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  destruct C2 as (C2R & C2F & _).
 Admitted.