progress in proofs

1 files changed, 42 insertions, 29 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 521cbe0f..a241e4f0 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -482,15 +482,37 @@ Proof.
   lia.
 Qed.
 
+Lemma Znearest_IZR_le :
+  forall rnd n x, (IZR n <= x)%R -> (n <= Znearest rnd x)%Z.
+Proof.
+  intros until x. intro ORDER.
+  pose proof (Znearest_ge_floor rnd x).
+  pose proof (Zfloor_le _ _ ORDER) as KK.
+  rewrite Zfloor_IZR in KK.
+  lia.
+Qed.
+
+Lemma Znearest_le_IZR :
+  forall rnd n x, (x <= IZR n)%R -> (Znearest rnd x <= n)%Z.
+Proof.
+  intros until x. intro ORDER.
+  pose proof (Znearest_le_ceil rnd x).
+  pose proof (Zceil_le _ _ ORDER) as KK.
+  rewrite Zceil_IZR in KK.
+  lia.
+Qed.
+  
+
 Theorem rough_approx_div_longu_correct :
   forall a b,
-    (0 < Int64.unsigned b)%Z ->
+    (2 <= Int64.unsigned b)%Z ->
     exists (q : int64),
       (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_NONZ.
+  intros a b b_NOT01.
   unfold rough_approx_div_longu.
+  assert (0 < Int64.unsigned b)%Z as b_NONZ by lia.
   destruct (rough_approx_inv_longu_correct b b_NONZ) as (f & C1R & C1F & C1D & C1S).
   rewrite C1R.
   cbn.
@@ -515,27 +537,17 @@ Proof.
   pose proof (Int64.unsigned_range b) as b_RANGE.
   change Int64.modulus with 18446744073709551616%Z in b_RANGE.
   set (b' := Int64.unsigned b) in *.
-  assert (1 <= IZR b' <= 18446744073709551615)%R as IZR_b_RANGE.
+  assert (2 <= IZR b' <= 18446744073709551615)%R as IZR_b_RANGE.
   { split ; apply IZR_le; lia.
   }
 
   set (f_r := (B2R _ _ f)) in *.
-  assert (0 <= f_r <= 1)%R as f_RANGE.
+  assert (0 <= f_r <= 4194305/8388608)%R as f_RANGE.
   { 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 *.
-    assert (2 <= IZR b')%R as NOT1.
-    { apply IZR_le. lia. }
     gappa.
   }
   
@@ -554,8 +566,8 @@ Proof.
   rewrite Rlt_bool_true in C3; cycle 1.
   { clear C3.
     rewrite C2R.
-    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.
+    fold f_r.
+    
     apply Rabs_relax with (b := bpow radix2 65).
     { apply bpow_lt ; lia. }
     cbn.
@@ -573,23 +585,24 @@ Proof.
   rewrite C3R in C4.
   rewrite C2R in C4.
 
-  assert(0 <=
-      (round radix2 (FLT_exp (-1074) 53) ZnearestE
+  set (y := (round radix2 (FLT_exp (-1074) 53) ZnearestE
               (round radix2 (FLT_exp (3 - 1024 - 53) 53) 
-                 (round_mode mode_NE) (IZR a') * B2R 53 1024 f))
-         <= IZR Int64.max_unsigned)%R as q_RANGE.
+                 (round_mode mode_NE) (IZR a') * B2R 53 1024 f))) in *.
+  assert(0 <= y <= IZR Int64.max_unsigned)%R as q_RANGE.
   { clear C4.
+    unfold y.
     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.
-    set (delta :=  (B2R 53 1024 f - 1 / IZR b')%R) in *.
+    fold f_r.
     gappa.
   }
+  cbn in C4.
+  rewrite Zle_imp_le_bool in C4; cycle 1.
+  { apply Znearest_IZR_le. intuition.
+  }
+  rewrite Zle_imp_le_bool in C4; cycle 1.
+  { apply Znearest_le_IZR. intuition.
+  }
+  
+    
 Admitted.