The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Sat, 26 Feb 2011 01:18:28 +0100,
Pierre-Marie Pédrot 
<pierremarie.pedrot AT ens-lyon.fr>
 a écrit :

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

There are always some alternative workaround I miss…

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

I don't think we require dependent choice in this case, but of course
you will lack the Stream library, and won't be able to make functions
from Stream in Prop to any Type.

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

Not sure, as inhabited is accessed via wf which is in Prop.

> 
> PMP
>