coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Strictly positive mutual inductive types

From: Chantal Keller <chantal.keller AT wanadoo.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Strictly positive mutual inductive types
Date: Fri, 23 Feb 2018 19:53:14 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chantal.keller AT wanadoo.fr; spf=None smtp.mailfrom=chantal.keller AT wanadoo.fr; spf=None smtp.helo=postmaster AT ext.lri.fr
Ironport-phdr: 9a23:Y6X8yhaMwyPXUhTkffcSwt7/LSx+4OfEezUN459isYplN5qZocW4bnLW6fgltlLVR4KTs6sC17KN9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCazbL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAn8G/Zl89+gqxVrx2uuxNy2IvUbJ2POfdkYq/Qc9EXSGxcVchRTSxBBYa8YpMRAuoBJ+lYqZX9qEEKrRCjAAejGufvyjtWiX/swKY31PguEQHc0wwmA9IBqnDUoM/2NKgMVeC1yLfHzS/YYvJYwzj97pLHfQ0mofGLR75wf9DRxFApGgjYjVuQsZToMy6L2ukJqWSX8uhtWOK1h2I6qwx9uDeiy8ExgYfTnI0V0ErL9SBhzYY1O9K4TEl7bMa6H5pfqyGWLY92QtkjQ21ytiY60KUKuZ+9fCcU1JQq3wPTZ+KDfoSS/x7uVuacLS1liH9lYr6yiA6+8U26xe39Usm03kxKri1AktTUqn8N1wbc6s6bSvRn+ketwzWP2B7X6uFAP080j7HWKpA7zb42jJUcrEPDHijslEX4lq+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA2YE6rh27Ej2O0dICnHBBIkgWVgiAit3CO1jIPPn8RdSyh1Chin8/zPDPOKHoBtPOI3zHna3JYr974kJbz0w914YMtNpvFrgdLaerCQfKv9vCA0phal3m86PcENx4k7gmdyeKC66dPrnVtAbStP0mJeCAY4hTtiyvc6F5tc6rtmcwnBomRYfsxYEeMSrqAf1gKkmeZjzimIVZSDpYjk8FVOXvzWa6f3tTanK1Bvhu6yEnToa8DMHNXNL1jQ==

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

Section Sec.

Hypothesis A : Type.

Inductive mut : Type :=
  | M : b -> mut

with b : Type :=
  | B : A -> b.

Inductive b' : Type :=
  | B' : A -> b'.

End Sec.

Inductive x' : Type :=
  | X' : (b' x') -> x'.

Inductive x : Type :=
  | X : (b x) -> x.

[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