coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How do I verify Euclid IX 20?

From: "Robert Merkin" <bobmerk AT earthlink.net>
To: "Coq Club" <coq-club AT inria.fr>
Subject: [Coq-Club] How do I verify Euclid IX 20?
Date: Wed, 3 Mar 2010 13:47:24 -0500
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=dk20050327; d=earthlink.net; b=NLMjTHwoTttDrKLCevHLF6F5J2jVD8HKOaYqYmwKGjkRI/E+WFd5ho3D+Xrl5Sx6; h=Received:Message-ID:Reply-To:From:To:References:In-Reply-To:Subject:Date:MIME-Version:Content-Type:Content-Transfer-Encoding:X-Priority:X-MSMail-Priority:X-Mailer:X-MimeOLE:X-ELNK-Trace:X-Originating-IP;

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

[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