Abstract
Finding an elementary form for an antiderivative is often a difficult task, so numerical integration has become a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis.
This paper presents an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq formal system. Our approach is not based on traditional quadrature methods such as Newton-Cotes formulas. Instead, it relies on computing and evaluating antiderivatives of rigorous polynomial approximations, combined with an adaptive domain splitting. This work has been integrated to the CoqInterval library.
This work was supported in part by the project FastRelax ANR-14-CE25-0018-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
Notes
- 1.
- 2.
We say that \(\mathbf {p} \in \mathbb {I}[X]\) is an enclosure of \(p \in \mathbb {R}[X]\) if, for all \(i \in \mathbb {N}\), the \(i^{th}\) coefficient \(\mathbf {p}_i\) of \(\mathbf {p}\) is an enclosure of the \(i^{th}\) coefficient \(p_i\) of p, where we take the convention that for \(i > \deg \mathbf {p}\), \(\mathbf {p}_i = \{0\}\) and for \(i > \deg p\), \(p_i = 0\).
- 3.
Note that the evaluation model is quite simple: the stack grows linearly with the size of the expression since no element of the stack is ever removed.
- 4.
The only thing that will later distinguishes the integration variable t from an actual constant such as \(\pi \) is that its value is placed at the top of the initial evaluation stack.
- 5.
The magnitude might be so coarse that it is computed as \(+\infty \). In that case, the user setting is directly understood as an absolute bound.
- 6.
- 7.
The bug lies in an incorrect implementation of Taylor models for absolute value.
- 8.
Any 3-SAT instance can be reduced to approximating the integral of a multivariate polynomial.
References
Ahmed, Z.: Ahmed’s integral: the maiden solution. Math. Spectr. 48(1), 11–12 (2015)
Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)
Eaton, J.W., Bateman, D., Hauberg, S., Wehbring, R., Octave, G.N.U.: version 3.8.1 manual: a high-level interactive language for numerical computations (2014)
Hass, J., Schlafly, R.: Double bubbles minimize. Ann. Math. 151(2), 459–515 (2000). Second Series
Helfgott, H.A.: Major arcs for Goldbach’s problem (2013). http://arxiv.org/abs/1305.2897
Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113–127. Springer, Heidelberg (2014)
Makarov, E., Spitters, B.: The picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 463–468. Springer, Heidelberg (2013)
Martin-Dorel, É., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 1–31 (2015)
Mayero, M.: Formalisation et automatisation de preuves en analyses réelle et numérique. Ph.D. thesis, Université Paris VI, December 2001
Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM, Philadelphia (2009)
Nedialkov, N.S.: Interval tools for ODEs and DAEs. In: Scientific Computing, Computer Arithmetic and Validated Numerics (SCAN) (2006). http://www.cas.mcmaster.ca/~nedialk/vnodelp/
O’Connor, R., Spitters, B.: A computer verified, monadic, functional implementation of the integral. Theor. Comput. Sci. 411(37), 3386–3402 (2010)
Rump, S.M.: Verification methods: Rigorous results using floating-point arithmetic. Acta Numerica 19, 287–449 (2010). http://www.ti3.tu-harburg.de/rump/intlab/
Tucker, W.: Validated Numerics: A Short Introduction to Rigorous Computations. Princeton University Press, Princeton (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Mahboubi, A., Melquiond, G., Sibut-Pinote, T. (2016). Formally Verified Approximations of Definite Integrals. In: Blanchette, J., Merz, S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science(), vol 9807. Springer, Cham. https://doi.org/10.1007/978-3-319-43144-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-43144-4_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-43143-7
Online ISBN: 978-3-319-43144-4
eBook Packages: Computer ScienceComputer Science (R0)