$$\begin{array}{}\end{array}$$

Typing rules

The underlying formal language of Coq is a Calculus of Inductive Constructions (CIC) whose inference rules are presented in this chapter. The history of this formalism as well as pointers to related work are provided in a separate chapter; see Early history of Coq.

The terms

The expressions of the CIC are terms and all terms have a type. There are types for functions (or programs), there are atomic types (especially datatypes)... but also types for proofs and types for the types themselves. Especially, any object handled in the formalism must belong to a type. For instance, universal quantification is relative to a type and takes the form “for all x of type $T$, $P$”. The expression “$x$ of type $T$” is written “$x:T$”. Informally, “$x:T$” can be thought as “$x$ belongs to $T$”.

Terms are built from sorts, variables, constants, abstractions, applications, local definitions, and products. From a syntactic point of view, types cannot be distinguished from terms, except that they cannot start by an abstraction or a constructor. More precisely the language of the Calculus of Inductive Constructions is built from the following rules.

1. the sorts $\mathsf{\text{SProp}}$, $\mathsf{\text{Prop}}$, $\mathsf{\text{Set}}$, $\mathsf{\text{Type}}(i)$ are terms.

2. variables, hereafter ranged over by letters $x$, $y$, etc., are terms

3. constants, hereafter ranged over by letters $c$, $d$, etc., are terms.

4. if $x$ is a variable and $T$, $U$ are terms then $\forall x:T,U$ (forall x:T, U in Coq concrete syntax) is a term. If $x$ occurs in $U$, $\forall x:T,U$ reads as “for all $x$ of type $T$, $U$”. As $U$ depends on $x$, one says that $\forall x:T,U$ is a dependent product. If $x$ does not occur in $U$ then $\forall x:T,U$ reads as “if $T$ then $U$”. A non-dependent product can be written: $T\to U$.

5. if $x$ is a variable and $T$, $u$ are terms then $\lambda x:T.u$ (fun x:T => u in Coq concrete syntax) is a term. This is a notation for the λ-abstraction of λ-calculus [Bar81]. The term $\lambda x:T.u$ is a function which maps elements of $T$ to the expression $u$.

6. if $t$ and $u$ are terms then $(tu)$ is a term (t u in Coq concrete syntax). The term $(tu)$ reads as “$t$ applied to $u$”.

7. if $x$ is a variable, and $t$, $T$ and $u$ are terms then $\mathsf{\text{let}}x:=t:T\mathsf{\text{in}}u$ is a term which denotes the term $u$ where the variable $x$ is locally bound to $t$ of type $T$. This stands for the common “let-in” construction of functional programs such as ML or Scheme.

Free variables. The notion of free variables is defined as usual. In the expressions $\lambda x:T.U$ and $\forall x:T,U$ the occurrences of $x$ in $U$ are bound.

Substitution. The notion of substituting a term $t$ to free occurrences of a variable $x$ in a term $u$ is defined as usual. The resulting term is written $u\{x/t\}$.

The logical vs programming readings. The constructions of the CIC can be used to express both logical and programming notions, according to the Curry-Howard correspondence between proofs and programs, and between propositions and types [CFC58][How80][dB72].

For instance, let us assume that $\mathsf{\text{nat}}$ is the type of natural numbers with zero element written $0$ and that True is the always true proposition. Then $\to$ is used both to denote $\mathsf{\text{nat}}\to \mathsf{\text{nat}}$ which is the type of functions from $\mathsf{\text{nat}}$ to $\mathsf{\text{nat}}$, to denote True→True which is an implicative proposition, to denote $\mathsf{\text{nat}}\to \mathsf{\text{Prop}}$ which is the type of unary predicates over the natural numbers, etc.

