The Coq mailing list

[AUGER Cédric <Cedric.Auger AT lri.fr>]

Le Fri, 2 Dec 2011 11:31:23 +0100,
Arnaud Spiwack 
<arnaud AT spiwack.net>
 a écrit :

> If I understood the question correctly, the short answer is: why
> should "Record" mean "Inductive" rather than "Coinductive".

I don't think that this is the way I would understand the question.

For instance, consider the following code in Ocaml:

type 'a llist = Nil | Cons of 'a llist' * 'a llist
and llist' = {
  head : 'a;
  tail : 'a llist
}

We may wish to do usual induction here; but we cannot do that in Coq:

Inductive llist (A:Type) :=
| Nil : llist A
| Cons : llist' A → llist A → llist A
with llist' (A:Type) := {
 head : A;
 tail : llist A
}.

⇒ Error: Cannot handle mutually (co)inductive records.

That is very sad; I complained a lot on this list about that
(see [1]).

I even tried to patch coq to enable it, but I didn't have enough time
to spend to do it, and there is no quick fix since the Record structure
is shared with the one of Class; so I guess that if we make Class the
ability to be recursive or mixed with inductives (I am not sure this is
meaningfull), then this restriction on Records should be raised.

> A longer version would invoke history and stuff like that (and maybe a
> fairy or two, for the children). But to be fair, when we started
> taking the record notations seriously,

Did we really take it seriously? I remember I submitted a patch to
enable the {|...|} notation; there was a buggy printer at that time,
which used to forget to print the ending "|}" if I well remember, but
that didn't matter since this was part of a dead code at that time.

> we made the explicit choice to
> have "Inductive" for inductive stuff, "Coinductive" for coinductive
> one and "Record" for non-recursive records. The unfortunate
> non-uniformity here, that "Record" doesn't accept non-recursive
> variants is for linguistic reason and is inherited from history.

I think that keeping Record as an Inductive is a good thing, since some
people here use "induction" even for non recursive inductives, and I
fear that putting Records as CoInductive may break it (although I am
not sure, since Coq is sometimes quite smart ;) )

Maybe that adding a CoRecord maybe of some interest for some of us.

> On 30 Nov 2011 14:15, "Alexandre Pilkiewicz" <
> alexandre.pilkiewicz AT polytechnique.org>
>  wrote:
> 
> > Inductive X: Type :=
> > Con {
> >    foo    : list nat;
> >    bar    : list X
> >    }.
> >
> > will work.
> >
> > I let someone else explain why it's not always the case, because I
> > don't really understand.
> >
> > And also, I vote for a line or two about that in the
> > documentation :-)
> >
> > Alexandre
> >
> >
> > On Wed, Nov 30, 2011 at 2:09 PM, Nuno Gaspar 
> > <nmpgaspar AT gmail.com>
> > wrote:
> > > X: Type :=
> > > Con {
> > >     foo    : list Stuff;
> > >     bar    : list X
> > >     }.
> >
> >

[1]http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=1942