The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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)