coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Equality for inductive type containing list
Date: Thu, 6 Oct 2016 17:08:19 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f50.google.com
Ironport-phdr: 9a23:pSJ20B+QXJ+QrP9uRHKM819IXTAuvvDOBiVQ1KB90ugcTK2v8tzYMVDF4r011RmSDN+dsKgP27Ce8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJdb974EY/Kjsmxy/v6u9iKO10J13KBZuZZKwz+hgHMvIFCiox7b6011xHho31Seu0Qy3k+dnyJmBOp3sa95oRuuw9Xpug99sNdGfHifqkiV7EeBzM7KXw06dDDuhzKTA/J7XwZBDZF2iFUChTIuUmpFqz6tTH3468kgHGX

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
>

[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
        
        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, Dominique Larchey-Wendling, 10/07/2016