The Coq mailing list

[Ilmārs Cīrulis <ilmars.cirulis AT gmail.com>]

Abhishek Anand, just because of curiosity - for what it was necessary?

Anyway, talking about user experience... It seems unnecessarily difficult to use this positive prime finding algorithm for finding nat primes.

I didn't find anything useful in the Standard Library.

What I must do if I want to make a faster decision procedure for nat, using this more effective represantation?

On Tue, Jan 27, 2015 at 4:50 AM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Thanks a lot! This is exactly what I needed.

-- Abhishek

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

On Mon, Jan 26, 2015 at 8:11 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

This is almost the same using PArith.

I was too lazy to use it for finding nat primes by conversions etc.

Of course, this can be improved in many ways. Anyway, this works good too, at least for first try.

For example, Eval compute in (projT1 (prime_infinitude (2::5::7::nil))) gives 71 almost instantly.

On Sun, Jan 25, 2015 at 3:01 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

A little bit unpolished, I believe. (For example, prime_infinitude follows from prime_infinitude_0, probably can be structured more nicely etc.)

And, oops, I missed the part when you asked for calculation of exact such prime. The proof can be remade for this purpose but I will leave that for someone else or for February when I have more free time.

On Sun, Jan 25, 2015 at 2:54 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

There it is. You can skip prime_infinitude and prime_infinitude_0.

--

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.

--

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.

--

To unsubscribe reply with "Nesūti spamu, ķēmīgais rausi!" in the subject heading.