diff options
| -rw-r--r-- | kvx/FPDivision64.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 608b3710..ffcc1ef9 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -50,7 +50,7 @@ Qed. Theorem approx_inv_longu_correct : forall b, - (1 <= Int64.unsigned b <= 18446744073709551616)%Z -> + (0 < Int64.unsigned b)%Z -> exists (f : float), (approx_inv_longu (Vlong b)) = Vfloat f /\ is_finite _ _ f = true /\ (Rabs((B2R _ _ f) - (1 / IZR (Int64.unsigned b))) <= approx_inv_thresh)%R. @@ -66,7 +66,9 @@ Proof. set (re := (@eq_refl Datatypes.comparison Lt)). change (Int.signed (Int.repr 1)) with 1%Z. set (b' := Int64.unsigned b) in *. - assert(1 <= IZR b' <= 18446744073709551616)%R as RANGE. + pose proof (Int64.unsigned_range b) as RANGE. + change Int64.modulus with 18446744073709551616%Z in RANGE. + assert(1 <= IZR b' <= 18446744073709551616)%R as RANGE'. { split; apply IZR_le; lia. } |