The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

Hello,

Keiko Nakata escribió:
> Hello, 
> 
> Thank you for the explanations. 
> 
>> My suggestion would be as follows :
>>
>> - Streams (and generally coinductive types) should be defined something
>> along the lines of :
>> CoInductive Stream (A:Type) := { hd : A ; tl : Stream A }
> 
> I am specifically interested in colists, i.e., potentially infinite lists 
> with Nil and Cons constructors; records seem to me a less natural
> representation for colists. What I imagine is something like:
> 
> CoInductive Colists (A:Type) := { hd : A ; tl : Option (Colists A) }

Please notice that in this representation you only obtain non empty,
potentially infinite lists. You do not have the Nil constructor. If you
would like to consider the Nil constructor, you should rather define the
type as follows:

CoInductive Colists (A:Type) := Nil | Cons : (hd : A)(tl: Colists A).


>> - Do not use destruct or case or intros [ ] or whatever similar on a string
>> object
> 
> When I deduce a coinductive property by coinduction, 
> I case analyze a coinductive object to get a constructor, 
> therefore to get a guarded coinduction. If I cannot move to records, 
> the absence of case and the likes sounds restrictive. Am I correct?

You can use destruct and case elimination on the representation I
propose you above, and your proof will still respect the guardedness
condition.

Kind regards,
Eduardo.

> Kind regards,
> Keiko
> 
> 
> 
> 
> 
> 
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>