Coquelicot: A User-Friendly Library of Real Analysis for Coq

International audienceReal 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 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.L'analyse réelle est utilisée dans de nombreux domaines pour modéliser des systèmes physiques ou socio-économiques. Pour cette raison, elle est implémentée dans de nombreux assistants de preuve afin que les utilisateurs disposent d'un moyen de vérifier formellement des théorèmes mathématiques et l'exactitude des systèmes critiques. Le système Coq contient une axiomatisation des nombres réels standard et une bibliothèque de théorèmes sur l'analyse réelle. Malheureusement, de nombreux résultats largement utilisé sont absents de cette bibliothèque. Par exemple, les séries entières ne sont pas développées au delà de leur définition. En outre, les définitions des intégrales et des dérivés sont basées sur les types dépendants, qui les rendent particulièrement difficiles à utiliser en pratique. Pour pallier ces insuffisances, nous avons conçu une bibliothèque conviviale : Coquelicot. Un moyen plus facile d'écrire des formules et déclarations théorème est réalisée en s'appuyant sur des fonctions totales au lieu de types dépendants pour les limites, dérivées, intégrales, séries entières, etc. Pour aider dans la réalisation de démonstrations, la bibliothèque contient un ensemble complet de théorèmes qui couvrent non seulement ces notions, mais aussi quelques extensions comme les intégrales paramétriques, la différentiabilité en deux dimensions et les comportements asymptotiques. Il offre également certaines automatisations pour effectuer les épreuves de différentiabilité. En outre, Coquelicot est une extension conservatrice de la bibliothèque standard de Coq et nous fournissons les théorèmes de correspondance entre les deux bibliothèques. Nous avons testé la bibliothèque sur plusieurs cas d'utilisation : sur le baccalauréat de Mathématiques, sur les définitions et propriétés des fonctions de Bessel, et sur la solution de l'équation d'onde unidimensionnelle