progress in proof

1 files changed, 34 insertions, 52 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 906ad650..76e21e54 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -461,10 +461,7 @@ Proof.
 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))).
-
-Definition rough_approx_div_thresh := 1649267441663%Z.
+  Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b).
 
 Lemma Bsign_false_nonneg:
   forall prec emax f,
@@ -502,15 +499,19 @@ Proof.
   lia.
 Qed.
   
+Definition rough_approx_div_thresh := 1%R.
 
 Theorem rough_approx_div_longu_correct :
   forall a b,
     (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.
+    exists (q : float),
+      (rough_approx_div_longu (Vlong a) (Vlong b)) = Vfloat q /\
+        (Rabs (B2R _ _ q - (IZR (Int64.unsigned a)) / (IZR (Int64.unsigned b)))
+         <= rough_approx_div_thresh)%R /\
+        is_finite _ _ q = true /\
+        Bsign _ _ q = false.
 Proof.
-  intros a b b_NOT01.
+  intros a b b_NON01.
   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).
@@ -528,12 +529,6 @@ 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 *.
@@ -541,6 +536,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.
+  }
+
   set (f_r := (B2R _ _ f)) in *.
   assert (0 <= f_r <= 4194305/8388608)%R as f_RANGE.
   { split.
@@ -559,7 +560,7 @@ Proof.
     cbn.
     gappa.
   }
-  destruct C2 as (C2R & C2F & _).
+  destruct C2 as (C2R & C2F & C2S).
 
   pose proof (Bmult_correct  53 1024 re re Float.binop_nan mode_NE
                              (BofZ 53 1024 re re a') f) as C3.
@@ -576,43 +577,24 @@ Proof.
   rewrite C1F in C3.
   rewrite C2F in C3.
   cbn in C3.
-  destruct C3 as (C3R & C3F & _).
+  destruct C3 as (C3R & C3F & C3S).
+
+  econstructor. split. reflexivity.
+  rewrite C3R.
+  rewrite C2R.
+  rewrite C3S.
+  rewrite C2S.
+  rewrite C1S.
+  rewrite C3F.
+  rewrite Zlt_bool_false by lia.
+  split. 2: auto; fail.
 
-  pose proof (ZofB_ne_range_correct 53 1024
-               (Bmult 53 1024 re re Float.binop_nan mode_NE
-                      (BofZ 53 1024 re re a') f) 0 Int64.max_unsigned) as C4.
-  rewrite C3F in C4.
-  rewrite C3R in C4.
-  rewrite C2R in C4.
-
-  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))) 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 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.
-  }
-  cbn in C4.
-  change Int64.max_unsigned with 18446744073709551615%Z.
-  rewrite C4.
   cbn.
-  exists (Int64.repr (ZnearestE y)).
-  split. reflexivity.
-  rewrite Int64.unsigned_repr; cycle 1.
-  { split.
-    - apply Znearest_IZR_le. intuition.
-    - apply Znearest_le_IZR. intuition.
-  }
-  
+  unfold rough_approx_div_thresh.
+  fold f_r.
+  set (rd := round radix2 (FLT_exp (-1074) 53) ZnearestE).
+  replace (rd (rd (IZR a') * f_r) - IZR a' / IZR b')%R with
+   ((rd (rd (IZR a') * f_r) - (rd (IZR a') * f_r))
+    + ((rd (IZR a') - IZR a') * f_r)
+    + (IZR a') * (f_r - 1 / IZR b'))%R by (field ; lra).
 Admitted.