Affine functions and series with co-inductive real numbers

TL;DR

This paper extends co-inductive real number algorithms in Coq, demonstrating how to verify and construct functions for affine formulas and series, including the computation of Euler's number e, using co-recursion and recursion techniques.

Contribution

It introduces methods to combine co-recursion and recursion for defining functions on co-inductive real numbers, enabling effective verification of algorithms for series and affine formulas.

Findings

Verified digit streams relate to axiomatized real numbers.

Constructed correct-by-construction addition algorithms.

Defined functions for affine formulas and series, including Euler's number e.

Abstract

We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as co-inductive types. Four aspects are studied: the first aspect concerns the proof that digit streams can be related to the axiomatized real numbers that are already axiomatized in the proof system (axiomatized, but with no fixed representation). The second aspect re-visits the definition of an addition function, looking at techniques to let the proof search mechanism perform the effective construction of an algorithm that is correct by construction. The third aspect concerns the definition of a function to compute affine formulas with positive rational coefficients. This should be understood as a testbed to describe a technique to combine co-recursion and recursion to obtain a model for an algorithm that appears at first sight to be outside the expressive power allowed by the proof system. The fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number e. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion, but we performed with the Coq system [12, 3, 14].