Let us assume that mult is a function of type $\mathsf{\text{nat}}\to \mathsf{\text{nat}}\to \mathsf{\text{nat}}$ and eqnat a predicate of type $\mathsf{\text{nat}}\to \mathsf{\text{nat}}\to \mathsf{\text{Prop}}$. The λ-abstraction can serve to build “ordinary” functions as in $\lambda x:\mathsf{\text{nat}}.(\mathsf{\text{mult}}xx)$ (i.e. fun x:nat => mult x x in Coq notation) but may build also predicates over the natural numbers. For instance $\lambda x:\mathsf{\text{nat}}.(\mathsf{\text{eqnat}}x0)$ (i.e. fun x:nat => eqnat x 0 in Coq notation) will represent the predicate of one variable $x$ which asserts the equality of $x$ with $0$. This predicate has type $\mathsf{\text{nat}}\to \mathsf{\text{Prop}}$ and it can be applied to any expression of type $\mathsf{\text{nat}}$, say $t$, to give an object $Pt$ of type $\mathsf{\text{Prop}}$, namely a proposition.

Furthermore forall x:nat, P x will represent the type of functions which associate with each natural number $n$ an object of type $(Pn)$ and consequently represent the type of proofs of the formula “$\forall x.P(x)$”.

Typing rules

As objects of type theory, terms are subjected to type discipline. The well typing of a term depends on a local context and a global environment.

Local context. A local context is an ordered list of declarations of variables. The declaration of a variable $x$ is either an assumption, written $x:T$ (where $T$ is a type) or a definition, written $x:=t:T$. Local contexts are written in brackets, for example $[x:T;y:=u:U;z:V]$. The variables declared in a local context must be distinct. If $\Gamma$ is a local context that declares $x$, we write $x\in \Gamma$. Writing $(x:T)\in \Gamma$ means there is an assumption or a definition giving the type $T$ to $x$ in $\Gamma$. If $\Gamma$ defines $x:=t:T$, we also write $(x:=t:T)\in \Gamma$. For the rest of the chapter, $\Gamma ::(y:T)$ denotes the local context $\Gamma$ enriched with the local assumption $y:T$. Similarly, $\Gamma ::(y:=t:T)$ denotes the local context $\Gamma$ enriched with the local definition $(y:=t:T)$. The notation $[]$ denotes the empty local context. Writing ${\Gamma }_1;{\Gamma }_2$ means concatenation of the local context ${\Gamma }_1$ and the local context ${\Gamma }_2$.

Global environment. A global environment is an ordered list of declarations. Global declarations are either assumptions, definitions or declarations of inductive objects. Inductive objects declare both constructors and inductive or coinductive types (see Section Theory of inductive definitions).

In the global environment, assumptions are written as $(c:T)$, indicating that $c$ is of the type $T$. Definitions are written as $c:=t:T$, indicating that $c$ has the value $t$ and type $T$. We shall call such names constants. For the rest of the chapter, the $E;c:T$ denotes the global environment $E$ enriched with the assumption $c:T$. Similarly, $E;c:=t:T$ denotes the global environment $E$ enriched with the definition $(c:=t:T)$.

The rules for inductive definitions (see Section Theory of inductive definitions) have to be considered as assumption rules in which the following definitions apply: if the name $c$ is declared in $E$, we write $c\in E$ and if $c:T$ or $c:=t:T$ is declared in $E$, we write $(c:T)\in E$.

Typing rules. In the following, we define simultaneously two judgments. The first one $E[\mathrm{\Gamma }]⊢t:T$ means the term $t$ is well-typed and has type $T$ in the global environment $E$ and local context $\Gamma$. The second judgment $\mathcal{W}\mathcal{F}(E)[\Gamma ]$ means that the global environment $E$ is well-formed and the local context $\Gamma$ is a valid local context in this global environment.

A term $t$ is well typed in a global environment $E$ iff there exists a local context $\mathrm{\Gamma }$ and a term $T$ such that the judgment $E[\mathrm{\Gamma }]⊢t:T$ can be derived from the following rules.

W-Empty

$$\frac{}{\mathcal{W}\mathcal{F}([])[]}$$

W-Local-Assum

$$\frac{E[\mathrm{\Gamma }]⊢T:ss\in \mathcal{S}x\notin \mathrm{\Gamma }}{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }::(x:T)]}$$

