From fc58331d1aa0c1379df8b17d52f71b07d80c3045 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 12 Jan 2022 15:37:43 +0100 Subject: give a name --- kvx/FPDivision64.v | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 81d587f7..e8e7f8be 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -463,12 +463,16 @@ Definition rough_approx_div_longu a b := Definition smallb_threshold := 4398046511104%Z. Definition rough_approx_div_longu_smallb_delta := 3917010173952%Z. +Definition step1_real_quotient (a b : R) := + rd ((rd a) * (rd (rs (1 / rs b)))). + Theorem rough_approx_div_longu_correct: forall a b, (1 < Int64.unsigned b)%Z -> exists (q : float), (rough_approx_div_longu (Vlong a) (Vlong b)) = Vfloat q /\ - (B2R _ _ q) = rd (rd (IZR (Int64.unsigned a)) * (rd (rs (1 / rs (IZR (Int64.unsigned b)))))) /\ + (B2R _ _ q) = step1_real_quotient (IZR (Int64.unsigned a)) + (IZR (Int64.unsigned b)) /\ is_finite _ _ q = true /\ Bsign _ _ q = false. Proof. -- cgit