The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

It is not difficult to get a version that computes from Log and exp:
https://github.com/c-corn/corn/blob/master/reals/fast/CRln.v

They can even be used to compute with the std lib reals:
Cezary Kaliszyk and Russell O’Connor. Computing with Classical Real
Numbers. Journal of Formalized Reasoning, Vol. 2, No. 1, 2009, Pages
27–29
http://jfr.cib.unibo.it/article/view/1411/932
Russell O’Connor. Certified Exact Transcendental Real Number
Computation in Coq. TPHOLS 2008, LNCS 5170: 246–261, Aug 2008,
Proceedings
http://www.springerlink.com/content/m380454267180372/

This work has not yet been ported to the faster "reals/faster" implementation.
Robbert Krebber and Bas Spitters Type classes for efficient exact real
arithmetic in Coq
LMCS 9(1:1), 2013. 10.2168/LMCS-9(1:01)2013.
http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

On Tue, Nov 18, 2014 at 6:52 PM, Abhishek Anand
<abhishek.anand.iitg AT gmail.com>
 wrote:
> 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?
>
>