The Coq mailing list

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

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.

I am reading Coq materials like CPDT, and watching videos like How to use CoqIDE, however, their syntax varies from each other. I don't know when and how to use definitions vs variables vs theorems vs lemmas. I don't always understand the logic of the example proofs, so I feel like I'm just copying code without any understanding. Hence the Peirce's Law exercise I assigned myself.

Adam, imply_to_or is defined in the Classical package. I'm just wondering how to tell Coq to apply it to H rather than the goal, resulting in H being ~(p -> q) \/ p, or perhaps using imply_to_or to make a new hypothesis, H0: ~(p -> q) \/ p. I don't know how Coq wants me to do this.

Once I can do that, my next questions are how to branch into the two cases of ~(p -> q) \/ p, syntactically how to conclude p in each case, how to jump between the cases, and how to conclude p based on exhausting both cases.

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.

Cheers,

Andrew Pennebaker

www.yellosoft.us

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

Andrew Pennebaker wrote:

I'd like to prove Peirce's Law a bit more explicitly than /tauto/, in fact I'd like to be as explicit in my hand proof just to learn the ins and outs of Coq.

A reasonable choice, as long as you keep in mind that good, "production-quality" Coq proof scripts do not include any manual steps to prove propositional tautologies or their instantiations with concrete propositions, since [tauto] handles that.

I'll also suggest that you reconsider Peirce's Law as an essential baby step in understanding Coq.  It goes outside constructive logic, and a lot of us here think that makes it a dubious exercise to carry out. ;)

I think Coq is attempting to rewrite the goal (p) using imply_to_or, but I want Coq to rewrite H.

I don't mean to be nasty, but I am getting the feeling here that you aren't reading any introduction to Coq especially carefully.  If we answered every question at this level of detail, the list would be overwhelmed with such answers, to the detriment of more thought-provoking threads.

(Also, I don't you how you've defined [imply_to_or].  It doesn't seem to be in the default top-level environment.)