Module positivity 

Strict positivity checking for inductive types.

An inductive type must appear only in “strictly positive” positions in its constructors. Without this check, we could define paradoxical types like:

Inductive Bad := Cons : (Bad -> False) -> Bad

This would allow encoding Russell’s paradox and proving False.

Strict Positivity Rules (from CIC):

I is strictly positive in T iff:

1. I does not occur in T, OR
2. T = Π(x:A). B where:
   • If A = I exactly, it’s a “recursive argument” (allowed)
   • Otherwise, I must NOT occur in A at all
   • AND I must be strictly positive in B

Examples:

• I -> I is valid: first I is a recursive argument, second is result
• (I -> X) -> I is INVALID: I occurs inside the param type of another arrow
• X -> I -> I is valid: X has no I, second param is recursive arg

Functions

check_positivity

Check strict positivity of an inductive type in a constructor type.