more proofs on step1 small b

1 files changed, 58 insertions, 1 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index c17e4f1b..fc2050bb 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -568,7 +568,64 @@ Lemma step1_div_longu_a0 :
   forall b,
     (0 < Int64.unsigned b)%Z ->
     (step1_div_longu (Vlong Int64.zero) (Vlong b)) = Vlong Int64.zero.
-Admitted.
+Proof.
+  intros b b_NOT0.
+  unfold step1_div_longu.
+  unfold step1_real_div_longu.
+  destruct (step1_real_inv_longu_correct b b_NOT0) as
+    (f & C1E & C1R & C1F & C1S).
+  rewrite C1E.
+  cbn.
+  unfold Float.to_longu_ne, Float.of_longu, Float.mul.
+  rewrite Int64.unsigned_zero.
+  set (re :=  (@eq_refl Datatypes.comparison Lt)).
+  assert (- 2 ^ 53 <= 0 <= 2 ^ 53)%Z as SILLY by lia.
+  destruct (BofZ_exact 53 1024 re re 0 SILLY) as (C2R & C2F & C2S).
+  
+  pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE
+                            (BofZ 53 1024 re re 0) f) as C3.
+  rewrite C1F in C3.
+  rewrite C2F in C3.
+  rewrite C1S in C3.
+  rewrite C2S in C3.
+  rewrite Z.ltb_irrefl in C3.
+  rewrite Rlt_bool_true in C3; cycle 1.
+  { clear C3.
+    apply Rabs_relax with (b := bpow radix2 64).
+    { apply bpow_lt. lia. }
+    cbn.
+    rewrite Rmult_0_l.
+    gappa.
+  }
+  rewrite C2R in C3.
+  rewrite Rmult_0_l in C3.
+  destruct C3 as (C3R & C3F & C3Sz).
+  change (true && true) with true in C3F.
+  change (xorb false false) with false in C3Sz.
+  assert (is_nan 53 1024
+           (Bmult 53 1024 re re Float.binop_nan mode_NE 
+                  (BofZ 53 1024 re re 0) f) = false) as NAN.
+  { apply is_finite_not_is_nan.
+    assumption.
+  }
+  pose proof (C3Sz NAN) as C3S.
+  clear NAN C3Sz.
+  pose proof ((ZofB_ne_range_correct 53 1024
+             (Bmult 53 1024 re re Float.binop_nan mode_NE
+                    (BofZ 53 1024 re re 0) f) 0 Int64.max_unsigned)) as C4.
+  rewrite C3R in C4.
+  replace (round radix2 (FLT_exp (3 - 1024 - 53) 53) (round_mode mode_NE) 0)
+    with 0%R in C4 by (cbn ; gappa).
+  rewrite Znearest_IZR in C4.
+  cbn zeta in C4.
+  rewrite Z.leb_refl in C4.
+  change (0 <=? Int64.max_unsigned)%Z with true in C4.
+  rewrite andb_true_r in C4.
+  rewrite andb_true_r in C4.
+  rewrite C3F in C4.
+  rewrite C4.
+  reflexivity.
+Qed.
                                          
 Definition smallb_approx_range := 4400000000000%Z.
 Lemma step1_div_longu_correct :