The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Why should this make sense?  You want the possibility of infinite even
lists, but only want finite odd lists?  If that's the case, you could
define simply even lists as a coninductive type and then a predicate
over finite elements of that type that add one to each thing.
However, I'm pretty sure that what you're asking doesn't make sense,
since it seems like if you want to allow for the possibility of
infinite even lists, you also need to allow for the possibility of
infinite odd lists, especially if you're defining them together.

Kris




On Thu, Mar 27, 2014 at 2:55 PM, Jean-Baptiste Jeannin
<jeannin AT cs.cornell.edu>
 wrote:
> 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