The Coquelicot library - The Coquelicot library
Person in charge :
BOLDO Sylvie
Coquelicot is a user-friendly Coq library for real analysist.
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
More information: http://coquelicot.saclay.inria.fr/
Research activities
Formalisation of (Specification and Programming) Languages in Proof Assistants
Members
BOLDO Sylvie MELQUIOND Guillaume LELAY Catherine
Group
Verification of Algorithms, Languages and Systems
