1
$\begingroup$

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.

Interactive Theorem Proving and Program Development pg 379

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.
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – chi Oct 17 '18 at 13:16
0
$\begingroup$

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}$.

$\endgroup$
  • $\begingroup$ 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$. $\endgroup$ – Mark Oct 16 '18 at 6:34
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrej Bauer Oct 17 '18 at 15:03
  • $\begingroup$ 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}$. $\endgroup$ – Andrej Bauer Oct 17 '18 at 15:09
  • $\begingroup$ 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. $\endgroup$ – Andrej Bauer Oct 17 '18 at 15:09
  • $\begingroup$ 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. $\endgroup$ – Mark Oct 17 '18 at 15:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.