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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00642206
Contributor : Catherine Lelay <>
Submitted on : Friday, December 2, 2011 - 1:45:33 PM
Last modification on : Thursday, April 5, 2018 - 12:30:08 PM
Long-term archiving on : Monday, December 5, 2016 - 8:35:14 AM

File

lelay.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00642206, version 2

Collections

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. ⟨hal-00642206v2⟩

Share

Metrics

Record views

642

Files downloads

585