Certified Exact Transcendental Real Number Computation in Coq

TL;DR

This paper presents a Coq library for exact real number computation, enabling automated proofs of inequalities and constructive real number functions, advancing formal reasoning in real analysis within proof assistants.

Contribution

The paper introduces a novel Coq library for exact real number computation and a tactic for automatic inequality proofs, enhancing formal verification capabilities.

Findings

Successfully implemented a constructive real number library in Coq

Developed an automated tactic for proving strict inequalities

Demonstrated correctness of elementary real number functions

Abstract

Reasoning about real number expressions in a proof assistant is challenging. Several problems in theorem proving can be solved by using exact real number computation. I have implemented a library for reasoning and computing with complete metric spaces in the Coq proof assistant and used this library to build a constructive real number implementation including elementary real number functions and proofs of correctness. Using this library, I have created a tactic that automatically proves strict inequalities over closed elementary real number expressions by computation.