Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why is the signature of sqrt R->R ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why is the signature of sqrt R->R ?


Chronological Thread 
  • From: Florian Steinberg <florian.steinberg AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why is the signature of sqrt R->R ?
  • Date: Tue, 5 Feb 2019 04:03:25 +0100

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



Archive powered by MHonArc 2.6.18.

Top of Page