Coquelicot: A user-friendly library of real analysis for Coq. Real analysis is pervasive to many applications, if only because it is a suitable tool for modeling physical or socio-economical systems. As such, its support is warranted in proof assistants, so that the users have a way to formally verify mathematical theorems and correctness of critical systems. The Coq system comes with an axiomatization of standard real numbers and a library of theorems on real analysis. Unfortunately, this standard library is lacking some widely used results. For instance, power series are not developed further than their definition. Moreover, the definitions of integrals and derivatives are based on dependent types, which make them especially cumbersome to use in practice. To palliate these inadequacies, we have designed a user-friendly library: 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 automation 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.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- Immler, Fabian; Traut, Christoph: The flow of ODEs: formalization of variational equation and Poincaré map (2019)
- Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas: Formally verified approximations of definite integrals (2019)
- Affeldt, Reynald; Cohen, Cyril; Rouhling, Damien: Formalization techniques for asymptotic reasoning in classical analysis (2018)
- Bertot, Yves; Rideau, Laurence; Théry, Laurent: Distant decimals of (\pi): formal proofs of some algorithms computing them and guarantees of exact computation (2018)
- Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
- Tassarotti, Joseph; Harper, Robert: Verified tail bounds for randomized programs (2018)
- Boldo, Sylvie; Melquiond, Guillaume: Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system (2017)
- Cohen, Cyril; Rouhling, Damien: A formal proof in Coq of Lasalle’s invariance principle (2017)
- Fulton, Nathan; Mitsch, Stefan; Bohrer, Brandon; Platzer, André: Bellerophon: tactical theorem proving for hybrid systems (2017)
- Li, Wenda; Paulson, Lawrence C.: A formal proof of Cauchy’s residue theorem (2016)
- Mahboubi, Assia; Melquiond, Guillaume; Sibut-Pinote, Thomas: Formally verified approximations of definite integrals (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: a user-friendly library of real analysis for Coq (2015)