The Coq mailing list

[Guillaume Allais <sbleune AT gmail.com>]

Hi Bob,

You can have a look at Freek's web page [1] : he maintains an arbitrary list of the "top 100 theorems" and their (sometimes lack of) formalization in various theorem provers. You can see that the theorem you are looking for has been proved (number 11) using Coq.

I didn't manage to find the code online but you can try to email Russell O'Connor [2] who's the one who proved it.

Starting with this kind of proof may be a bit ambitious. You may want to begin with Master level exercises if you have no experience in theorem provers (If the fact that the subject is in French is not a problem for you, you can try to look at Aurelien Pardon's web page [3]).

Cheers,

[1] : http://www.cs.ru.nl/~freek/100/
[2] : http://r6.ca/
[3] : http://perso.ens-lyon.fr/aurelien.pardon/coq/index.html

--
guillaume

On 3 March 2010 19:47, Robert Merkin <bobmerk AT earthlink.net> wrote:

I am a beginner.

I would like to acquire a functional grasp of Coq by starting with a familiar and short proof, and then write/use Coq to verify it. Or read someone else's Coq code which verified this same proof.

Arbitrarily I have chosen Euclid IX 20: There are infinitely many Primes.

1. Is this a bad way to start learning Coq? Why?

2. Has anyone used Coq to verify Euclid IX 20? Is the code on-line, or can someone send it to me?

3. If I write the Coq program myself, how should I go about it?

Thanks for any guidance and help you can offer.

Bob / Massachusetts USA