The Coq mailing list

["Peter Hawkins" <hawkinsp AT cs.stanford.edu>]

Hi...

No, I don't think that's what I want. If I understand things
correctly, that's a dependent type that lets me describe the type of
elements satisfying a predicate. I want _all_ elements satisfying a
predicate (as a concrete set), so I can, for example, write theorems
about properties of the set. Normally I'd want a value in Set, but I
don't think that's possible here.

Here's an example:
Suppose P : nat -> Prop denotes (relationally) a finite set of natural
numbers (say all primes less than 100). Can I talk about/write
theorems about the sum of all natural numbers n such that P n holds?

(NB. I don't care about the computational content of the proof, so
adding non-constructive axioms is fine by me)

Cheers,
Peter

On 3/3/07, Adam Chlipala 
<adamc AT cs.berkeley.edu>
 wrote:
> Peter Hawkins wrote:
> > Is there a way to express a set comprehension in Coq's type theory?
> > That is, if I have a predicate P: A->Prop, is it possible to talk
> > about the set of all x:A satisfying P?
>
> It sounds like the 'sig' type fits the bill:
>     http://coq.inria.fr/V8.1/stdlib/Coq.Init.Specif.html