Certified Exact Transcendental Real Number Computation in Coq
It provides a foundational tool for formal verification of real number computations in proof assistants, addressing a long-standing challenge in theorem proving.
The paper presents a Coq library for exact real number computation using complete metric spaces, enabling automatic proof of strict inequalities over elementary real expressions.
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.