W-Local-Def

$$\frac{E[\mathrm{\Gamma }]⊢t:Tx\notin \mathrm{\Gamma }}{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }::(x:=t:T)]}$$

W-Global-Assum

$$\frac{E[]⊢T:ss\in \mathcal{S}c\notin E}{\mathcal{W}\mathcal{F}(E;c:T)[]}$$

W-Global-Def

$$\frac{E[]⊢t:Tc\notin E}{\mathcal{W}\mathcal{F}(E;c:=t:T)[]}$$

Ax-SProp

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }]}{E[\mathrm{\Gamma }]⊢\mathsf{\text{SProp}}:\mathsf{\text{Type}}(1)}$$

Ax-Prop

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }]}{E[\mathrm{\Gamma }]⊢\mathsf{\text{Prop}}:\mathsf{\text{Type}}(1)}$$

Ax-Set

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }]}{E[\mathrm{\Gamma }]⊢\mathsf{\text{Set}}:\mathsf{\text{Type}}(1)}$$

Ax-Type

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }]}{E[\mathrm{\Gamma }]⊢\mathsf{\text{Type}}(i):\mathsf{\text{Type}}(i+1)}$$

Var

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }](x:T)\in \mathrm{\Gamma }\text{or}(x:=t:T)\in \mathrm{\Gamma }\text{for some }t}{E[\mathrm{\Gamma }]⊢x:T}$$

Const

$$\frac{\mathcal{W}\mathcal{F}(E)[\mathrm{\Gamma }](c:T)\in E\text{or}(c:=t:T)\in E\text{for some }t}{E[\mathrm{\Gamma }]⊢c:T}$$

Prod-SProp

$$\frac{E[\mathrm{\Gamma }]⊢T:ss\in \mathcal{S}E[\mathrm{\Gamma }::(x:T)]⊢U:\mathsf{\text{SProp}}}{E[\mathrm{\Gamma }]⊢\mathrm{\forall }x:T,U:\mathsf{\text{SProp}}}$$

Prod-Prop

$$\frac{E[\mathrm{\Gamma }]⊢T:ss\in \mathcal{S}E[\mathrm{\Gamma }::(x:T)]⊢U:\mathsf{\text{Prop}}}{E[\mathrm{\Gamma }]⊢\forall x:T,U:\mathsf{\text{Prop}}}$$

Prod-Set

$$\frac{E[\mathrm{\Gamma }]⊢T:ss\in \{\mathsf{\text{SProp}},\mathsf{\text{Prop}},\mathsf{\text{Set}}\}E[\mathrm{\Gamma }::(x:T)]⊢U:\mathsf{\text{Set}}}{E[\mathrm{\Gamma }]⊢\forall x:T,U:\mathsf{\text{Set}}}$$

Prod-Type

$$\frac{E[\mathrm{\Gamma }]⊢T:ss\in \{\mathsf{\text{SProp}},\mathsf{\text{Type}}(i)\}E[\mathrm{\Gamma }::(x:T)]⊢U:\mathsf{\text{Type}}(i)}{E[\mathrm{\Gamma }]⊢\forall x:T,U:\mathsf{\text{Type}}(i)}$$

Lam

$$\frac{E[\mathrm{\Gamma }]⊢\forall x:T,U:sE[\mathrm{\Gamma }::(x:T)]⊢t:U}{E[\mathrm{\Gamma }]⊢\lambda x:T.t:\forall x:T,U}$$

App

$$\frac{E[\mathrm{\Gamma }]⊢t:\forall x:U,TE[\mathrm{\Gamma }]⊢u:U}{E[\mathrm{\Gamma }]⊢(tu):T\{x/u\}}$$

Let

$$\frac{E[\mathrm{\Gamma }]⊢t:TE[\mathrm{\Gamma }::(x:=t:T)]⊢u:U}{E[\mathrm{\Gamma }]⊢\mathsf{\text{let}}x:=t:T\mathsf{\text{in}}u:U\{x/t\}}$$

Note

