The Coq mailing list

[Altenkirch Thorsten <psztxa AT exmail.nottingham.ac.uk>]

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.