Formal proof of a wave equation resolution scheme: the method error
Abstract
Popular finite difference numerical schemes for the resolution of the one-dimensional acoustic wave equation are well-known to be convergent. We present a comprehensive formalization of the simplest one and formally prove its convergence in Coq. The main difficulties lie in the proper definition of asymptotic behaviors and the implicit way they are handled in the mathematical pen-and-paper proofs. To our knowledge, this is the first time such kind of mathematical proof is machine-checked.
Les schémas numériques de résolution de l'équation des ondes en dimension 1 sont notoirement convergents. Nous présentons une formalisation détaillée du schéma le plus simple et nous prouvons formellement sa convergence dans le système d'aide à la preuve Coq. La difficulté principale se situe dans la définition adéquate des comportements asymptotiques et du fait que ces comportements ne sont pas complètement décrits dans les preuves sur papier. À notre connaissance, c'est la première mécanisation complète d'une telle preuve en analyse numérique.
Origin : Files produced by the author(s)
Loading...