The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

AFAIK, the reals in the standard library are axiomatically defined; you cannot compute with them in general.

If you want to compute with exact reals, look at the CoRN library.

http://corn.cs.ru.nl/

Note that real numbers (not to be confused with floats/doubles/triples....) are in some sense infinite objects.

When you compute a real number, you get a function that can be used to compute

arbitrarily close rational (finite) approximations to the represented real number.

In CoRN, there is a certified implementation of square roots using the Wolfram's method

https://github.com/c-corn/corn/blob/master/reals/faster/ARroot.v

For example usages, look at

https://github.com/c-corn/corn/blob/master/examples/RealFaster.v

The above implementations seems to be specialized for square roots.

I didn't find any specialized method for cube roots, or n^th roots.

I think that you can use computational content of the Intermediate Value Theorem (IVT) to 

get an inefficient implementation of n^th roots for any positive natural n.

https://github.com/c-corn/corn/blob/master/ftc/StrongIVT.v

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, Nov 18, 2014 at 2:56 AM, <ncyms8r3x2 AT snkmail.com> wrote:

I can't find a cube root function for reals in the standard library. Am I
missing it?

Is there another commonly used and more complete library for real numbers that
you can recommend?