The Coq mailing list

["Haoyang Wang" <hywang AT pobox.com>]

On 11/23/06, Klaus Ostermann 
<ostermann AT informatik.tu-darmstadt.de>
 wrote:
> Hi all,
>
> I am new to Coq (and theorem proving) and have a few (probably trivial)
> questions that I have not found in the FAQ or elsewhere:

You need the Coq'Art book.
(<http://www.labri.fr/perso/casteran/CoqArt/>) It answers many of your
questions.

> 1) What is the technical difference between Prop and Set? The tutorial and
> the book contain a few paragraphs that look like "philosophical" differences
> (e.g., regarding proof irrelevance), but is there also a technical
> difference? I.e., a situation where I can only use Prop but not Set or vice
> versa.

Prop is impredicative, while Set is predicative (stratified). That is,
(forall x:Prop, P x) is itself still a Prop, while (forall x:Set, P x)
belongs to a different Type universe.

Proof Irrelevance does have a technical (rather than philosophical)
meaning. It means any two proofs of the same Prop type are equal. That
is, forall (P:Prop) (x y:P), x = y.

> 2) I am quite fascinated by the fact that Coq turns every proof into a
> program or function, but I wonder what these functions are good for, except
> for proving other theorems. Is there a "use case" where I have a
> constructive proof of a theorem that is then later used to extract code that
> is executed?

Yes. For example, see <http://pauillac.inria.fr/~xleroy/compcert-backend/>.

> 3) If I import the law of excluded middle and use it, Coq can still generate
> a function for each proof. How is this possible? I thought the Curry-Howard
> isomorphism breaks down then because such proofs were not constructive?

Before you execute your program, first you will have to link it
against an implementation for the excluded middle.

Surprisingly, such an implementation exists. The excluded middle can
be derived from the Peirce's law, which through the Curry-Howard
isomorphism, becomes call/cc.

So *some* of the classical proofs can be constructive.

> 4) What sets Coq apart from other proof assistants such as Isabelle/HOL?
> Probably the most significant difference is that Coq is based on the
> calculus of constructions, right? But what does this imply for a user? What
> can I do with Coq that I cannot do (easily) with Isabelle? What is Coq bad
> at?

Coq comes with a full-featured programming language embedded in its
logic, which is capable to specify complicated real-world problems.

I don't have much experience with Isabelle in order to make
comparisons, but it seems that Isabelle is more capable in solving
trivial theorems automatically. (For example, Isabelle can
automatically rewrite using local assumptions.)

Cheers,
Haoyang Wang