Document Open Access Logo

A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq

Authors Reynald Affeldt , Zachary Stone

PDF
Thumbnail PDF

File

LIPIcs.ITP.2024.5.pdf
  • Filesize: 0.78 MB
  • 19 pages

Document Identifiers

Author Details

Reynald Affeldt
  • National Institute of Advanced Industrial Science and Technology (AIST), Tokyo, Japan
Zachary Stone
  • The MathComp-Analysis development team, Boston, MA, USA

Funding

  • Affeldt, Reynald: The first author acknowledges support of the JSPS KAKENHI Grant Number 22H00520.

Acknowledgements

The authors are grateful to A. Bruni, C. Cohen, Y. Ishiguro, and T. Saikawa for their inputs. This work has benefited from feedback gained during the MathComp-Analysis development meetings. The authors would like to thank the anonymous referees of ITP 2024 for their careful and informative review, as well as the program committee of JFLA 2024 where a preliminary version of this work was presented [Reynald Affeldt and Zachary Stone, 2024].

Cite AsGet BibTex

Reynald Affeldt and Zachary Stone. A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.ITP.2024.5

Abstract

Formalization of real analysis offers a chance to rebuild traditional proofs of important theorems as unambiguous theories that can be interactively explored. This paper provides a comprehensive overview of the Lebesgue Differentiation Theorem formalized in the Coq proof assistant, from which the first Fundamental Theorem of Calculus (FTC) for the Lebesgue integral is obtained as a corollary. Proving the first FTC in this way has the advantage of decomposing into loosely-coupled theories of moderate size and of independent interest that lend themselves well to incremental and collaborative development. We explain how we formalize all the topological constructs and all the standard lemmas needed to eventually relate the definitions of derivability and of Lebesgue integration of MathComp-Analysis, a formalization of analysis developed on top of the Mathematical Components library. In the course of this experiment, we substantially enrich MathComp-Analysis and even devise a new proof for Urysohn’s lemma.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Mathematics of computing → Mathematical analysis
Keywords
  • Coq proof assistant
  • Mathematical Components library
  • Lebesgue integral
  • fundamental theorem of calculus

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Théry. MathComp-Analysis: Mathematical Components compliant analysis library. https://github.com/math-comp/analysis, 2017. Last stable version: 1.2.0 (2024).
  2. Reynald Affeldt and Cyril Cohen. Measure construction by extension in dependent type theory with application to integration. J. Autom. Reason., 67(3):28:1-28:27, 2023. Google Scholar
  3. Reynald Affeldt, Cyril Cohen, and Damien Rouhling. Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason., 11(1):43-76, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8124.
  4. Reynald Affeldt, Cyril Cohen, and Ayumu Saito. Semantics of probabilistic programs using s-finite kernels in Coq. In 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023), Boston, MA, USA, January 16-17, 2023, pages 3-16. ACM, 2023. URL: https://doi.org/10.1145/3573105.3575691.
  5. Reynald Affeldt and Zachary Stone. Towards the fundamental theorem of calculus for the Lebesgue integral in Coq. In 35ème Journées Francophones des Langages Applicatifs (JFLA 2024), Saint-Jacut-de-la-Mer, France, January 30-February 2. January 2024. URL: https://inria.hal.science/hal-04406350/document.
  6. Jeremy Avigad, Johannes Hölzl, and Luke Serafin. A formally verified proof of the central limit theorem. J. Autom. Reason., 59(4):389-423, 2017. URL: https://doi.org/10.1007/s10817-017-9404-x.
  7. Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. Coquelicot: A user-friendly library of real analysis for Coq. Math. Comput. Sci., 9(1):41-62, 2015. URL: https://doi.org/10.1007/S11786-014-0181-1.
  8. Lewis Bowen. Lecture notes in real analysis. Available at https://web.ma.utexas.edu/users/lpbowen/m381c/lecture-notes.pdf, December 2014. University of Texas at Austin.
  9. Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 34:1-34:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.FSCD.2020.34.
  10. Luís Cruz-Filipe. A constructive formalization of the fundamental theorem of calculus. In Selected Papers of the 2nd International Workshop on Types for Proofs and Programs (TYPES 2002), Berg en Dal, The Netherlands, April 24-28, 2002, volume 2646 of Lecture Notes in Computer Science, pages 108-126. Springer, 2002. URL: https://doi.org/10.1007/3-540-39185-1_7.
  11. The MathComp development team. Mathematical components. https://github.com/math-comp/math-comp, 2005. Last stable version: 2.2.0 (2024).
  12. François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. Packaging mathematical structures. In 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17-20, 2009, volume 5674 of Lecture Notes in Computer Science, pages 327-342. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03359-9_23.
  13. Johannes Hölzl, Fabian Immler, and Brian Huffman. Type classes and filters for mathematical analysis in Isabelle/HOL. In 4th International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22-26, 2013, volume 7998 of Lecture Notes in Computer Science, pages 279-294. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39634-2_21.
  14. Yoshihiro Ishiguro and Reynald Affeldt. The Radon-Nikodým theorem and the Lebesgue-Stieltjes measure in Coq. Computer Software, 41(2), 2024. Japan Society for Software Science and Technology. Google Scholar
  15. Samuel Leland Lesseig. Metrization of uniform spaces. Master’s thesis, Department of Mathematics, Kansas State University, Manhattan, Kansas, 1963. Google Scholar
  16. Daniel Li. Notions fondamentales d'analyse réelle et complexe - Espaces de Hardy et interpolation, avec exercices corrigés. Ellipses, 2022. Google Scholar
  17. Assia Mahboubi and Enrico Tassi. Mathematical Components. Zenodo, January 2021. URL: https://doi.org/10.5281/zenodo.4457887.
  18. Mathlib 4. File MeasureTheory/Covering/DensityTheorem.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/MeasureTheory/Covering/DensityTheorem.lean, June 2024.
  19. Mathlib 4. File MeasureTheory/Covering/Differentiation.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/MeasureTheory/Covering/Differentiation.lean, June 2024.
  20. Mathlib 4. File MeasureTheory/Integral/FundThmCalculus.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean, June 2024.
  21. Mathlib 4. File MeasureTheory/Integral/SetIntegral.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/MeasureTheory/Integral/SetIntegral.lean, June 2024.
  22. Mathlib 4. File Topology/TietzeExtension.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/Topology/TietzeExtension.lean, June 2024.
  23. Mathlib 4. File Topology/UrysohnsLemma.lean. https://github.com/leanprover-community/mathlib4/blob/9a2e9d332236861f33e75fb5c398577b0d5ffc70/Mathlib/Topology/UrysohnsLemma.lean, June 2024.
  24. Maran Mohanarangan. The fundamental theorem of calculus for Lebesgue integration. Technical report, ETH Zürich, 2021. Exercise Class 13, Measure and Integration, Spring 2021, available at URL: https://metaphor.ethz.ch/x/2021/fs/401-2284-00L/sc/notes_exclass13.pdf.
  25. NASALib. NASA PVS library of formal developments. Current version: 7.1.1. Available at https://github.com/nasa/pvslib, 2023.
  26. Oliver Nash. A Formalisation of Gallagher’s Ergodic Theorem. In 14th International Conference on Interactive Theorem Proving (ITP 2023), volume 268 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:16, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITP.2023.23.
  27. Ayumu Saito and Reynald Affeldt. Experimenting with an intrinsically-typed probabilistic programming language in Coq. In 21st Asian Symposium on Programming Languages and Systems (APLAS 2023), Taipei, Taiwan, November 26-29, 2023, volume 14405, pages 182-202. Springer, 2023. URL: https://doi.org/10.1007/978-981-99-8311-7_9.
  28. Laurent Schwartz. Analyse III: Calcul intégral. Hermann, 1997. Google Scholar
  29. The Coq Development Team. The Coq Proof Assistant Reference Manual. Inria, 2024. Available at https://coq.inria.fr. Version 8.19.2.
  30. The mathlib Community. The lean mathematical library. In 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), New Orleans, LA, USA, January 20-21, 2020, pages 367-381. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373824.
  31. Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, and Mingsheng Ying. CoqQ: Foundational verification of quantum programs. Proc. ACM Program. Lang., 7(POPL):833-865, 2023. URL: https://doi.org/10.1145/3571222.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact