coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Strictly positive mutual inductive types

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Strictly positive mutual inductive types
Date: Wed, 28 Feb 2018 10:28:44 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f52.google.com
Ironport-phdr: 9a23:dm/JFxAhm/OFlgCZnna4UyQJP3N1i/DPJgcQr6AfoPdwSPryrsbcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBCPAOPfpEr4n9plsBswa+DhSxCuPoyz5HmGX53bAn2OkmFAHJxhAgH84Uv3TRt9j1Mb0dUfypzKbSyDXPdfRW2S3y6IXRdB0qvPKCXapofMfTxkQjDR7JgkuQpID/PD6ZyP4BvmiF4+dmSOmhkXQoqxtrrTiq3sosipfGhoYSyl3c8CV22oc1JdmhRE91ZN6oDIJcty+aOodoWM8iTGZouCE1yr0Cp5G3ZjQFyJMixxLHavyHdZaH4g77WeuTLjp0nm9pdKy/ihqo8kWs1PfwW8mq3FpSqypKiNjMtnQD1xzJ7ciHT+Nw/kK71jaTywDT6uBELl4plabBMJ4hxb8xmYQJvkTeBSL2l0D2g7WXdkUg4OSn9+PnYrD+qp+GK4B0kh3+MrgpmsGnHes4NREOU3GH9uS4yb3s5lb0QK5Kj/0ziqnWqorWJcUdpq6jAg9ayJwv6xilD2Tu7NNNln4eaVlBZRivjo7zOliILuqrI+24hgGJmSt3x/HLI/XaBYfAJ2WLxLLoYap07mZZwRYvxNUZ4IhbXOJSaMnvU1P84YSLRiQyNBa5lr6+WYdNk7gGUGfKOZe3dabbsFuG/OUqerDea4ocuTK7IP8gtae30S0J3GQFdKzs5qM5LWiiF608cUCQfWblh5EGC2hY5lNjHtyvs0WLVHtoX1j3X6844WtmWoevDIOGWYX1xbLchmG0GZpZYm0AAVeJQy/l

Hi,

This is a restriction of the theory, specifically the kernel implements:

(* Nested mutual inductive types are not supported *)

let auxntyp = mib.mind_ntypes in

if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));

I don't see why that is though, for example the theory of Containers justifies

the construction of nested and mutual inductive types as far as I know.

-- Matthieu

On Fri, Feb 23, 2018 at 7:54 PM Chantal Keller <chantal.keller AT wanadoo.fr> wrote:

Hi

In the attached file, I do not understand why x' can be defined whereas
the definition of x fails with the message

Error: Non strictly positive occurrence of "x" in "b x -> x".

The only difference between the two are that x' is constructed using b'
(a non-mutual inductive) whereas x is constructed using b (an inductive
which is mutual with something else).

Thanks
Chantal

[Coq-Club] Strictly positive mutual inductive types, Chantal Keller, 02/23/2018
- Re: [Coq-Club] Strictly positive mutual inductive types, Matthieu Sozeau, 02/28/2018
  - Re: [Coq-Club] Strictly positive mutual inductive types, Maxime Dénès, 02/28/2018
    - Re: [Coq-Club] Strictly positive mutual inductive types, Matthieu Sozeau, 02/28/2018