Library Flocq.Calc.Fcalc_div

This file is part of the Flocq formalization of floating-point arithmetic in Coq:

Copyright (C) 2010-2011 Sylvie Boldo
Copyright (C) 2010-2011 Guillaume Melquiond

This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Helper function and theorem for computing the rounded quotient of two floating-point numbers.

Require Import Fcore_Raux.
Require Import Fcore_defs.
Require Import Fcore_float_prop.
Require Import Fcore_digits.
Require Import Fcalc_bracket.
Require Import Fcalc_digits.

Section Fcalc_div.

Variable beta : radix.
Notation bpow e := (bpow beta e).

Computes a mantissa of precision p, the corresponding exponent, and the position with respect to the real quotient of the input floating-point numbers.

The algorithm performs the following steps:
  • Shift dividend mantissa so that it has at least p2 + p digits.
  • Perform the Euclidean division.
  • Compute the position according to the division remainder.
Complexity is fine as long as p1 <= 2p and p2 <= p.

Definition Fdiv_core prec m1 e1 m2 e2 :=
  let d1 := Zdigits beta m1 in
  let d2 := Zdigits beta m2 in
  let e := (e1 - e2)%Z in
  let (m, e') :=
    match (d2 + prec - d1)%Z with
    | Zpos p => (m1 * Zpower_pos beta p, e + Zneg p)%Z
    | _ => (m1, e)
    end in
  let '(q, r) := Zdiv_eucl m m2 in
  (q, e', new_location m2 r loc_Exact).

Theorem Fdiv_core_correct :
  forall prec m1 e1 m2 e2,
  (0 < prec)%Z ->
  (0 < m1)%Z -> (0 < m2)%Z ->
  let '(m, e, l) := Fdiv_core prec m1 e1 m2 e2 in
  (prec <= Zdigits beta m)%Z /\
  inbetween_float beta m e (F2R (Float beta m1 e1) / F2R (Float beta m2 e2)) l.

End Fcalc_div.