The Coq mailing list

[Adam Chlipala <adamc AT cs.berkeley.edu>]

Tom Harke wrote:

> Suppose I have an infinite stream, and I'm looking for a special element
> in it.  I don't know where it is, I only know that it definitely occurs.
> In fact, I've got a Prop demonstrating its existence.
>
> Is it possible to write a function in Set which will find this element?
> I haven't been able to, and I can't tell whether I should be able to.

My intuition is that this is impossible.  Since you aren't allowed to 
eliminate values of types in Prop to construct values of types in Set, I 
can't see how you could get any "information flow" from the existential 
witness to the return value of your function.  I don't know how to prove 
that it's impossible to write your function, though.

> I'm new to Coq and a bit unclear on its limitations.

I wouldn't call this a limitation.  Especially if you turn on 
impredicativity of Set, you can ignore Prop altogether and not have this 
problem.  The reason to choose Prop versions of constructs in the first 
place is because you _want_ to prevent functions like yours from being 
written!