The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

         Hi Ewen,

As Jean-Christophe said, you cannot. Indeed, one way to understand the
Set/Prop distinction is to view it as a tagging of what is removed and
what is not during the program extraction.

Another one is:

* an object of type {x:A|P} is indeed a pair composed of an object of
type A and the proof that it verifies P. You thus have the two pair
projections, corresponding to the description operator.

* a object of type (EX x:A|P) is just a proof that somewhere in the
model, there exists an object in the interpretation of A verifying P
(actually verifiying the interpretation of P). But the information of
which object it is lost. So there is no hope for the first projection.

Actually, it is even possible to prove in Coq that there is no such
projection.

More generaly, it is easy to imagine that your model construction is
done in classical logic and thus you can take the axiom
(P:Prop)P\/~P

The computational axiom 
(P:Set)P+~P
however corresponds to a program which decides upon the validity of a
computational proposition (for instance it solves the halting
problem). Coq's logic is powerfull enough to show there is no such
program, and thus the latter axiom can be shown false.

In other words, the Prop/Set distinction also makes sense apart form
the program extraction question.


Hope this helps,

cheers,



Benjamin