some progress

1 files changed, 25 insertions, 1 deletions

diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v
index 7f7aa71a..63b48140 100644
--- a/kvx/FPDivision64.v
+++ b/kvx/FPDivision64.v
@@ -1213,6 +1213,23 @@ Proof.
   lia.
 Qed.
 
+Lemma function_ite :
+  forall {A B : Type} (fn : A->B) (b : bool) (x y: A),
+    fn (if b then x else y) = (if b then fn x else fn y).
+Proof.
+  intros.
+  destruct b; reflexivity.
+Qed.
+
+Lemma normalize_ite :
+  forall ty (b : bool) x y,
+    Val.normalize (if b then x else y) ty =
+      (if b then Val.normalize x ty else Val.normalize y ty).
+Proof.
+  intros.
+  destruct b; reflexivity.
+Qed.
+  
 Lemma step2_div_long_smalla_correct :
     forall a b
       (a_SMALL : (Z.abs (Int64.signed a) <= smalla_thresh)%Z)
@@ -1237,8 +1254,8 @@ Proof.
   assert ((Int64.min_signed <=? ZnearestE (B2R 53 1024 q))=true)%Z as q_LOW.
   { apply Zle_imp_le_bool.
     change Int64.min_signed with (-9223372036854775808)%Z.
-  set (q' :=  B2R 53 1024 q) in *.
     apply Znearest_lub.
+    set (q' :=  B2R 53 1024 q) in *.
     replace q' with (IZR a' / IZR b' + (q' - IZR a' / IZR b'))%R by ring.
     unfold smalla_thresh in a_RANGE'.
     gappa.
@@ -1261,3 +1278,10 @@ Proof.
   rewrite q_LOW.
   rewrite q_HIGH.
   cbn.
+  rewrite normalize_ite.
+  cbn.
+  rewrite <- (function_ite Vlong).
+  f_equal.
+  set (q' :=  B2R 53 1024 q) in *.
+  
+