|
|
Catherine LELAY |
|
Contacts: |
Différentiabilité et intégrabilité en CoqRé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. Documents |