The Coq mailing list

[Richard Ford <richardlford AT gmail.com>]

I wonder if you have investigated Coquelicot (http://coquelicot.saclay.inria.fr/)? It uses total functions on reals to represent derivatives and integrals. The usual dependent formulations of these are unwieldy if you are doing more complex algorithms in calculus. Section 9.2 of the book "Computer Arithmetic and Formal Proof", by Boldo and Melquiond, explains in more detail how using total functions makes expressible some things that would be difficult or impossible using the default formulation of derivatives and integrals in Coq.

Best regards,

Rich

On Mon, Feb 4, 2019 at 5:26 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Théo, Florian,

thanks for sharing your insights and considerations!

After pondering over this for a while, I tend to agree with Florian, that a relational interpretation of terms of real numbers might also be worthwhile to consider. Besides being able to handle partial functions, it has the advantage that it could handle "multivalued functions", like complex roots or an inverse sine. It might be that this allows a more natural handling of e.g. representing the solutions of equations than CAS systems like Mathematica offer. Also the elementary functions of real numbers typically evaluate to existentials, so that the usual advantage of a functional interpretation (that it can be evaluated) doesn't seem to apply here. But I guess that such an interpretation would be more confusing at the beginning, e.g. that sqrt(x) simply means + sqrt(x) or - sqrt(x).

I am a mere beginner in doing real analysis in Coq and until I started to define new functions like asin, it was reasonably easy and straightforward to use and mostly compatible with the "outside the coq world" real analysis, so it is quite good as it is.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928