some more proof

1 files changed, 47 insertions, 7 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 1dbf2782..4d9f0537 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -296,8 +296,8 @@ Theorem rough_approx_inv_longu_correct :
     exists (f : float),
       (rough_approx_inv_longu (Vlong b)) = Vfloat f /\
         is_finite _ _ f = true /\
-        (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= rough_approx_inv_thresh)%R (* /\
-        Bsign _ _ f = false. *)
+        (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= rough_approx_inv_thresh)%R /\
+        Bsign _ _ f = false.
 Proof.
   intros b NONZ.
   unfold rough_approx_inv_longu.
@@ -362,8 +362,6 @@ Proof.
   pose proof (C2Sz NAN) as C2S.
   clear C2Sz.
   
-  apply is_finite_not_is_nan in C2S.
-
   assert ((1/18446744073709551616 <= B2R 24 128 invb_s <= 1)%R) as invb_s_RANGE.
   { rewrite C2R.
     set (r_b_s := B2R 24 128 b_s) in *.
@@ -385,7 +383,7 @@ Proof.
     gappa.
   }
   
-  destruct C3 as (C3R & C3F & _).
+  destruct C3 as (C3R & C3F & C3S).
   set (invb_d :=  (Bconv 24 128 53 1024 re re Float.of_single_nan mode_NE invb_s)) in *.
   assert ((1/18446744073709551616 <= B2R 53 1024 invb_d <= 1)%R) as invb_d_RANGE.
   { 
@@ -394,8 +392,9 @@ Proof.
     cbn.
     gappa.
   }
+  rewrite C2S in C3S.
 
-  split. assumption.
+  split. assumption. split. 2: assumption.
   unfold rough_approx_inv_thresh.
   rewrite C3R.
   rewrite C2R.
@@ -411,6 +410,22 @@ Definition rough_approx_div_longu a b :=
 
 Definition rough_approx_div_thresh := 1649267441663%Z.
 
+Lemma Bsign_false_nonneg:
+  forall prec emax f,
+    (Bsign prec emax f) = false -> (0 <= (B2R prec emax f))%R.
+Proof.
+  intros until f. intro SIGN.
+  destruct f.
+  1, 2, 3: cbn; lra.
+  cbn.
+  apply F2R_ge_0.
+  cbn.
+  cbn in SIGN.
+  rewrite SIGN.
+  cbn.
+  lia.
+Qed.
+
 Theorem rough_approx_div_longu_correct :
   forall a b,
     (0 < Int64.unsigned b)%Z ->
@@ -420,7 +435,7 @@ Theorem rough_approx_div_longu_correct :
 Proof.
   intros a b b_NONZ.
   unfold rough_approx_div_longu.
-  destruct (rough_approx_inv_longu_correct b b_NONZ) as (f & C1R & C1F & C1D).
+  destruct (rough_approx_inv_longu_correct b b_NONZ) as (f & C1R & C1F & C1D & C1S).
   rewrite C1R.
   cbn.
 
@@ -435,6 +450,12 @@ Proof.
   { split ; apply IZR_le; lia.
   }
 
+  set (a_d := (round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a'))).
+  assert (0 <= a_d <= 18446744073709551616)%R as a_d_RANGE.
+  { unfold a_d.
+    gappa.
+  }
+
   pose proof (Int64.unsigned_range b) as b_RANGE.
   change Int64.modulus with 18446744073709551616%Z in b_RANGE.
   set (b' := Int64.unsigned b) in *.
@@ -442,6 +463,19 @@ Proof.
   { split ; apply IZR_le; lia.
   }
 
+  set (f_r := (B2R _ _ f)) in *.
+  assert (0 <= f_r <= 1)%R as f_RANGE.
+  { split.
+    { apply Bsign_false_nonneg. trivial .}
+    unfold rough_approx_inv_thresh in C1D.
+    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.
@@ -482,7 +516,13 @@ Proof.
                  (round_mode mode_NE) (IZR a') * B2R 53 1024 f))
          <= IZR Int64.max_unsigned)%R as q_RANGE.
   { clear C4.
+    cbn.
     change (IZR Int64.max_unsigned) with 18446744073709551615%R.
+    fold a_d.
+    gappa.
+    set (y := ((IZR a') * B2R 53 1024 f)%R).
+    assert ((round radix2 (FLT_exp (-1074) 53) ZnearestE (IZR a') * B2R 53 1024 f) >= 0)%R.
+   
     cbn.
     replace (B2R 53 1024 f)%R with ((B2R 53 1024 f - 1 / IZR b') + 1 / IZR b')%R by ring.
     unfold rough_approx_inv_thresh in C1D.