Prod-Prop and Prod-Set typing-rules make sense if we consider the semantic difference between $\mathsf{\text{Prop}}$ and $\mathsf{\text{Set}}$:

• All values of a type that has a sort $\mathsf{\text{Set}}$ are extractable.

• No values of a type that has a sort $\mathsf{\text{Prop}}$ are extractable.

Note

We may have $\mathsf{\text{let}}x:=t:T\mathsf{\text{in}}u$ well-typed without having $((\lambda x:T.u)t)$ well-typed (where $T$ is a type of $t$). This is because the value $t$ associated with $x$ may be used in a conversion rule (see Section Conversion rules).

Subtyping rules

At the moment, we did not take into account one rule between universes which says that any term in a universe of index $i$ is also a term in the universe of index $i+1$ (this is the cumulativity rule of CIC). This property extends the equivalence relation of convertibility into a subtyping relation inductively defined by:

1. if $E[\Gamma ]⊢t{=}_{\beta \delta \iota \zeta \eta }u$ then $E[\Gamma ]⊢t{\le }_{\beta \delta \iota \zeta \eta }u$,

2. if $i\le j$ then $E[\Gamma ]⊢\mathsf{\text{Type}}(i){\le }_{\beta \delta \iota \zeta \eta }\mathsf{\text{Type}}(j)$,

3. for any $i$, $E[\Gamma ]⊢\mathsf{\text{Set}}{\le }_{\beta \delta \iota \zeta \eta }\mathsf{\text{Type}}(i)$,

4. $E[\Gamma ]⊢\mathsf{\text{Prop}}{\le }_{\beta \delta \iota \zeta \eta }\mathsf{\text{Set}}$, hence, by transitivity, $E[\Gamma ]⊢\mathsf{\text{Prop}}{\le }_{\beta \delta \iota \zeta \eta }\mathsf{\text{Type}}(i)$, for any $i$ (note: $\mathsf{\text{SProp}}$ is not related by cumulativity to any other term)

5. if $E[\Gamma ]⊢T{=}_{\beta \delta \iota \zeta \eta }U$ and $E[\Gamma ::(x:T)]⊢T^{\prime }{\le }_{\beta \delta \iota \zeta \eta }{U}^{\prime }$ then $E[\Gamma ]⊢\forall x:T,T\prime {\le }_{\beta \delta \iota \zeta \eta }\forall x:U,U\prime$.

6. if $\mathsf{\text{Ind}}[p]\left({\Gamma }_I:={\Gamma }_C\right)$ is a universe polymorphic and cumulative (see Chapter Polymorphic Universes) inductive type (see below) and $(t:\forall {\Gamma }_P,\forall {\Gamma }_{\mathit{Arr}(t)},S)\in {\Gamma }_I$ and $(t^{\prime }:\forall {\Gamma }_P^{\prime },\forall {\Gamma }_{\mathit{Arr}(t)}^{\prime },S^{\prime })\in {\Gamma }_I$ are two different instances of the same inductive type (differing only in universe levels) with constructors

   $$[c_1:\forall {\Gamma }_P,\forall T_{1,1}\dots T_{1,n_1},t{v}_{1,1}\dots v_{1,m};\dots ;c_k:\forall {\Gamma }_P,\forall T_{k,1}\dots T_{k,n_k},t{v}_{k,1}\dots v_{k,m}]$$

   and

   $$[c_1:\forall {\Gamma }_P^{\prime },\forall T_{1,1}^{\prime }\dots T_{1,n_1}^{\prime },t^{\prime }{v}_{1,1}^{\prime }\dots v_{1,m}^{\prime };\dots ;c_k:\forall {\Gamma }_P^{\prime },\forall T_{k,1}^{\prime }\dots T_{k,n_k}^{\prime },t^{\prime }{v}_{k,1}^{\prime }\dots v_{k,m}^{\prime }]$$

   respectively then

   $$E[\Gamma ]⊢t{w}_1\dots w_m{\le }_{\beta \delta \iota \zeta \eta }{t}^{\prime }{w}_1^{\prime }\dots w_m^{\prime }$$

   (notice that $t$ and $t^{\prime }$ are both fully applied, i.e., they have a sort as a type) if

   $$E[\Gamma ]⊢w_i{=}_{\beta \delta \iota \zeta \eta }{w}_i^{\prime }$$

   for $1\le i\le m$ and we have

   $$E[\Gamma ]⊢T_{i,j}{\le }_{\beta \delta \iota \zeta \eta }{T}_{i,j}^{\prime }$$

   and

   $$E[\Gamma ]⊢A_i{\le }_{\beta \delta \iota \zeta \eta }{A}_i^{\prime }$$

   where ${\Gamma }_{\mathit{Arr}(t)}=[a_1:A_1;\dots ;a_l:A_l]$ and ${\Gamma }_{\mathit{Arr}(t)}^{\prime }=[a_1:A_1^{\prime };\dots ;a_l:A_l^{\prime }]$.

