The Coq mailing list

[Jean-Baptiste Jeannin <jeannin AT cs.cornell.edu>]

Hi all,

Thanks for your answers. Thorsten's solution is exactly what we were looking 
for. Abhishek's solution is an interesting alternative where the inductive 
constructors can only appear finitely many times along each path.

Thanks,
Jean-Baptiste

On Mar 28, 2014, at 8:28 AM, Dexter Kozen wrote:

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