The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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