A constructive proof of Simpson's Rule
Thierry Coquand, Bas Spitters

TL;DR
This paper provides a constructive proof of Simpson's Rule and related numerical analysis results, avoiding classical non-constructive theorems by using alternative ideas from Ampère and Genocchi.
Contribution
It introduces a constructive approach to prove the error term for Simpson's Rule, replacing classical theorems with constructive methods.
Findings
Constructive proof of Simpson's Rule error term
Avoids classical Rolle's theorem in proofs
Uses ideas from Ampère and Genocchi
Abstract
For most purposes, one can replace the use of Rolle's theorem and the mean value theorem, which are not constructively valid, by the law of bounded change. The proof of two basic results in numerical analysis, the error term for Lagrange interpolation and Simpson's rule, however seem to require the full strength of the classical Rolle's Theorem. The goal of this note is to justify these two results constructively, using ideas going back to Amp\`ere and Genocchi.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
