The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

I saw that other answers were posted while I was typing, but anyway,
here is my version.

Well, I am a relatively new user as well, so here are my newbie answers.

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

(1) When one defined an inductive type T in Set, Coq generates an
induction principle that deals with predicates of type T -> Type.
Since elements of Set are also elements of Type (and the same is true
for Prop and Type), one also gets induction for predicates T -> Set
and T -> Prop.  Now induction for T -> Set is (dependent) recurrence,
and induction for T -> Prop is our regular induction.

For example, for the type nat, recurrence has the type

forall P : nat -> Set, P 0 -> (forall n : nat, P n -> P (S n)) ->
forall n : nat, P n.

If one instantiates P with (fun _ => Z) (or (lambda x. Z) in standard
notation), where Z is the type of integers, then one gets

Z -> (nat -> Z -> Z) -> nat -> Z

which is a more familiar type of recurrence with the target type Z.

Recursion is done by case analysis, so one can branch based on whether
a natural number is 0 or (S n) and return result in Z, which is in
Set.

Now when one defined an inductive type T in Prop, Coq generates an
induction principle that deals only with predicates of type T -> Prop,
which means that there is no recursion. One can still do case analysis
but only when the target type is in Prop. For instance, one cannot
make case analysis and return something in Z.

One example is disjunction which is defined as

Inductive or (A : Prop) (B : Prop) : Prop :=
   or_introl : A -> A \/ B | or_intror : B -> A \/ B

Since it is in Prop, one cannot take a disjunction and return 0 when
the left disjunct is true and 1 if the right one is true. However, one
can prove a theorem (in Prop) by cases, i.e., construct terms of type
A -> C and B -> C where C : Prop and, using induction on or, obtain a
term of type (or A B) -> C.

In all this the assymetry appears because "datatypes" like nat, Z,
etc. are in Set. One can define "propositional natural numbers"

Inductive pnat : Prop :=
 Op : pnat |
 Sp : pnat -> pnat.

and then one can return Op or (Sp Op) depending on which disjunct is true.

(2) Since version 8.0, Set is predicative and Prop is not. See
questions 36 and 37 in FAQ.

(3) The principle of proof irrelevance has a precise meaning in that
the statement

for all A:Prop, for all p q:A, p=q

is consistent with Coq (see FAQ 34). Obviously, the same cannot be
said about Set.

(4) During program extraction, the subterms of types in Prop are left
out, and subterms of types in Set are preserved. This goes back to
"modified realizability."

> 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?

First, proofs in Coq are indeed lambda terms (which can be seen using
Print command), and they can be run, or normalized. In particular, if
all constants were transparent (see Transparent in Coq manual) then
closed terms of type or would evaluate either to (or_introl t) or
(or_intror t). Similarly,  proofs of existential quantification would
evaluate to a pair consisting of the witness and the proof of this
fact. Coq terms have a different syntax than ML, but in the simple
case (when Type and automatic tactics like ring are not used) one can
presumably write a simple translator from Coq terms to ML ones.

Now Coq's program extraction mechanism, following modified
realizability, simplifies proof terms by stripping subterms of types
in Prop. See the chapter "Extraction of programs in Objective Caml and
Haskell" in the reference manual and the file
contrib/extraction/test_extraction.v in the distribution.

> 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?

The proof is a lambda term in any case but when the law of excluded
middle is used then it contains, for example, an identifier "classic"
whose type is forall P:Prop, P \/ ~ P. This constant does not have any
reductions associated with it. So there is a question how to interpret
it during term evaluation.

In fact, one can give a meaningful computational content to the law of
excluded middle and other classical propositions, so classical proofs
*can* be evaluated with meaningful results! Moreover, sometimes this
can be done even in Coq. The chapter about program extraction
describes how to associate ML terms with uninterpreted constant
(coming from axioms) in the proof term. For more details on classical
program extractions in general see
http://www.cs.indiana.edu/~emakarov/articles/thesis.pdf.

> 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'd like to learn more about this myself.

Yevgeniy