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 document has been produced using \({\rm\kern-.15em T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}_{\textsc{macs}}\)(see http://www.texmacs.org)
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bishop, E., Bridges, D.: Constructive Analysis. Grundlehren der mathematischen Wissenschaften, vol. 279. Springer, Heidelberg (1985)
Cruz-Filipe, L.: Constructive Real Analysis: a Type-Theoretical Formalization and Applications. PhD thesis, University of Nijmegen (April 2004)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN: the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004)
Cruz-Filipe, L., Spitters, B.: Program extraction from large proof developments. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 205–220. Springer, Heidelberg (2003)
Cruz-Filipe, L., Letouzey, P.: A large-scale experiment in executing extracted programs. Electr. Notes Theor. Comput. Sci. 151(1), 75–91 (2006)
Geuvers, H., Niqui, M.: Constructive reals in Coq: Axioms and categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 79–95. Springer, Heidelberg (2002)
Gonthier, G.: A computer-checked proof of the four colour theorem. Technical report, Microsoft Research Cambridge (2005)
Hales, T.C.: A computer verification of the Kepler conjecture. In: Proceedings of the International Congress of Mathematicians, Beijing, vol. III, pp. 795–804. Higher Ed. Press (2002)
Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)
Jones, C.: Completing the rationals and metric spaces in LEGO. In: The second annual Workshop on Logical environments, New York, NY, USA, pp. 297–316. Cambridge University Press, Cambridge (1993)
Julien, N.: Certified exact real arithmetic using co-induction in arbitrary integer base. In: Functional and Logic Programming Symposium (FLOPS). LNCS, Springer, Heidelberg (2008)
Muñoz, C., Lester, D.: Real number calculations and theorem proving. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 195–210. Springer, Heidelberg (2005)
Niqui, M., Wiedijk, F.: The “Many Digits” friendly competition (2005), http://www.cs.ru.nl/~milad/manydigits
O’Connor, R.: A monadic, functional implementation of real numbers. Mathematical. Structures in Comp. Sci. 17(1), 129–159 (2007)
Odlyzko, A.M., te Riele, H.J.J.: Disproof of the Mertens conjecture. J. Reine Angew. Math. 357, 138–160 (1985)
Richman, F.: Real numbers and other completions. Math. Log. Q. 54(1), 98–108 (2008)
The Coq Development Team. The Coq Proof Assistant Reference Manual – Version V8.0 (April 2004), http://coq.inria.fr
Weisstein, E.W.: Machin-like formulas. From MathWorld–A Wolfram Web Resource (January 2004), http://mathworld.wolfram.com/Machin-LikeFormulas.html
Williams, R.: Arctangent formulas for PI (December 2002), http://www.cacr.caltech.edu/~roy/upi/pi.formulas.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
O’Connor, R. (2008). Certified Exact Transcendental Real Number Computation in Coq. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2008. Lecture Notes in Computer Science, vol 5170. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71067-7_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-71067-7_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71065-3
Online ISBN: 978-3-540-71067-7
eBook Packages: Computer ScienceComputer Science (R0)