Computer certified efficient exact reals in Coq

TL;DR

This paper presents an optimized implementation of exact real numbers in Coq, leveraging dyadic rationals and approximate division to significantly improve computational efficiency and usability.

Contribution

It introduces a novel Coq library for exact reals using dyadic rationals and type classes, achieving over 100x speedup and enhancing mathematical interface design.

Findings

Over 100 times speedup in basic operations

Use of dyadic rationals from machine integers

First application of type classes in heavy computation

Abstract

Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-implementation by O'Connor in two ways: we use dyadic rationals built from the machine integers and we optimize computation of power series by using approximate division. Moreover, we use type classes for clean mathematical interfaces. This appears to be the first time that type classes are used in heavy computation. We obtain over a 100 times speed up of the basic operations and indications for improving the Coq system.