coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Bas Spitters <b.a.w.spitters AT gmail.com>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Cube root function
- Date: Tue, 18 Nov 2014 19:14:27 +0100
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?
>
>
- [Coq-Club] Cube root function, ncyms8r3x2, 11/18/2014
- Re: [Coq-Club] Cube root function, Abhishek Anand, 11/18/2014
- Re: [Coq-Club] Cube root function, Bas Spitters, 11/18/2014
- Re: [Coq-Club] Cube root function, Kyle Stemen, 11/23/2014
- Re: [Coq-Club] Cube root function, Abhishek Anand, 11/26/2014
- Re: [Coq-Club] Cube root function, Kyle Stemen, 11/23/2014
- Re: [Coq-Club] Cube root function, Bas Spitters, 11/18/2014
- Re: [Coq-Club] Cube root function, bertot, 11/19/2014
- Re: [Coq-Club] Cube root function, Guillaume Melquiond, 11/19/2014
- Re: [Coq-Club] Cube root function, Kyle Stemen, 11/23/2014
- Re: [Coq-Club] Cube root function, Abhishek Anand, 11/18/2014
Archive powered by MHonArc 2.6.18.