This repository contains a real analysis library for the Coq proof-assistant. It is based on the Mathematical Components library.
In terms of opam, it comes as the following packages:
coq-mathcomp-classical
: a layer for classical reasoningcoq-mathcomp-analysis
: theories for real analysis
- Author(s):
- Reynald Affeldt (initial)
- Alessandro Bruni
- Yves Bertot
- Cyril Cohen (initial)
- Marie Kerjean
- Assia Mahboubi (initial)
- Damien Rouhling (initial)
- Pierre Roux
- Kazuhiko Sakaguchi
- Zachary Stone
- Pierre-Yves Strub (initial)
- Laurent Théry
- License: CeCILL-C
- Compatible Coq versions: Coq 8.18 to 8.19 (or dev)
- Additional dependencies:
- Coq namespace:
mathcomp.analysis
The easiest way to install the latest released version of MathComp-Analysis library is via the opam package manager:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-analysis
Note that the package coq-mathcomp-classical
will be installed as a dependency.
To build and install manually, make sure that the dependencies are met and do:
git clone https://github.com/math-comp/analysis.git
cd analysis
make # or make -j <number-of-cores-on-your-machine>
make install
Changes are documented systematically in CHANGELOG.md and CHANGELOG_UNRELEASED.md.
We bump the minor part of the version number for breaking changes.
We use deprecation warnings to help transitioning to new versions.
We try to preserve backward compatibility as best as we can.
Each file is documented in its header
(documentation for the last version, using coq2html
).
Overview presentations:
- Classical Analysis with Coq (2018)
- A selection of links to well-known lemmas
- An Introduction to MathComp-Analysis (2024)
Publications about MathComp-Analysis:
- Formalization Techniques for Asymptotic Reasoning in Classical Analysis (2018) doi:10.6092/issn.1972-5787/8124
- Formalisation Tools for Classical Analysis (2019)
- Competing inheritance paths in dependent type theory---a case study in functional analysis (2020) doi:10.1007/978-3-030-51054-1_1
- Measure Construction by Extension in Dependent Type Theory with Application to Integration (2023) doi:10.1007/s10817-023-09671-5
- The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq (2024) doi:10.11309/jssst.41.2_41
Other work using MathComp-Analysis:
- A Formal Classical Proof of Hahn-Banach in Coq (2019)
- Semantics of Probabilistic Programs using s-Finite Kernels in Coq (2023)
- CoqQ: Foundational Verification of Quantum Programs (2023)
- Experimenting with an intrinsically-typed probabilistic programming language in Coq (2023)
MathComp-Analysis adds mathematical structures on top of MathComp's ones.
The following inheritance diagram displays the resulting hierarchy as of version 1.1.0
(excluding most MathComp structures).
The structures introduced by MathComp-Analysis are highlighted.
(See topology.v
, normedtype.v
, reals.v
, measure.v
.)
Functions | Functions with a finite image | Measures | Kernels |
---|---|---|---|
![]() |
![]() |
![]() |
![]() |
(see functions.v ) |
(see cardinality.v , lebesgue_integral.v ) |
(see measure.v , charge.v ) |
(see kernel.v ) |
Detailed requirements and installation procedure
This library was inspired by the Coquelicot library
by Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond.
In the first releases, topology.v
and normedtype.v
contained a reimplementation of the file
Hierarchy.v
from the library Coquelicot.
The instantiation of the mathematical structures of the Mathematical Components library
with the real numbers of the standard Coq library used a well-known file (Rstruct.v
)
from the CoqApprox library (with
modifications by various authors).
The proof of Zorn's Lemma in classical_sets.v
(NB: new filename) was a reimplementation
of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma) but it has been rewritten for version 1.3.0;
we also originally took inspiration from Schepler's work on topology (https://github.com/coq-community/topology) for parts
of topology.v
.
ORIGINAL_FILES.md gives more details about the files in the first releases.
Many thanks to various contributors