2
$\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.
Improve this question
$\endgroup$
1
  • 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
    Commented Oct 17, 2018 at 13:16

1 Answer 1

Reset to default
2
$\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}$.

Improve this answer
$\endgroup$
8
  • $\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
    Commented Oct 16, 2018 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
    Commented Oct 17, 2018 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
    Commented Oct 17, 2018 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
    Commented Oct 17, 2018 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
    Commented Oct 17, 2018 at 15:37

Your Answer

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

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