Analysis library compatible with Mathematical Components

$Nix CI$

This repository contains a real analysis library for the Coq / Rocq 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 reasoning
coq-mathcomp-reals: real numbers for MathComp
coq-mathcomp-reals-stdlib: compatibility with the real numbers of the Coq standard library
coq-mathcomp-analysis-stdlib: compatibility with the Coq standard library (topology only)
coq-mathcomp-analysis: theories for real analysis
coq-mathcomp-experimental-reals: sequences of real numbers and distributions (experimental)

Meta

Authors
License: CeCILL-C
Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
Additional dependencies:
Coq/Rocq namespace: mathcomp.analysis

Building and installation instructions

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.

Manual installation

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

About the stability of this library

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.

Documentation

Each file is documented in its header in ASCII.

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

Overview presentations:

Publications about MathComp-Analysis:

Other work using MathComp-Analysis:

Development information

Detailed requirements and installation procedure

Developping with nix

Contributing

Previous work reused at the time of the first releases

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.

Acknowledgments

Many thanks to various contributors

License

jmmarulang/analysis

ErrorLooks like something went wrong!

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Languages

Error
Looks like something went wrong!

Packages