Description
La méthode des éléments finis est largement employée pour résoudre de nombreux problèmes issus de la physique, de la biologie... Elle s'enrichit quotidiennement de nouveaux développements à la fois en termes d'applications, de méthodes mathématiques, numériques et de calcul scientifiques. L'un de ses avantages est qu'elle s'appuie sur des fondations mathématiques solides. De nombreux codes de calcul basés sur les éléments finis, libres ou non, sont disponibles. La question se pose à chaque fois de la confiance qu'on peut avoir dans les résultats fournis par ces codes, les sources d'erreur étant nombreuses : erreur de programmation, méthode mathématique incorrecte, convergence incomplète (méthode elle-même, résolution non linéaire ou linéaire), maillage inadapté, accumulation d'erreurs flottantes...
Les physiciens, les mathématiciens et les informaticiens cherchent et donnent des moyens pour augmenter cette confiance : la validation est une étape systématiquement nécessaire, avant tout calcul. Il nous semble qu'au-delà des techniques de validation, un niveau supplémentaire de confiance peut être fourni par la vérification formelle de la méthode des éléments finis, ainsi que d'une bibliothèque, ou tout au moins des pans d'une bibliothèque d'éléments finis.
La preuve formelle a été développée par des chercheurs en informatique pour prouver qu'un programme ou un théorème est correct par rapport à sa spécification. Le théorème est mathématiquement vrai et le programme fait ce qui lui a été spécifié (la spécification du programme doit également être formalisée pour pouvoir dérouler la totalité du processus formel), étant donnés le contexte de départ. Des assistants de preuve, comme Coq, permettent de prouver formellement des théorèmes et des programmes.
L'objet de cet exposé est donc de présenter quelques étapes vers la preuve formelle en Coq de la méthode mathématique des éléments finis, ainsi que de parties de programmes d'éléments finis. Une première expérience avait été menée avec la preuve formelle complète des différences finies 1D pour l'équation des ondes (méthode et programme), incluant une borne de l'erreur due aux calculs en arithmétique flottante.
Pour les éléments finis (EF), nous avons commencé par la preuve formelle en Coq du Théorème de Lax-Milgram et du Lemme de Céa, dans l'objectif de prouver les EF pour le problème de Poisson. On se limitera pour le moment à ce type de problèmes et aux méthodes "classiques" (EF de Lagrange). Dans une seconde étape, nous avons construit formellement en Coq la théorie d'intégration de Lebesgue, afin de mettre en place dans un troisième temps (à venir) les espaces de Sobolev et appliquer le théorème de Lax-Milgram. Quelques résultats préliminaires concernant la définition formelle des éléments finis proprement dits seront présentés.
