For linear systems I analyze the case where the associated matrix has interval coefficients. This corresponds to the idea that the value of a coefficient is not known exactly, but rather it is known to lie in an interval of possible values. For solving such systems an important issue is whether the associated matrix is regular (has non-null determinant) for whatever values we choose for the coefficients in their corresponding interval. The results of this work are reusable libraries dealing with intervals, interval matrices and basic operations on them as well as a collection of formally verified criteria for regularity of interval matrices.
In the case of non-linear systems I formalized properties of Newton's method inside the proof assistant Coq. Newton's method is a numerical method widely used for approximating solutions of equations or systems of equations. The goal was to formalize Kantorovitch's theorem which gives the convergence of Newton's method to a solution, the speed of the convergence and the local stability of the method. For the formalization of Kantorovitch's theorem I used the implementation of real numbers provided in the Standard Library of Coq. For the case of one equation the results in the library were sufficient. For the case of a system of equations the proof of Kantorovitch's theorem requires multivariate analysis and Coq does not provide such a library. I formalized concepts of multivariate analysis by using not only the standard library of Coq but also the SSReflect extension of Coq and the libraries developed on it. The formalization covers: real vectors and matrices, norm on vectors and matrices, convergences of sequences of vectors, relations between a matrix norm and its determinant, limit and continuity for functions of several variables, properties of the partial derivatives of such functions.
In a joint work with Nicolas Julien, we use the formalization of Kantorovitch's theorem done on the real numbers of Coq's Standard Library in order to validate the computation with Newton's method done with a library of exact real arithmetic based on co-inductive streams. This work has two main parts. First, based on Newton's method, we design and prove correct an algorithm on streams for computing the root of a real function in a lazy manner. Second, we prove that rounding at each step in Newton's method still yields a convergent process with an accurate correlation between the precision of the input and that of the result.
This proof is designed on the previous proofs formalized for Kantorovitch's theorem but it is an original result.
Here are the associated Coq files: