Formalization Techniques for Asymptotic Reasoning in Classical Analysis
DOI:
https://doi.org/10.6092/issn.1972-5787/8124Keywords:
Formal Proofs, Coq, Classical Analysis, Bachmann-Landau NotationsAbstract
Formalizing analysis on a computer involves a lot of “epsilon-delta” reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable “delta”. We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.
References
Reynald Affeldt, Cyril Cohen, Assia Mahboubi, Damien Rouhling,and Pierre-Yves Strub. Analysis library compatible with Mathematical Components. https://github.com/math-comp/analysis/tree/asymptotic_reasoning_paper, 2018. Work in progress.
Jeremy Avigad and Kevin Donnelly. Formalizing O notation in Isabelle/HOL. In David A. Basin and Michaël Rusinowitch, editors, Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork, Ireland, July 4-8, 2004, Proceedings, volume 3097 of Lecture Notes in Computer Science, pages 357–371. Springer, 2004.
Jean-Marie Arnaudiès and Henri Fraysse. Cours de mathématique, volume 2, Analyse. Dunod, 1988.
Paul Bachmann. Die Analytische Zahlentheorie. B.G. Teubner, 1894.
Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, 9(1):41–62, 2015.
Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. The Coquelicot library. Available at: http://coquelicot.saclay.inria.fr/, Sep 2017. Version 3.0.1.
Cyril Cohen. Formalized algebraic numbers: construction and first-order theory. PhD thesis, École polytechnique, Nov 2012.
The Coq Development Team. The Coq proof assistant reference manual, 2018. Version 8.8.0.
Cyril Cohen and Damien Rouhling. A Formal Proof in Coq of LaSalle’s Invariance Principle. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving - 8th International Conference, ITP 2017, Brasília, Brazil, September 26-29, 2017, Proceedings, volume 10499 of Lecture Notes in Computer Science, pages 148–163. Springer, 2017.
Manuel Eberl. Proving divide and conquer complexities in Isabelle/HOL. Journal of Automated Reasoning, 58(4):483–508, 2017.
Georges Gonthier et al. The Mathematical Components repository. https://github.com/math-comp/math-comp, 2018. Full list of contributors: https://github.com/math-comp/math-comp/blob/ master/etc/AUTHORS. Project started in 2006.
Armaël Guéneau, Arthur Charguéraud, and François Pottier. A fistful of dollars: Formalizing asymptotic complexity claims via deductive program verification. In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 533–560. Springer, 2018.
François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science, pages 327–342. Springer, 2009.
Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning, 3(2):95–152, 2010.
Georges Gonthier, Assia Mahboubi, and Enrico Tassi. A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France, 2016.
Johannes Hölzl, Fabian Immler, and Brian Huffman. Type Classes and Filters for Mathematical Analysis in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors. Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science. Springer, 2013, pages 279–294.
Donald E. Knuth. Letter to the editor of the Notices of the American Mathematical Society. https://www-cs-faculty.stanford.edu/~knuth/calc, Mar 1998.
Edmund Landau. Handbuch der Lehre von der Verteilung der Primzahlen. B.G. Teubner, 1909.
Lean mathematical components library. https://github.com/leanprover/mathlib, 2018. Work in progress.
Assia Mahboubi and Enrico Tassi. Canonical Structures for the Working Coq User. In Blazy et al. [BPP13], pages 19–34.
Assia Mahboubi and Enrico Tassi. Mathematical Components. Available at: https://math-comp.github.io/mcb/, 2016. With contributions by Yves Bertot and Georges Gonthier.
Damien Rouhling. A Formal Proof in Coq of a Control Function for the Inverted Pendulum. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 28–41. ACM, 2018.
The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2018 Reynald Affeldt, Cyril Cohen, Damien Rouhling
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
