From bfbd4b7235fe67cc3fa023bcdec88d89ca6f3c99 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 7 Jan 2022 23:05:19 +0100 Subject: nice intervals --- kvx/FPDivision64.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'kvx') 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. } -- cgit