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 scheme 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 this kind of mathematical proof is machine-checked.
This research was supported by the ANR projects CerPAN (ANR-05-BLAN-0281-04) and F\(\oint\)ST (ANR-08-BLAN-0246-01).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Thomas, J.W.: Numerical Partial Differential Equations: Finite Difference Methods. Texts in Applied Mathematics, vol. 22. Springer, Heidelberg (1995)
Zwillinger, D.: Handbook of Differential Equations. Academic Press, London (1998)
Dutertre, B.: Elements of Mathematical Analysis in PVS. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 141–156. Springer, Heidelberg (1996)
Harrison, J.: Theorem Proving with the Real Numbers. Springer, Heidelberg (1998)
Fleuriot, J.D.: On the Mechanization of Real Analysis in Isabelle/HOL. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 145–161. Springer, Heidelberg (2000)
Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. PhD thesis, Université Paris VI (2001)
Gamboa, R., Kaufmann, M.: Nonstandard Analysis in ACL2. Journal of Automated Reasoning 27(4), 323–351 (2001)
Geuvers, H., Niqui, M.: Constructive Reals in Coq: Axioms and Categoricity. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 79–95. Springer, Heidelberg (2002)
Cruz-Filipe, L.: A Constructive Formalization of the Fundamental Theorem of Calculus. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 108–126. Springer, Heidelberg (2003)
Mayero, M.: Using Theorem Proving for Numerical Analysis (Correctness Proof of an Automatic Differentiation Algorithm). In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 246–262. Springer, Heidelberg (2002)
Harrison, J.: A HOL Theory of Euclidean Space. In: Hurd, J., Melham, T.F. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114–129. Springer, Heidelberg (2005)
Avigad, J., Donnelly, K.: A Decision Procedure for Linear ”Big O” Equations. J. Autom. Reason. 38(4), 353–373 (2007)
Bécache, E.: Étude de schémas numériques pour la résolution de l’équation des ondes. Master Modélisation et simulation, Cours ENSTA (2009), http://www-rocq.inria.fr/~becache/COURS-ONDES/Poly-num-0209.pdf
Achenbach, J.D.: Wave Propagation in Elastic Solids. North Holland, Amsterdam (1973)
Brekhovskikh, L.M., Goncharov, V.: Mechanics of Continua and Wave Dynamics. Springer, Heidelberg (1994)
Newton, I.: Axiomata, sive Leges Motus. In: Philosophiae Naturalis Principia Mathematica, London, vol. 1 (1687)
le Rond D’Alembert, J.: Recherches sur la courbe que forme une corde tendue mise en vibrations. In: Histoire de l’Académie Royale des Sciences et Belles Lettres (Année 1747), vol. 3, pp. 214–249. Haude et Spener, Berlin (1749)
John, F.: Partial Differential Equations. Springer, Heidelberg (1986)
Courant, R., Friedrichs, K., Lewy, H.: On the partial difference equations of mathematical physics. IBM Journal of Research and Development 11(2), 215–234 (1967)
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)
Boldo, S.: Floats & Ropes: a case study for formal numerical program verification. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 91–102. Springer, Heidelberg (2009)
Letouzey, P.: A New Extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol. 2646, pp. 200–219. Springer, Heidelberg (2003)
Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Boldo, S., Clément, F., Filliâtre, JC., Mayero, M., Melquiond, G., Weis, P. (2010). Formal Proof of a Wave Equation Resolution Scheme: The Method Error. In: Kaufmann, M., Paulson, L.C. (eds) Interactive Theorem Proving. ITP 2010. Lecture Notes in Computer Science, vol 6172. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14052-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-14052-5_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14051-8
Online ISBN: 978-3-642-14052-5
eBook Packages: Computer ScienceComputer Science (R0)