The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Awesome, I stand corrected! I can think of a few examples of this, but
these resources are good pointers!

Kris


On Fri, 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.
>
>