The Coq mailing list

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

Cool! :)

No, they're good. Probably was tired too much few days ago when I last time tried it.

I had some beginner's difficulties with lia and nia when nat and positive are mixed together but it's solved now.
 

On Fri, Jan 30, 2015 at 7:04 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I had to give a lecture about Constructive Logic and dependent types.

I  like to use this Euclid's proof to show that many traditional mathematical proofs were already constructive.

I thought it was worth spending 30 seconds in demonstrating how one can "run" these proofs.

Thanks to your timely reply, I showed them:

Eval compute in  ( π₁ (prime_infinitude [2,3,5,7])).

Why is it   "unnecessarily difficult to use this positive prime finding algorithm for finding nat primes." ?

Are there issues in using Coq.PArith.BinPos.Pos.to_nat and Coq.PArith.BinPos.Pos.of_nat ?

Thanks,

-- Abhishek

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

On Fri, Jan 30, 2015 at 6:22 AM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

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.

--

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