Certified Exact Transcendental Real Number Computation in Coq
arXiv:0805.2438 · doi:10.1007/978-3-540-71067-7_21
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.
This paper is to be part of the proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008)
References in corpus (1)
Cited by in corpus (5)
- Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
- Computer certified efficient exact reals in Coq
- Computable decision making on the reals and other spaces via partiality and nondeterminism
- Classical Mathematics for a Constructive World
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof