From 9cacc4caa5710f35a7ab73de6aa0ddf849e60d73 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 12 Jan 2022 16:06:35 +0100 Subject: proof of approx for a/b --- kvx/FPDivision64.v | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e8e7f8be..f4d727be 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -464,7 +464,7 @@ 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)))). + rd ((rd (a)) * (rd (rs (1 / rs (b))))). Theorem rough_approx_div_longu_correct: forall a b, @@ -535,7 +535,31 @@ Proof. auto. Qed. - + +Definition smallb_thresh := 4398046511104%Z. + +Definition smallb_approx_range := 1649280000000%R. +Lemma step1_smallb : + forall a b + (a_RANGE : (0 <= a <= 18446744073709551615)%R) + (b_RANGE : (1 <= b <= IZR smallb_thresh)%R), + (Rabs((step1_real_quotient a b) - a/b) <= smallb_approx_range)%R. +Proof. + intros. + unfold smallb_thresh in b_RANGE. + unfold smallb_approx_range. + replace (step1_real_quotient a b - a/b)%R with + ((rd ((rd (a)) * (rd (rs (1 / rs (b))))) + - ((rd (a)) * (rd (rs (1 / rs (b)))))) + + (rd(a)) * (rd (rs (1 / rs (b))) - 1/b) + + (rd(a) - a)/b)%R; cycle 1. + { unfold step1_real_quotient. + field. + lra. + } + gappa. +Qed. + (* Definition rough_approx_div_thresh := 1683627180032%R. -- cgit