Coquelicot

Coquelicot is a 3-year research project funded by the Fondation de Coopération Scientifique «Campus Paris-Saclay» and Digiteo. Its goal is to create a new Coq library for Reals.

We provide a user-friendly Coq library for real analysis called Coquelicot.

An easier way of writing formulas and theorem statements is achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals, two-dimensional differentiability, asymptotic behaviors. It also offers some automations for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and we provide correspondence theorems between the two libraries. We have exercised the library on several use cases: in an exam at university entry level, for the definitions and properties of Bessel functions, and for the solution of the one-dimensional wave equation.

This Coq library is freely available: you may click here to download the latest version (3.0.1, compatible with Coq 8.5 to 8.7) or browse the library.

There is a mailing list for users: coquelicot-friends@lists.gforge.inria.fr, more information at http://lists.gforge.inria.fr/mailman/listinfo/coquelicot-friends.