Skip to Main content Skip to Navigation
Conference papers

Définir le fini : deux formalisations d'espaces de dimension finie

Florian Faissole 1
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Résumé : Les espaces de dimension finie permettent de décrire mathématiquement certaines méthodes numériques comme la méthode des éléments finis. Leur formalisation est nécessaire pour certifier que ces méthodes sont correctes et plus précisément qu'elles sont convergentes. Dans cet article, nous présentons deux méthodes pour formaliser les espaces de dimension finie en Coq, dans un cadre de topologie générale. Les deux approches utilisent des mécanismes différents et ne présentent pas les mêmes avantages et inconvénients. La première repose sur l'extension, à l'aide de structures canoniques, de la hiérarchie algébrique de la bibliothèque Coquelicot. Elle permet aisément de montrer que les espaces R n sont de dimension finie et plus généralement que le produit cartésien d'espaces de dimension finie est de dimension finie. La seconde repose sur l'utilisation de sous-espaces en tant que prédicats sur l'espace total. Elle permet d'extraire des propriétés topologiques sur des sous-espaces de dimension finie d'un espace de dimension infinie, comme la fermeture des sous-espaces de dimension finie des espaces de Hilbert. Nous proposons par ailleurs une étude comparative de ces deux approches.
Document type :
Conference papers
Complete list of metadata

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01654457
Contributor : Florian Faissole <>
Submitted on : Monday, December 4, 2017 - 8:49:38 AM
Last modification on : Thursday, July 8, 2021 - 3:49:47 AM

File

jfla.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01654457, version 1

Citation

Florian Faissole. Définir le fini : deux formalisations d'espaces de dimension finie. JLFA 2018 - Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-mer, France. pp.1-6. ⟨hal-01654457⟩

Share

Metrics

Record views

226

Files downloads

154