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

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
Résumé : 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.
Type de document :
Article dans une revue
Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. <10.1007/s11786-014-0181-1>
Liste complète des métadonnées


https://hal.inria.fr/hal-00860648
Contributeur : Catherine Lelay <>
Soumis le : mardi 18 février 2014 - 17:06:04
Dernière modification le : samedi 18 février 2017 - 01:09:38
Document(s) archivé(s) le : dimanche 9 avril 2017 - 13:36:16

Fichier

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

Identifiants

Citation

Sylvie Boldo, Catherine Lelay, Guillaume Melquiond. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science, Springer, 2015, 9 (1), pp.41-62. <10.1007/s11786-014-0181-1>. <hal-00860648v2>

Partager

Métriques

Consultations de
la notice

572

Téléchargements du document

282