The Coq mailing list

[Dexter Kozen <kozen AT cs.cornell.edu>]

Hi Thorsten,
That's  exactlly what we wanted, except instead
of 'gets' and 'puts' we have something else, but we
wanted exactly that behavior.
Thanks!
Dexter

On Mar 28, 2014, at 6:48 AM, Altenkirch Thorsten 
<psztxa AT exmail.nottingham.ac.uk>
 wrote:

> There are many examples of inductive – coinductive definitions. My favorite 
> one is Stream processors:
> 
> data SP (I O : Set) : Set where
> 
>   get : (I -> SP I O) -> SP I O
>   put : O -> \infty (SP I O) -> SP I O
> 
> The idea is that you can have only finitely many gets between any two puts 
> but you can have infinitely many puts. In Agda you can achieve this by 
> simply putting the \infty symbol in front of the recursive occurrence of 
> the type. In Coq that can be achieved by a hack by Tarmo Uustalu and Keiko 
> Nakata.
> 
> Hence in Agda your type could be translated as 
> 
> data even_list : Set
> data odd_list : Set
> 
> data even_list where
>      ENil : even_list
>      ECons : nat -> odd_list -> even_list
> 
> data odd_list : Set 
>     OCons : nat -> \infty even_list -> odd_list.
> 
> However, in a way this is a bad example because it doesn't really matter 
> wether one or both constructors are coinductive. 
> 
> Cheers,
> Thorsten
> 
> See
> 
> Subtyping, Declaratively - An Exercise in Mixed Induction and Coinduction
> http://www.cs.nott.ac.uk/~txa/publ/danielsson-altenkirch-subtyping.pdf
> 
> Termination Checking Nested Inductive and Coinductive Types
> http://www.cs.nott.ac.uk/~txa/publ/InvertedQuantifiers.pdf
> 
> 
> From: Jean-Baptiste Jeannin 
> <jeannin AT cs.cornell.edu>
> Reply-To: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Date: Thu, 27 Mar 2014 18:55:46 +0000
> To: 
> "coq-club AT inria.fr"
>  
> <coq-club AT inria.fr>
> Cc: Dexter Kozen 
> <kozen AT cs.cornell.edu>,
>  Konstantinos Mamouras 
> <mamouras AT cs.cornell.edu>
> Subject: [Coq-Club] Mixing Inductive and CoInductive 
> constructors/destructors in the same type
> 
>> Hi,
>> 
>> I am trying to define a type with both inductive constructors and 
>> coinductive constructors (really destructors).
>> 
>> With the [Inductive] keyword, I can define a type with all constructors 
>> inductive, as in:
>> 
>> Inductive list: Type:=
>>   | LNil : list
>>   | LCons : nat -> list -> list.
>> 
>> and similarly with the [CoInductive] keyword, I can define a type with all 
>> constructors coinductive, as in:
>> 
>> CoInductive stream : Type :=
>>   | SCons : nat -> stream -> stream.
>> 
>> If I want some constructors to be inductive and others to be coinductive, 
>> an idea I had was to use two mutually recursive types, with a construct 
>> akin to:
>> 
>> CoInductive even_list : Set :=
>> | ENil : even_list
>> | ECons : nat -> odd_list -> even_list
>> with odd_list : Set :=
>> | OCons : nat -> even_list -> odd_list.
>> 
>> But I can't seem to make odd_list just [Inductive], while keeping 
>> even_list [CoInductive]. Is there any way I could do this? Or any other 
>> way to mix Inductive and CoInductive constructors?
>> 
>> (examples taken or inspired from 
>> http://adam.chlipala.net/cpdt/html/Coinductive.html and 
>> http://adam.chlipala.net/cpdt/html/InductiveTypes.html)
>> Thank you,
>> Jean-Baptiste
> 
> This message and any attachment are intended solely for the addressee and 
> may contain confidential information. If you have received this message in 
> error, please send it back to me, and immediately delete it.   Please do 
> not use, copy or disclose the information contained in this message or in 
> any attachment.  Any views or opinions expressed by the author of this 
> email do not necessarily reflect the views of the University of Nottingham.
> This message has been checked for viruses but the contents of an attachment 
> may still contain software viruses which could damage your computer system, 
> you are advised to perform your own checks. Email communications with the 
> University of Nottingham may be monitored as permitted by UK legislation.
>