The conversion rule up to subtyping is now exactly:

Conv

$$\frac{E[\Gamma ]⊢U:sE[\Gamma ]⊢t:TE[\Gamma ]⊢T{\le }_{\beta \delta \iota \zeta \eta }U}{E[\Gamma ]⊢t:U}$$

Normal form. A term which cannot be any more reduced is said to be in normal form. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the head reduction which will play an important role (see Chapter Tactics). Any term $t$ can be written as $\lambda x_1:T_1.\dots \lambda x_k:T_k.(t_0{t}_1\dots t_n)$ where $t_0$ is not an application. We say then that $t_0$ is the head of $t$. If we assume that $t_0$ is $\lambda x:T.u_0$ then one step of β-head reduction of $t$ is:

$$\lambda x_1:T_1.\dots \lambda x_k:T_k.(\lambda x:T.u_0{t}_1\dots t_n)▹\lambda (x_1:T_1)\dots (x_k:T_k).(u_0\{x/t_1\}{t}_2\dots t_n)$$

Iterating the process of head reduction until the head of the reduced term is no more an abstraction leads to the β-head normal form of $t$:

$$t▹\dots ▹\lambda x_1:T_1.\dots \lambda x_k:T_k.(v{u}_1\dots u_m)$$

where $v$ is not an abstraction (nor an application). Note that the head normal form must not be confused with the normal form since some $u_i$ can be reducible. Similar notions of head-normal forms involving δ, ι and ζ reductions or any combination of those can also be defined.

The Calculus of Inductive Constructions with impredicative Set

Coq can be used as a type checker for the Calculus of Inductive Constructions with an impredicative sort $\mathsf{\text{Set}}$ by using the compiler option -impredicative-set. For example, using the ordinary coqtop command, the following is rejected,

Example

Fail Definition id: Set := forall X:Set,X->X.

The command has indeed failed with message: The term "forall X : Set, X -> X" has type "Type" while it is expected to have type "Set" (universe inconsistency: Cannot enforce Set+1 <= Set).

while it will type check, if one uses instead the coqtop -impredicative-set option..

The major change in the theory concerns the rule for product formation in the sort $\mathsf{\text{Set}}$, which is extended to a domain in any sort:

ProdImp

$$\frac{E[\Gamma ]⊢T:ss\in \mathcal{S}E[\Gamma ::(x:T)]⊢U:\mathsf{\text{Set}}}{E[\Gamma ]⊢\forall x:T,U:\mathsf{\text{Set}}}$$

This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called large inductive definitions like the example of second-order existential quantifier (exSet).

There should be restrictions on the eliminations which can be performed on such definitions. The elimination rules in the impredicative system for sort $\mathsf{\text{Set}}$ become:

Set1

$$\frac{s\in \{\mathsf{\text{Prop}},\mathsf{\text{Set}}\}}{[I:\mathsf{\text{Set}}|I\to s]}$$

Set2

$$\frac{I\mathsf{\text{is a small inductive definition}}s\in \{\mathsf{\text{Type}}(i)\}}{[I:\mathsf{\text{Set}}|I\to s]}$$