# Understanding the definition of Positivity Constraints in Coq

In Interactive Theorem Proving and Program Development the authors explain constraints on constructors of inductive types in Coq.

For inductive type $$T$$, a constructor must have the form $$t_1 \rightarrow t_2 \rightarrow ... \rightarrow t_l \rightarrow T a_1 ... a_k$$ where $$k$$ is the number of arguments of the inductive type $$T$$.

There are some restrictions placed on the $$t_i$$s, which I cannot understand.

If $$t_i$$ is the type of a constant, then $$t_i$$ can have the form "$$g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k}),$$" provided the expressions $$b_{i,j}$$ also satisfy the typing rules, and $$T$$ does not occur in these expressions or in $$g$$.

and

If $$t_i$$ is the type of a function, this type can have the form $$t_1'\rightarrow ... \rightarrow t'_m \rightarrow g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$$ but the type $$T$$ cannot occur in the expressions $$t'_1, ... t'_m$$ or in the expressions $$b_{i,j}$$

I am confused on what it means for a type $$t_i$$ "to have the form of $$g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$$".

For instance, does nat (the type of natural numbers) have the form of $$g(Tb_{1,1} ... b_{1,k})...(Tb_{l,1} ... b_{l,k})$$"?

If so, how does nat obtain such a elaborate form? What is $$g$$ and what are the terms in the $$(l,k)$$ matrix $$b_{i,j}$$?

If not, am I prohibited from using nat in type constructors of inductive types? (That would seem absurd...)

Below I have uploaded a screenshot of the page in question. Update: I was able to construct a counterexample to the textbook:

Definition g := fun x y z : Type => nat.

Inductive T : Set :=
t : (g T T T) -> T.


Here $$l = 1, k = 0$$, and $$t_1$$ can only have the form $$g(T)$$ but I was able to use $$T$$ 3 times inside an actual Coq environment.

Edit 2: I think what you guys are saying about the reduced form makes sense so I tried to make another "counterexample"

Inductive g (x y z: Type) : Set.

Inductive T : Set :=
t : (g T T T) -> T.

• I think Coq reduces g T T T to its normal form nat, and then checks the resulting t: nat -> T which complies with the rules. The book probably does not mention this normalization step. – chi Oct 17 '18 at 13:16

Take $$l = k = 0$$, the matrix of $$b_{ij}$$'s has size $$0 \times 0$$, hence we do not have to defined any $$b_{ij}$$, and take $$g = \mathbf{nat}$$.
• Thanks for your answer @AndrejBauer but I don't think we can choose $l, k$ aribitrarily. In fact, they are related to the terms in the constructor. So $l = 1$ since the constructor would have one argument of type nat and $k$ is decided by the number of arguments to the inductive type $T$. – Mark Oct 16 '18 at 6:34
• You misunderstand the textbook. The $g$ and the $b_{ij}$ are schematic, i.e., they show you the form of syntax that can be used, and are not meant to be actual Coq code. Your counter-example reduces to Inductive T : Set := t : nat -> T by the definition of g and shows nothing. You need to compare the reduced definition of T (i.e., with the definition of g unfolded) to the indicated forms in the textbook. But I doubt I can explain this point in a comment, unless you understand the difference between a meta-variable and a variable. – Andrej Bauer Oct 17 '18 at 15:03
• To address your comment further: I did not "choose $l$, $k$ arbitrarily". You might be confused about how to quantify $l$ and $k$. If we want to verify that some particular expression $E$ has the form $g (T b_{1,1} \ldots b_{1,k}) \cdots (T b_{l,1} \ldots b_{l,k})$ then we need to find $l, k$, the $b_{ij}$'s and the $g$ so that we end up getting $E$. Example: take $l = 1$, $k = 2$, $b_{11} = a$, $b_{12} = a$, and $g(x) = \sqrt{1+x}$. (I purposely use strange things to emphasize that these are purely syntactic manipulations of expressions.) Then $g(T b_{11} b_{12}) = \sqrt{1 + T a a}$. – Andrej Bauer Oct 17 '18 at 15:09
• Consider the case $l = k = 0$: then $g (T b_{1,1} \ldots b_{1,k}) \cdots (T b_{l,1} \ldots b_{l,k})$ is just $g$. Furthermore, consider $g = \mathbf{nat}$. Then we get just $\mathbf{nat}$. This is precisely what you asked for: what should we take for $l$, $k$, $b_{ij}$ and $g$ so that $g (T b_{1,1} \ldots b_{1,k}) \cdots (T b_{l,1} \ldots b_{l,k})$ becomes equal to $\mathbf{nat}$. I just answered your question. – Andrej Bauer Oct 17 '18 at 15:09
• I think what you are saying about reduced definition makes sense. But I'm still confused about $l =0$. $g$ is the schematic of a type $t_i$ inside one of the arguments of a constructor for inductive type $T$. But this means that the constructor has at least one argument (namely $t_i$) and therefore $l$ (the number of $i$'s is greater than or equal to 1. – Mark Oct 17 '18 at 15:37