The Coq mailing list

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

Andrew Pennebaker wrote:
> 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

You haven't answered my question about how much of CPDT you have read.  
The book is meant to be accessible to people with your background.

If you have read no more than the first 3 chapters, then it would be 
expected that you haven't learned how to prove propositional logic 
tautologies, because that topic first appears significantly in Chapter 
4!  You may be falling into a similar trap of Haskell newbies who want 
their first program to do input/output.  Haskell experts know that I/O 
is far from central to the language, even though it is viewed as central 
in other contexts.  Similarly, propositional logic is not central to 
Coq; it is defined on top of more primitive constructs, and you should 
find the proof techniques much more intuitive after taking the time to 
learn those constructs properly.

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

Yes, I don't believe in the law of the excluded middle.  Classical and 
constructive propositional logic are equivalent when all underlying 
propositions are decidable, which is (probably) the case in the real 
(probably finite) world.  Our intuitions are formed based on that real 
world, and thus our intuitions have nothing to say about the meanings of 
the propositional connectives over undecidable propositions.  We have no 
real-world precedent for excluded middle applied to undecidable 
propositions.  The constructive logic mindset gets around this by 
defining the meanings of (essentially) _all_ the connectives in terms of 
algorithmic processes, where our intuitions work better.