Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert

Catherine Lelay 1, 2 Guillaume Melquiond 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Résumé : La bibliothèque standard de Coq contient de nombreuses définitions et lemmes permettant de faire de l'analyse, mais 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 montre les limites de cette approche. La formalisation en Coq de cette étude a ainsi nécessité de développer une théorie sur la dérivation des intégrales à paramètre et des fonctions à deux variables. De plus, démontrer en Coq la dérivabilité de la formule de d'Alembert s'est révélé être excessivement long. Nous avons donc construit une tactique par réflexion permettant de résumer l'expression "par application des théorèmes généraux de dérivation" souvent utilisée dans les démonstrations sur papier.
Type de document :
Communication dans un congrès
JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Liste complète des métadonnées


https://hal.inria.fr/hal-00642206
Contributeur : Catherine Lelay <>
Soumis le : vendredi 2 décembre 2011 - 13:45:33
Dernière modification le : jeudi 9 février 2017 - 15:53:42
Document(s) archivé(s) le : lundi 5 décembre 2016 - 08:35:14

Fichier

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

Identifiants

  • HAL Id : hal-00642206, version 2

Citation

Catherine Lelay, Guillaume Melquiond. Différentiabilité et intégrabilité en Coq. Application à la formule de d'Alembert. JFLA - Journées Francophone des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. <hal-00642206v2>

Partager

Métriques

Consultations de
la notice

458

Téléchargements du document

500