diff options
Diffstat (limited to 'kvx')
-rw-r--r-- | kvx/FPDivision64.v | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 9463313a..9cde7d97 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -394,7 +394,7 @@ Proof. Qed. Definition rough_approx_div_longu a b := - Val.maketotal (Val.longuoffloat + Val.maketotal (Val.longuoffloat_ne (Val.mulf (Val.maketotal (Val.floatoflongu a)) (rough_approx_inv_longu b))). Definition rough_approx_div_thresh := 1649267441663%Z. @@ -413,7 +413,7 @@ Proof. cbn. Local Transparent Float.to_longu Float.mul. - unfold Float.to_longu, Float.mul, Float.of_longu. + unfold Float.to_longu_ne, Float.mul, Float.of_longu. set (re := (@eq_refl Datatypes.comparison Lt)). pose proof (Int64.unsigned_range a) as a_RANGE. @@ -452,5 +452,15 @@ Proof. cbn. gappa. } + rewrite C1F in C3. + rewrite C2F in C3. + cbn in C3. + destruct C3 as (C3R & C3F & _). + + 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. Admitted. |