some more proofs?

1 files changed, 65 insertions, 2 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 4d9f0537..521cbe0f 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -404,6 +404,62 @@ Proof.
   gappa.
 Qed.
 
+Theorem rough_approx_inv_longu_correct1 :
+  forall b,
+    (Int64.unsigned b = 1%Z) ->
+    exists f,
+    (rough_approx_inv_longu (Vlong b)) = Vfloat f /\
+        is_finite _ _ f = true /\
+        (B2R _ _ f) = 1%R /\
+        Bsign _ _ f = false.
+Proof.
+  intros b ONE.
+  cbn.
+  unfold Float.of_single, ExtFloat32.inv, Float32.div, ExtFloat32.one, Float32.of_longu, Float32.of_int.
+  set (re := (@eq_refl Datatypes.comparison Lt)).
+  rewrite ONE.
+  change (Int.signed (Int.repr 1)) with 1%Z.
+  
+  econstructor.
+  split. reflexivity.
+  split. reflexivity.
+  split. 2: reflexivity.
+  destruct (BofZ_exact 24 128 re re 1%Z) as (C1R & C1F & C1S). lia.
+
+  pose proof (Bdiv_correct 24 128 re re Float32.binop_nan mode_NE 
+                           (BofZ 24 128 re re 1) (BofZ 24 128 re re 1)) as C2.
+  rewrite C1R in C2.
+  rewrite C1F in C2.
+  rewrite C1S in C2.
+  rewrite Rlt_bool_true in C2; cycle 1.
+  { clear C2.
+    apply Rabs_relax with (b := bpow radix2 0%Z).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  assert (1 <> 0)%R as OBVIOUS by lra.
+  destruct (C2 OBVIOUS) as (C2R & C2F & C2S).
+  clear C2.
+
+  pose proof (Bconv_correct 24 128 53 1024 re re Float.of_single_nan mode_NE
+       (Bdiv 24 128 re re Float32.binop_nan mode_NE 
+          (BofZ 24 128 re re 1) (BofZ 24 128 re re 1)) C2F) as C3.
+  rewrite Rlt_bool_true in C3; cycle 1.
+  { clear C3.
+    rewrite C2R.
+    apply Rabs_relax with (b := bpow radix2 0%Z).
+    { apply bpow_lt. lia. }
+    cbn.
+    gappa.
+  }
+  destruct C3 as (C3R & C3F & C3S).
+  rewrite C3R.
+  rewrite C2R.
+  cbn.
+  gappa.
+Qed.
+
 Definition rough_approx_div_longu a b :=
   Val.maketotal (Val.longuoffloat_ne
     (Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b))).
@@ -468,14 +524,21 @@ Proof.
   { split.
     { apply Bsign_false_nonneg. trivial .}
     unfold rough_approx_inv_thresh in C1D.
+    destruct (Z_le_gt_dec b' 1) as [LE | GT].
+    { unfold f_r.
+      assert (b' = 1%Z) as EQ by lia.
+      destruct (rough_approx_inv_longu_correct1 b EQ) as
+        (f2 & OE & OF & OR & OS).
+      replace f2 with f in * by congruence.
+      lra.
+    }
     replace f_r with ((f_r - 1 / IZR b') + 1/ IZR b')%R by (field; lra).
     set (delta := (f_r - 1 / IZR b')%R) in *.
-    destruct (Z_le_gt_dec b' 1) as [LE | GT].
-    { admit. }
     assert (2 <= IZR b')%R as NOT1.
     { apply IZR_le. lia. }
     gappa.
   }
+  
   pose proof (BofZ_correct 53 1024 re re a') as C2.
   rewrite Rlt_bool_true in C2; cycle 1.
   { clear C2.