The Coq mailing list

[Florian Steinberg <florian.steinberg AT inria.fr>]

Hi Michael!

If you want to explore multivalued functions you can take a look at a 
wrapper for interpreting relations as multivalued functions that I am 
working on. You can find it in the mf repository of my github account. 
The documentation is currently mostly done inside of the files, the 
mf_set.v and the mf.v files have a preamble that briefly describes the 
important concepts. I don't know how usable this is, and am happy about 
any kind of feedback. mf has ssreflect as a dependency but is not 
ssreflect style as there is no attempt to talk about boolean valued 
anythings and all relations go to Prop. It also overwrites some of the 
notations of ssreflect, which I am not sure yet is a good idea.

I am mostly using mf for formalization of results about Kleene-Kreisel 
continuous functionals and some things from computable analysis. I did 
also use it for some formalizations about spaces of sequences (lp 
spaces) but in hindsight that was not a good idea, the lp-norms are more 
naturally understood as total functions from R^nat to the lower reals 
(luckily, as mentioned before, Coquelicot provides the possibility to 
translate to those, so I didn't have to redo a lot). So... yeah... use 
with care.

Best,

Florian

On 04/02/2019 12:25, Soegtrop, Michael 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