The Coq mailing list

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

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.)