Thèse préparée dans l’unité de recherche : Laboratoire Méthodes Formelles (Université Paris Saclay, CNRS, ENS Paris-Saclay), sous la direction de Sylvie BOLDO, directrice de recherche, la co-direction de Micaela MAYERO, maîtresse de conférences, le co-encadrement de François CLÉMENT, chargé de recherche.
Thèse soutenue à Paris-Saclay, le 09 décembre 2024, par
Houda MOUHCINE
Composition du Jury
Membres du jury avec voix délibérative
Sylvain CONCHON
Professeur des universités, université Paris Saclay, France : Président
Damien POUS
Directeur de recherche, CNRS et ENS Lyon, France : Rapporteur & Examinateur
Alan SCHMITT
Directeur de recherche, Inria Rennes, France : Rapporteur & Examinateur
Laura GRIGORI
Professeure, EPFL, Suisse : Examinatrice
Sébastien IMPÉRIALE
Chargé de recherche, Inria Saclay, France : Examinateur
Évaluation brève du résumé de la thèse par Dr. Jawad DABOUNO
Professeur à l’université Hassan 1er Setat.
Director of Laboratory of Artificial intelligence Research and Applications (AIRA).
Cette thèse vise à développer des preuves formelles de théorèmes et de propositions mathématiques dans le domaine de l’analyse réelle en utilisant l’assistant de preuve Coq pour garantir leur exactitude. Le travail est divisé en deux parties principales :
Première partie : Elle se concentre sur la formalisation de concepts mathématiques fondamentaux en analyse fonctionnelle, tels que le principe d’induction de Lebesgue et le théorème de Tonelli, utilisés pour calculer des intégrales doubles sur des espaces produits.
Deuxième partie : Elle traite de la formalisation et de la construction des éléments finis dans le cadre de la méthode des éléments finis (FEM), une technique numérique couramment utilisée pour résoudre les équations aux dérivées partielles (EDP). Cette partie se concentre sur les éléments finis simpliciaux de Lagrange et nécessite l’utilisation de divers concepts algébriques tels que les espaces affines et les espaces de dimensions finies.
Le sujet de recherche est d’une grande importance, et l’approche est scientifique et rigoureuse. La thèse est une contribution précieuse au domaine de la vérification formelle des calculs scientifiques, en particulier pour améliorer la précision et la fiabilité des programmes utilisant la méthode des éléments finis. Le travail inclut des cadres théoriques et s’étend aux applications dans divers domaines industriels, notamment ceux liés au calcul des structures et aux industries mécaniques.
تقويم باللغة العربية
تهدف هذه الأطروحة إلى تطوير إثباتات رسمية (formal proofs) لنظريات ومبادئ رياضية في مجال التحليل الحقيقي (real analysis) باستخدام مساعد الإثبات كوك (Coq) لضمان صحتها. ينقسم العمل إلى جزأين رئيسيين:
1ـ الجزء الأول: يركز على ترميز مبادئ رياضية أساسية في التحليل الوظيفي، مثل مبدأ استقراء لبيغ(Lebesgue) ومبرهنة تونيلي، التي تُستخدم لحساب التكاملات المزدوجة على الفضاءات المنتجة.
2ـ الجزء الثاني: يتناول ترميز وبناء عناصر محدودة ضمن إطار طريقة العناصر المحدودة (Finite Element Method (FEM),)، وهي تقنية عددية شائعة لحل المعادلات التفاضلية الجزئية (EDP). يُركز هذا الجزء على عناصر لاغرانج المتعددة الأبعاد، ويتطلب استخدام مفاهيم جبرية متنوعة مثل الفضاءات الأفينية والفضاءات ذات الأبعاد المحدودة.
موضوع البحث مهم جدا والمقاربة علمية ودقيقة. وتُعتبر الأطروحة مساهمة قيمة في مجال التحقق الرسمي للحسابات العلمية، خاصة في تحسين دقة وموثوقية برامج طريقة العناصر المحدودة. كما أن العمل يشمل الأطر النظرية ويمتد للتطبيقات في مجالات صناعية مختلفة، خاصة ما يتعلق بحساب البنيات والصناعات الميكانيكية.
Abstract : This thesis is dedicated to developing formal proofs of mathematical theorems and propositions within the field of real analysis, using the Coq proof assistant to ensure their correctness. The core of this work is divided into two main parts. The first part focuses on using Coq to formalize the Lebesgue induction principle and the Tonelli theorem, allowing the computation of double integrals on product spaces by iteratively integrating with respect to each variable. This work builds upon previous research in measure theory and the Lebesgue integral. The second part is within the framework of the Finite Element Method (FEM), a widely used numerical technique for numerically solving partial differential equations. FEM plays an important role in numerous industrial simulation programs, particularly in approximating solutions to complex problems. Specifically, we aim to construct finite elements, focusing on simplicial Lagrange finite elements. This work requires the use of a broad range of algebraic concepts such as finite families, monoids, module spaces, affine spaces, and finite-dimensional spaces. To conduct this study, we begin by defining a general finite element in Coq. Then, we show the effectiveness of this definition by building the widely used simplicial Lagrange finite elements. This involves the formalization in classical logic of several foundational components, including the construction of the approximation space, expressing its Lagrange polynomial basis, and formalizing affine geometric transformations and the unisolvence property of Lagrange finite elements.
Synthèse en Français
Cette thèse est consacrée au développement de preuves formelles de théorèmes et de propositions mathématiques dans le domaine de l’analyse réelle, en utilisant l’assistant de preuve Coq pour assurer leur exactitude. Le cœur de ce travail est divisé en deux parties principales.
La première partie se concentre sur l’utilisation de Coq pour formaliser des concepts mathématiques fondamentaux en analyse fonctionnelle, notamment le principe d’induction de Lebesgue et le théorème de Tonelli. Ce travail sert de base pour prouver des propriétés liées aux fonctions mesurables. Le principe d’induction de Lebesgue se présente comme une technique de preuve pour établir des résultats concernant les fonctions mesurables non négatives, notamment celles qui impliquent des intégrales. Il reflète les trois étapes de construction suivies par Henri Lebesgue pour définir son intégrale. Ces étapes comprennent d’abord l’établissement de la propriété pour des fonctions indicatrices, puis son extension aux fonctions simples non négatives en vérifiant sa compatibilité avec les opérations linéaires positives. Enfin, la propriété s’applique à toutes les fonctions mesurables non négatives en s’assurant de sa compatibilité avec l’opération de supremum. Ce principe est dérivé d’un type inductif et apparaı̂t comme un outil nécessaire pour prouver le théorème de Tonelli.
Le théorème de Tonelli permet de simplifier le calcul d’intégrales multiples en établissant leur égalité avec des intégrales itérées, facilitant ainsi l’interchangeabilité des ordres d’intégration. Ce théorème est applicable spécifiquement aux fonctions mesurables non négatives et s’aligne avec le théorème de Fubini, qui étend son domaine d’application aux fonctions intégrables avec des signes arbitraires. Dans le cadre de cette thèse, l’accent est mis sur les fonctions non négatives à deux variables, ce qui prépare le terrain pour de futures explorations concernant les équations aux dérivées partielles (EDP) impliquant plusieurs variables.
La deuxième partie de ce travail de recherche, qui constitue le principal axe de cette thèse, s’intéresse à la formalisation dans Coq et à la construction des éléments finis, qui sont essentiels à la méthode des éléments finis (MEF). Cette méthode est largement utilisée pour trouver des solutions approximatives à des problèmes de valeur aux limites pour des EDP dans divers domaines scientifiques tels que la physique, la mécanique et la biologie. L’utilisation étendue et le succès de la MEF par les numériciens peuvent être attribués à sa flexibilité et à sa précision dans la gestion de problèmes présentant des géométries complexes, des discontinuités et des contraintes. Cependant, malgré les larges applications de la MEF, plusieurs défis critiques peuvent nuire à son efficacité et à sa fiabilité. Le processus de mise en place des simulations, de leur exécution et de l’analyse des résultats est souvent extrêmement chronophage, surtout pour les simulations complexes. De plus, les programmes de MEF sont généralement complexes, nécessitant une attention particulière aux détails. Même des erreurs mineures dans la mise en œuvre peuvent entrainer des contradictions significatives dans les résultats, compromettant la validité des résultats de simulation et pouvant conduire à des conclusions erronées. Pour faire face à ces problèmes, des preuves formelles sont employées pour garantir la correction et la fiabilité des algorithmes et des méthodes utilisés dans les simulations de MEF.
Plus précisément, nous visons à formaliser un élément fini (EF), qui est défini mathématiquement comme un triplet et formalisé sous forme d’un record. La MEF subdivise un grand domaine en parties plus petites et plus simples appelées éléments finis, typiquement reliés par des points appelés sommets. Chaque élément est caractérisé par un triplet constitué de trois composants complémentaires, notés (K, P, Σ). Le composant K représente l’élément géométrique pour l’élément fini, qui varie en forme, des intervalles dans des espaces unidimensionnels aux formes plus complexes comme des triangles ou des quadrilètres en deux dimensions, et des tétraèdres ou des cuboı̈des en trois dimensions, en fonction de la complexité du domaine et des exigences de la simulation. Dans le cadre de cette thèse, nous nous concentrons spécifiquement sur les simplexes, qui sont une généralisation du concept de triangle ou de tétraèdre à des dimensions arbitraires. Le second composant P du triplet d’éléments finis représente un espace vectoriel de dimension finie de fonctions polynomiales définies sur l’élément géométrique K. Ces polynômes sont utilisés pour approximer la solution au sein de l’élément fini, où le degré du polynôme (par exemple, linéaire, quadratique) détermine la précision de l’approximation. Le troisième composant Σ du triplet correspond à une famille de formes linéaires, également appelées degrés de liberté locaux, qui agissent sur les fonctions au sein de l’espace P. Ces formes sont choisies pour satisfaire la propriété d’unisolvance, garantissant que l’élément fini est bien défini. Cependant, traiter le problème pour des éléments individuels n’est pas suffisant. La méthode des éléments finis (MEF) assemble les équations locales de chaque élément fini en un système global d’équations qui représente l’ensemble du problème. En résolvant ce système global, nous obtenons une approximation de la solution qui couvre l’ensemble du domaine du problème.
L’accent de cette dernière partie de la recherche est la construction des éléments finis de la famille Lagrange simpliciaux en utilisant Coq. L’objectif principal de ce développement est d’établir un élément fini utile et de garantir que nos définitions pour les éléments finis sont suffisantes et valides pour être utilisées. Le choix de formaliser les éléments finis de Lagrange pour cette étude découle de leur utilisation répandue dans les applications de la MEF et de leur simplicité inhérente. Ce travail explore également la formalisation des définitions et des preuves concernant des propriétés essentielles telles que les polynômes de Lagrange, les transformations géométriques affines, et les éléments finis courrants et de références, entre autres.
Pour mettre cela en œuvre, nous devrons utiliser l’analyse réelle et des structures algébriques allant des monoı̈des abéliens aux espaces de modules de la bibliothèque Coquelicot. Chaque com- posant contribue à l’objectif principal de cette thèse, qui est d’établir formellement la propriété d’unisolvance des éléments finis de Lagrange. Les orientations futures incluent la formalisation des éléments finis quadrangulaires, certaines formules de quadrature et la construction d’espaces de Sobolev. Ainsi, les efforts collectifs décrits dans ce travail visent un objectif à long terme plus large : la vérification formelle des programmes de calcul scientifique et des parties de bibliothèques C++ comme FreeFEM++ et XLiFE++, qui implémentent la méthode des éléments finis.
