Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives

Sylvie Boldo 1, 2 Catherine Lelay 1, 2 Guillaume Melquiond 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
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.
Type de document :
Communication dans un congrès
Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_22>
Liste complète des métadonnées


https://hal.inria.fr/hal-00712938
Contributeur : Guillaume Melquiond <>
Soumis le : vendredi 14 septembre 2012 - 18:14:44
Dernière modification le : jeudi 9 février 2017 - 15:41:39
Document(s) archivé(s) le : samedi 15 décembre 2012 - 03:49:36

Fichier

article.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives. Chris Hawblitzel and Dale Miller. CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. Springer, 7679, pp.289-304, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_22>. <hal-00712938v2>

Partager

Métriques

Consultations de
la notice

813

Téléchargements du document

345