Skip to content

math-comp/analysis

Repository files navigation

Analysis library compatible with Mathematical Components

Docker CI Chat

This repository contains an experimental library for real analysis for the Coq proof-assistant and using the Mathematical Components library.

Meta

Building and installation instructions

The easiest way to install the latest released version of Analysis library compatible with Mathematical Components is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-analysis

To instead build and install manually, 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 (documentation for the last version, using coq2html).

Overview presentation: Classical Analysis with Coq (2018)

See also "Related publication(s)" above.

Other work using MathComp-Analysis:

Mathematical structures

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.)

Main_inheritance_graph

Hierarchies of functions

Functions Functions with a finite image Measures Kernels
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)

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. topology.v and normedtype.v contained a reimplementation of 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 from various authors).

Our proof of Zorn's Lemma in classical_sets.v (NB: new filename) is a reimplementation of the one by Daniel Schepler (https://github.com/coq-community/zorns-lemma); we also took inspiration from his 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