Computing Solutions for Systems of Multivariate Ordinary Differential Equations in Rocq

Abstract

We formalize a solver for initial value problems for systems of multivariate analytic ordinary differential equations in the sense of constructive/computable analysis, using the Rocq proof assistant. The construction follows the classical proof of the Cauchy-Kovalevskaya theorem, computing the Taylor series expansion of the solution by iteratively deriving its coefficients. We prove that the computed Taylor series converges and provide explicit bounds on the truncation error, ensuring the error can be made arbitrarily small. Instead of relying on a concrete implementation of constructive reals, we develop an abstract framework using type classes and setoids, allowing the formalization to remain flexible and compatible with different implementations. Additionally, we extend the formalization to a more efficient variant based on interval arithmetic and illustrate its practical use with several examples.