The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

Viktor, thanks. I'll try that.

Adam, please don't feel bad about my description of CPDT. I'm a Coq newbie, an undergrad, and I've only taken a couple introductory formal methods / discrete math courses. If you couldn't tell by my hand proof, I'm very much a newbie to this subfield. CPDT could be the best book ever written about formal proofs, and I would never even know. :P

I'm just trying to express to the Coq club my mindset so that we can better communicate with each other. For instance, I need to write my own Coq proofs in under to learn Coq; just following someone else's Coq proof, even a beautifully taught Coq proof, isn't enough for me.

Why all the questions? The dozens of questions I'm asking are mostly about syntax, something I usually Google. There just aren't enough Coq tutorials for me to get a solid grip on the syntax. Coq appears very different from everyday procedural programming, or even functional programming. Curry-Howard doesn't imply that we know how to use Curry-Howard to translate programs to proofs.

Re: importing the Classical module. Now that's interesting. Are there Coq programmers who don't believe in, say, the law of excluded middle?

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 2:34 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Andrew Pennebaker wrote:

I picked Peirce's Law because I think of it as a conceptually trivial proof, and I need to start somewhere in order to learn Coq's syntax and semantics. Agreed: It's just an exercise, one that in a larger proof I would just resort to /tauto/ to solve.

[...]

Repeat: this would all be reduced to /Require Import Classical; tauto./ in a larger proof, but I think that the Peirce example can help me understand how to use the Coq interface. The tutorials are interesting, but for me the examples feel more like demos than teaching exercises.

How much of CPDT have you read?  If it doesn't contain teaching exercises, then I have a lot of work to do on improving the book, and I'd love to get more specific suggestions!

(P.S.: A public service message: Please think hard before importing [Classical].  Not all of us believe that classical logic corresponds with valid reasoning. :P)