The Coq mailing list

["Kyle Stemen" <ncyms8r3x2 AT snkmail.com>]

Is there a getting started guide for CoRN? My questions are less about the mathematical basis of CoRN and more like simple beginner questions, for example what's the difference between the CR and AR types and how do I prove simple things like (0 < 2)%CR ?

I can run CoRN out of the build directory using coqidescript, but it I can't figure out how to install CoRN. Is CoRN even intended to be installed?

On Tue, Nov 18, 2014 at 10:14 AM, Bas Spitters b.a.w.spitters-at-gmail.com |coq-club/Example Allow| <9bz1k46gut AT sneakemail.com> wrote:

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?
>
>