The Coq mailing list

[Pierre-Marie Pédrot <pierremarie.pedrot AT ens-lyon.fr>]

On 26/02/2011 00:11, AUGER Cedric wrote:
> As Adam said, you can use some axioms.
> Another work around is to make "wf" informative (in Type).
> Its dual workaround is to put "Stream A" as non informative
> "CoInductive PStream A: Prop := Pstream: A -> PStream A -> PStream A."

If A is countable, you can still retrieve some information through the
coutable epsilon principle, as not being of the form « None » is
decidable, thus proving it without any other change whatsoever.

If you put Stream in Prop, though I am not sure, I think you are still
going to face some problems and you will need to use some weaker form of
the choice axiom (looks a lot like dependent choice in this case).

Otherwise, placing inhabited in Type should be sufficient since this is
the only point where you need to retrieve a witness (the other
properties are not really informative), and you can even show existence
of your stream in Type (with sig) instead of in Prop (with ex).

PMP

Attachment: signature.asc
Description: OpenPGP digital signature