The Coq mailing list

["Eric Jaeger" <eric.jaeger AT sgdn.pm.gouv.fr>]

Hi, here are some newbie answers (thatwill possible cause further olbies
reactions):

> 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 supposed to be the sort for logic, Set the sort for computations.

As far as I've noted, they ARE differences between Prop and Set, especially
when dealing with elimination; to enforce (or rather to avoid contradiction
with) proof irrelevance, you are not supposed to destruct Prop constructs
(proving that two proofs of the same proposition are not equal is not a good
idea if you have just assumed proof irrelevance). So, in terms of visible
differences when using Coq, you may for example find that you cannot
"destruct" a Prop hypothesis to prove a Set goal, or vice-versa (I do not
remember). If you want to test that, just redefine e.g. <= in the Set sort
and play with it (that means, prove various theorems).

You can also decide to use only the Set sort in your developments, even to
describe logic types, that will only looks "weird" to other users.

> 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, a very simple one : once again, take the <= relation, prove that it is
decidable, i.e. {i<=j}+{i<=j->False}, but instead if ending your proof with
"Qed" use "Defined"; this proof then defines a function computing "i<=j" and
returning a (form of) boolean, that can be extracted. Note that the term
"{i<=j}+{i<=j->False}" inhabits the Set sort and that you can for example
makes pattern matching on it.

> 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?
In such case, if EM is used in the proof, the associated extracted function
will call the EM function... The EM being provided as an axiom (i.e. you got
the signature but not its implementation), the extracted function is
unlikely to be of any use.

> 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?
I let this troll to more involved people ;-)

    Regards, Eric