coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Koprowski <adam.koprowski AT gmail.com>
- To: Robert Merkin <bobmerk AT earthlink.net>
- Cc: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How do I verify Euclid IX 20?
- Date: Wed, 3 Mar 2010 23:25:54 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; b=o9l70+r6Kxyc4E2VuXqx40ces9VUkPt7NXwarRBUAqN37yTzClnlJrKsiwHAsZnChg HE/Xlj3Zl16N96Z6IFHFEiSrHxNSldcUyZc9Zd1oIxg1QqUPIeCn0UR0JYL1ehQMTZd2 4ZlWXZGtA1aaSWKKVmNRT60Det3h9a0mgmFc0=
Hi Bob,
You can also check out the Euler's project [1] with a list of (rather simple) mathematical problems that you can try to solve (with correctness proofs clearly :) in Coq. The credit for this very fine idea goes to Stephane Lescuyer: you can check his web-page [2] for his solutions to some of those problems.
For something even simpler you check out the web-page [3] of the course on Coq that I gave few years ago and some exercise suggestions there [4].
Best,
Adam
On Wed, Mar 3, 2010 at 21:49, Guillaume Allais <sbleune AT gmail.com> wrote:
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
--
Adam Koprowski [http://www.cs.ru.nl/~Adam.Koprowski]
R&D @ MLstate [http://mlstate.com, 15 rue Berlier, 75013 Paris, France]
- [Coq-Club] [Off-topic] Classification/taxonomy of formal methods?, David MENTRE
- [Coq-Club] How do I verify Euclid IX 20?,
Robert Merkin
- Re: [Coq-Club] How do I verify Euclid IX 20?,
Guillaume Allais
- Re: [Coq-Club] How do I verify Euclid IX 20?, Adam Koprowski
- Re: [Coq-Club] How do I verify Euclid IX 20?,
Guillaume Allais
- [Coq-Club] How do I verify Euclid IX 20?,
Robert Merkin
Archive powered by MhonArc 2.6.16.