This repository contains a real analysis library for the Rocq proof-assistant. It is based on the Mathematical Components library.

In terms of opam, it comes as the following packages:

• rocq-mathcomp-classical: a layer for classical reasoning
• rocq-mathcomp-reals: real numbers for MathComp
• rocq-mathcomp-reals-stdlib: compatibility with the real numbers of the Rocq standard library
• rocq-mathcomp-analysis-stdlib: compatibility with the Rocq standard library (topology only)
• rocq-mathcomp-analysis: theories for real analysis
• rocq-mathcomp-experimental-reals: sequences of real numbers and distributions (experimental)

• Authors
• License: CeCILL-C
• Compatible Rocq versions: Rocq 9.1--9.3 (or dev)
• Additional dependencies:
  • MathComp boot 2.6.0 or later
  • MathComp finite-group 2.6.0 or later
  • MathComp order 2.6.0 or later
  • MathComp algebra 2.6.0 or later
  • MathComp solvable 2.6.0 or later
  • MathComp field 2.6.0 or later
  • MathComp finmap 2.1.0
  • MathComp bigenough 1.0.0
  • Hierarchy Builder 1.8.0 or later
• Coq/Rocq 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 rocq-released https://rocq-prover.org/opam/released
opam install coq-mathcomp-analysis

Note that the packages coq-mathcomp-classical and coq-mathcomp-reals will be installed as dependencies.

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

Each file is documented in its header in ASCII.

HTML rendering of the source code and inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones (using rocqnavi):

• last version: 1.19.0
• master

Overview presentations:

• Classical Analysis with Coq (2018)
• A selection of links to well-known lemmas
• An Introduction to MathComp-Analysis (2022-2025)

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
• A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq (2024)
• Prouver que pi est irrationnel avec MathComp-Analysis (2025)
• Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation (2025)

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) doi:10.1145/3573105.357569
• CoqQ: Foundational Verification of Quantum Programs (2023) doi:10.1145/3571222
• Experimenting with an intrinsically-typed probabilistic programming language in Coq (2023) doi:10.1007/978-981-99-8311-7_9
• Taming Differentiable Logics with Coq Formalisation (2024)
• Décomposition Algébrique Cylindrique en Coq/Rocq (2025)
• Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory (2025)
• Vancomycert: A Certified Neuro-Symbolic Drug Delivery System (Case Study) (2025)
• A Formal Foundation for Equational Reasoning on Probabilistic Programs (2025) doi:10.1007/978-981-95-3585-9_3
• Cylindrical Algebraic Decomposition in Coq/Rocq (2026) doi:10.1145/3779031.3779100
• Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice (2026)

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.

Detailed requirements and installation procedure

Developping with nix

Contributing

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