diff options
| -rw-r--r-- | kvx/FPDivision64.v | 6 |
1 files changed, 5 insertions, 1 deletions
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. |