The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Yes.

Many Coq developments contain mutual-inductive definitions that contain custom specializations of generic containers like list.

The example in the first email in this thread would be rewritten in such developments as:

Inductive ty: Set :=

  | tvar : id -> ty

  | tpoly : id -> lty -> ty

with lty : Set :=

  | tnil : lty

  | tcons : ty -> lty -> lty.

I suspect that this pattern is encouraged by the good induction-principle generation (Scheme command) for mutual inductives and the lack thereof for nested inductives.

This creates unnecessary duplication of combinators on lists and their proofs. Personally, I find this duplication very unfortunate.

I hope that generating good induction principles for nested inductives will put an end to the above practice.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Oct 6, 2016 at 11:08 AM, Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:

The default inductive principles for mutual are dumb and I don't
understand why we keep on generating it.

But the ones defined by Scheme...with... . are reasonable. Mimicking
on nested inductives what Scheme does for mutual would be a very good
approximation. Won't it?

P.

2016-10-06 16:48 GMT+02:00 Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>:
> On 06/10/2016 16:44, Maxime Dénès wrote:
>> Aren't we already doing exactly that for mutual inductive types?
>
> No, the principle defined by default on mutual inductive types is
> stupid, as it does not recurse on the other types than self. Note that
> there is again a problem of canonicity here. What would be the type of
> such a principle here? Shall we return pairs? Or shall we define several
> principles?
>
> PMP
>