Catherine LELAY

Abstract: 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 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.

Abstract: In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.

Abstract: Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert's epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq's standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library's in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.

Résumé: La bibliothèque standard de Coq contient de nombreuses définitions et lemmes permettant de faire de l'analyse, seulement ceux-ci se limitent à l'étude de fonctions totales à une seule variable. Même si l'étude des dérivées partielles de fonctions à deux variables peut le plus souvent réutiliser les lemmes existants, l'étude de la formule de d'Alembert comme solution de l'équation des ondes en dimension 1 m'a amenée à étudier des théorèmes ne pouvant être traités auparavant comme la dérivation d'intégrales à paramètres et certains cas de compositions. De plus, démontrer la dérivabilité d'une fonction comme la formule de d'Alembert est souvent excessivement long en Coq car il faut détailler toutes les étapes, j'ai donc construit une tactique par réflexion permettant de résumer la phrase "par application des théorèmes généraux de dérivation" souvent utilisée dans les démonstrations sur papier.