The Coq mailing list

[roconnor AT theorem.ca]

On Fri, 12 Mar 2010, Robert Helgesson wrote:

> which is rather straight-forward until I hit precisely the problem in
> my previous message, i.e., I have to show something like
>
>  setoid_sym (setoid_sym (assoc f g h)) = assoc f g h
>
> applying proof irrelevance does indeed do away with this equality and
> subsequently makes the whole theorem pass.  Seeing the "proof
> completed" fills me with giddy joy but I'm worried that introducing
> the axiom in this situation is bad.  Am I worrying unnecessarily?

Adding the axiom is not believed to be inconsistent, so you are safe in 
that front.  Adding axioms to Coq can lead to non-canonical objects.  This 
means you can have normalized values (containing axioms) of inductive 
types that do not begin with a constructor.  However, making opaque proof 
objects (ending a proof with QED) also creates non-canonical objects, 
because an opaque proof is almost the same thing as declaring the theorem 
as an axiom.

Making opaque proofs is common practice because you very rarely need to 
reduce proof objects.  In fact, making them opaque can speed up 
computation because the reduction engine will specifically avoid reducing 
the proof objects.

So on the one hand this axioms is quite unlikely to ever cause you 
difficulties.  On the other hand I usually find these axioms are in the 
end usually unnecessary, but avoiding using such axioms can complicates 
the proof development.  As a beginner I would recommend you use your 
axioms as needed.  When you become more experienced you can learn to make 
the complex proof developments needed to avoid such axioms.

I should also add that I understand that Coq will eventually be adding 
proof irrelevence as a theorem, though I understand that there may be a 
high price to pay for such luxery (undecidable type checking).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''