The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Thanks Andreas! 

That might work with a correction. If I understand correctly your definition 
gives:

f_1 : A -> A   and the next P is f_1 x = a ,

f_2 : { a : A ; f_1 x = a } -> A  and the next P is  something like  ~ ( f_1 
x = a ) \/ ((f_1 x = a ) /\ ( f_2 x = a )) ,

f_3 : { a : A ; ~ ( f_1 x = a ) \/ ((f_1 x = a ) /\ ( f_2 x = a )) } which is 
not quite right. 

So may be :

CoInductive Stream (P : A -> Prop) : Type :=
 cons : forall
         (head : { x : A | P x } -> A)
         (tail : Stream (fun x => ( P x ) /\ ( forall (p : P x),
                           head (exist (fun x => P x) x p) = a)) ),
        Stream P.

Vladimir. 



On Jun 27, 2011, at 5:14 AM, Andreas Abel wrote:

> Hello Vladimir,
> 
> does this serve your purpose?
> 
> Variable A : Type.
> Variable a : A.
> 
> CoInductive Stream (P : A -> Prop) : Type :=
>  cons : forall
>          (head : { x : A | P x } -> A)
>          (tail : Stream (fun x => forall (p : P x),
>                            head (exist (fun x => P x) x p) = a)),
>         Stream P.
> 
> Definition VS := Stream (fun x => True).
> 
> Cheers,
> Andreas
> 
> On 27.06.11 2:30 AM, Vladimir Voevodsky wrote:
>> Is there a way to define in Coq the type which can be informally
>> described as follows:
>> 
>> 1. Given parameters A : Type , a : A .
>> 
>> 2. I want to define the type of (infinite) sequences f_0 ,..., f_n,
>> .... where
>> 
>> 2a. f_0 : A ->  A .
>> 
>> 2b. f_{S n} : {| x : A ; f_n x = a |} ->  A .
>> 
>> Is there a way to define the type of such sequences ?
>> 
> 
> -- 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel AT ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/