coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Equality for inductive type containing list

From: Maxime Dénès <mail AT maximedenes.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Equality for inductive type containing list
Date: Thu, 6 Oct 2016 16:44:40 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mail AT maximedenes.fr; spf=Pass smtp.mailfrom=mail AT maximedenes.fr; spf=None smtp.helo=postmaster AT 1.mo5.mail-out.ovh.net
Ironport-phdr: 9a23:KlMkzxCQkxCpKzcjudvUUyQJP3N1i/DPJgcQr6AfoPdwSP38p8bcNUDSrc9gkEXOFd2CrakV0ayN6eu/ByRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUt2as8Pi3OervpbXfg9ghTynYLo0Ig/lgx/Ws5wziJtjL6t55prPImAAL+FfxGdAIFuDnhPx6sq28YUl/T4G6KFpzNJJTaivJ/dwdrdfFjlza20=

Aren't we already doing exactly that for mutual inductive types?

Maxime.

On 10/06/16 16:41, Pierre-Marie Pédrot wrote:
> On 06/10/2016 16:29, Dominique Larchey-Wendling wrote:
>> So I wonder why the nested induction required by the type of trees ty
>> is still not guessed when Coq generates induction principles.
>
> As far as I can tell, there is no canonical induction principle
> corresponding to nested inductive types (e.g. here ty depends on list
> ty). If we agreed on some standard way, depending for instance on the
> fold of the underlying structure, we could easily generate such code.
>
> PMP
>

[Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
- Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
  - Re: [Coq-Club] Equality for inductive type containing list, Clément Pit--Claudel, 10/06/2016
  - Re: [Coq-Club] Equality for inductive type containing list, Klaus Ostermann, 10/06/2016
    - Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
      - Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Maxime Dénès, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/06/2016
        Re: [Coq-Club] Equality for inductive type containing list, Abhishek Anand, 10/06/2016
        Re: [Coq-Club] Equality for inductive type containing list, Dominique Larchey-Wendling, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Jonathan Leivent, 10/06/2016
        
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/06/2016
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016
        Re: [Coq-Club] Equality for inductive type containing list, Pierre Courtieu, 10/07/2016
        Re: [Coq-Club] Equality for inductive type containing list, Matthieu Sozeau, 10/07/2016
        Re: [Coq-Club] Equality for inductive type containing list, Pierre-Marie Pédrot, 10/07/2016