The Coq mailing list

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

Sorry, I didn't realize how important the question was to you. I tend to skim tutorials and try to code on my own afterwards, skimming more deeply for specific areas of interest.

I started reading Chapter 1, skimming less over the start and more over the end, when I realized Coq was being compared to other verifiers like HOL, which I am also not familiar with, so the comparisons would be largely meaningless.

In Chapter 2, I was amazed that the tutorial jumps right into constructing a compiler for a stack language. The note about coqdoc / prettyprinting was very important; I would have been lost for how to type the code into Coq. On one hand, the prettyprinting is helpful, because the concision allows more information to be shown at once, but on the other, it's frustrating to learn two syntaxes in parallel when one, what you actually type into Coq, would have sufficed. The problem itself necessitates a parallel syntax: raw stack language expressions and compiled stack code. And then there's the parallel syntax of conceptual inductive proofs and inductive Coq proofs--I'm not even strong on hand inductive proofs. At that point, I started to get lost.

So I backed away from Chapter 2, from inductive proofs, and decided to try out Andrej's How to use CoqIDE. His example proof is short, and explains a lot about CoqIDE, but it uses Peirce's Law, which I wasn't ready to accept. On the surface, Peirce's Law is a bunch of nested implications. So I backed away from Andrej's example and started asking questions about how I could go about proving Peirce's Law, which, as we've seen, has its own difficulties.

CPDT Chapter 2 has practical examples, something few manuals stress. But that's a double-edged sword. Because it's so practical, it's hard to sort out the fundamental lessons. It might be better to teach super incrementally, and reserve alternating chapters for practical examples. Peter Seibel does this in Practical Common Lisp.

In other words, I find it hard to absorb prettyprinting; stack languages; ML-style type declarations; inductive proofs; and Coq syntax all in one chapter, even though I know how to use the first four. If each of these subprocesses take O(n) of my mental resources, then Chapter 2 takes O(n²), not the intuitive 5*O(n) = O(5n) = O(n).

In contrast, by RWH Chapter 3, I was able to play around in GHC and make silly types like data Mool = Mool. That freedom, that fun, made me keep reading until somewhere in Chapter 4, where I departed and began coding my own Haskell projects. I believe that the smallness of the examples in RWH Chapters 1-3 are what allowed me to do this.

There may be two extremes of programming learners: One learner who likes to see super incremental examples that gradually build up to something practical; and another who likes to dive into a practical example, run it, and later learn how the pieces work. Of course, there's overlap and what-not.

I'm very much the Hello World kind of learner, in part, because it lets me pull from what I know about how other languages do Hello World. Though propositional logic may be in actuality harder to prove in Coq than inductive logic, to me, propositional logic is more basic and therefore easier to learn how to verify in Coq.

In CPDT Chapter 12, the stuff about type hierarchies, I find both fascinating and fairly intuitive. I kind of wish that CPDT started with set theory / type theory and built up to the other stuff.

Cheers,

Andrew Pennebaker

www.yellosoft.us

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

Andrew Pennebaker wrote:

Oo, the Haskell IO point is apt. So I guess propositional logic tautologies aren't the easiest things to do in Coq? :)

No, they're very easy, either automatically or, after the proper preparation, manually.

I don't mean to be argumentative, but I'm going to start ignoring your questions if you keep ignoring mine about which chunk of CPDT you have read.  I truly believe all of your questions on propositional logic so far are answered in CPDT, in reasonably accessible form.

Re: The law of excluded middle

How much of our logic is not based on the law of excluded middle?

Can Peirce's Law be derived without it?

Peirce's law and excluded middle are logically equivalent.

I don't know of any theorem in, for instance, verification of traditional programs that fundamentally relies on classical logic.  Rather, I view it as more of a shortcut to avoid proving decidability of some important families of propositions.