progress

1 files changed, 15 insertions, 6 deletions

diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v
index 28c7fe72..2c0739e1 100644
--- a/kvx/FPDivision.v
+++ b/kvx/FPDivision.v
@@ -84,9 +84,12 @@ Proof.
   set (b_d := (Float.of_longu (Int64.repr b'))) in *.
   Local Transparent Float.of_longu.
   unfold Float.of_longu in b_d.
+
+  assert(SILLY : (- 2 ^ 24 <= 1 <= 2 ^ 24)%Z) by lia.
+  destruct (BofZ_exact 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1 SILLY) as (C0E & C0F & C0S).
+  clear SILLY.
   
-  
-  pose proof (BofZ_correct 24 128 eq_refl eq_refl b') as C1.
+  pose proof (BofZ_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C1.
   rewrite Rlt_bool_true in C1; cycle 1.
   { clear C1. cbn.
     admit.
@@ -99,12 +102,12 @@ Proof.
   fold b' in invb_d.
   Check BofZ.
   change (Int.signed (Int.repr 1%Z)) with 1%Z in invb_d.
-  pose proof (Bdiv_correct 24 128 eq_refl eq_refl Float32.binop_nan mode_NE
-                      (BofZ 24 128 eq_refl eq_refl 1)
-                      (BofZ 24 128 eq_refl eq_refl b')) as C2.
+  pose proof (Bdiv_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) Float32.binop_nan mode_NE
+                      (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)
+                      (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b')) as C2.
   rewrite Rlt_bool_true in C2; cycle 1.
   { clear C2. admit. }
-  assert (B2R 24 128 (BofZ 24 128 eq_refl eq_refl b') <> 0%R) as NONZ.
+  assert (B2R 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') <> 0%R) as NONZ.
   { admit. }
   destruct (C2 NONZ) as (C2E & C2F & C2S).
   clear C2 NONZ.
@@ -163,6 +166,12 @@ Proof.
   destruct C6 as (C6E & C6F & C6S).
   split.
   { exact C6F. }
+  rewrite C6E.
+  rewrite C5E.
+  rewrite C3E.
+  rewrite C2E.
+  rewrite C1E.
+  rewrite C0E.
 Admitted.
 
 Definition approx_div a b :=