Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more than welcome!

Page 122 of the Coq reference manual describes the strict positivity criteria:

The constant X occurs strictly positively in T in the following cases:

  • X does not occur in T
  • T converts to (X t1 . . . tn) and X does not occur in any of ti
  • T converts to ∀ x : U, V and X does not occur in type U but occurs strictly positively in type V
  • T converts to (I a1 . . . am t1 . . . tp) where I is the name of an inductive declaration of the form Ind(Γ)[m](I : A := c1 : ∀p1 : P1, . . . ∀pm : Pm, C1; . . . ; cn : ∀p1 : P1, . . . ∀pm : Pm, Cn ) (in particular, it is not mutually defined and it has m parameters) and X does not occur in any of the ti , and the (instantiated) types of constructor Ci{pj/aj}j=1...m of I satisfy the nested positivity condition for X

The emphasis (i.e., around "not mutually defined") was added by me.

Why is I required to not be mutually defined? If we removed this restriction (i.e., we allowed I to be mutually defined), would this introduce inconsistency into the system? If so, I'd greatly appreciate an example (e.g., where you prove False).

  • 2
    $\begingroup$ Mutually defined inductive types can be encoded as a single inductive type (provided they live in the same sort), so I don't think the restriction is foundational. If I had to guess, I'd bet that this has to do with implementation hassle. $\endgroup$ Commented Aug 15, 2023 at 11:04


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.