Floating-point arithmetic in the Coq system (Q714617)

Floating point arithmetic is not only an important aspect of computation but has also become an important aspect of proofs. Hales' proof of the Kepler conjecture is probably the most famous of such proofs. If these proofs are to be trusted then it is necessary to rely on the correctness of the computations. If they are to be checked formally then the floating point arithmetic must be checked formally as well. In the paper the author introduces the formal foundations of floating-point arithmetic (a radix is fixed and then the number is approximated by two integers, mantissa and exponent with respect to the radix) in the Coq proof development environment. This allows to develop certified algorithms. The main question in floating-point computation is that of its accuracy and rounding plays an important role. After the foundations are laid, addition, multiplication, division, and square root are defined. Next follow elementary functions such as \(\sin\), \(\cos\), \(\exp\) and \(\arctan\). For these functions it is important to reduce the argument to a range in which the corresponding power series converges reasonably fast. A big advantage of using Coq is that the proofs can be checked in a few minutes and then certified algorithms can be used. For this reason, the author rightly motivates his work by the goal to check computational proofs such as Hales' by a formal system.