Certified Exact Transcendental Real Number Computation in Coq
Logic in Computer Science
2010-08-04 v1 Mathematical Software
Numerical Analysis
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.
Keywords
Cite
@article{arxiv.0805.2438,
title = {Certified Exact Transcendental Real Number Computation in Coq},
author = {Russell O'Connor},
journal= {arXiv preprint arXiv:0805.2438},
year = {2010}
}
Comments
This paper is to be part of the proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008)