# 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 *Credits*.

## 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.

the sorts \(\SProp\), \(\Prop\), \(\Set\), \(\Type(i)\) are terms.

variables, hereafter ranged over by letters \(x\), \(y\), etc., are terms

constants, hereafter ranged over by letters \(c\), \(d\), etc., are terms.

if \(x\) is a variable and \(T\), \(U\) are terms then \(∀ x:T,~U\) (

`forall x:T, U`

in Coq concrete syntax) is a term. If \(x\) occurs in \(U\), \(∀ x:T,~U\) reads as “for all \(x\) of type \(T\), \(U\)”. As \(U\) depends on \(x\), one says that \(∀ x:T,~U\) is a*dependent product*. If \(x\) does not occur in \(U\) then \(∀ x:T,~U\) reads as “if \(T\) then \(U\)”. A*non dependent product*can be written: \(T \rightarrow U\).if \(x\) is a variable and \(T\), \(u\) are terms then \(λ 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 \(λ x:T .~u\) is a function which maps elements of \(T\) to the expression \(u\).if \(t\) and \(u\) are terms then \((t~u)\) is a term (

`t u`

in Coq concrete syntax). The term \((t~u)\) reads as “\(t\) applied to \(u\)”.if \(x\) is a variable, and \(t\), \(T\) and \(u\) are terms then \(\letin{x}{t:T}{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
\(λx:T.~U\) and \(∀ 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
\(\subst{u}{x}{t}\).

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

For instance, let us assume that \(\nat\) is the type of natural numbers
with zero element written \(0\) and that `True`

is the always true
proposition. Then \(→\) is used both to denote \(\nat→\nat\) which is the type
of functions from \(\nat\) to \(\nat\), to denote True→True which is an
implicative proposition, to denote \(\nat →\Prop\) which is the type of
unary predicates over the natural numbers, etc.

Let us assume that `mult`

is a function of type \(\nat→\nat→\nat\) and `eqnat`

a
predicate of type \(\nat→\nat→ \Prop\). The λ-abstraction can serve to build
“ordinary” functions as in \(λ x:\nat.~(\kw{mult}~x~x)\) (i.e.
`fun x:nat => mult x x`

in Coq notation) but may build also predicates over the natural
numbers. For instance \(λ x:\nat.~(\kw{eqnat}~x~0)\)
(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
\(\nat → \Prop\)
and it can be applied to any expression of type \(\nat\), say \(t\), to give an
object \(P~t\) of type \(\Prop\), namely a proposition.

Furthermore `forall x:nat, P x`

will represent the type of functions
which associate to each natural number \(n\) an object of type \((P~n)\) and
consequently represent the type of proofs of the formula “\(∀ 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 global environment and a local
context.

**Local context.**
A *local context* is an ordered list of *local declarations* of names
which we call *variables*. The declaration of some variable \(x\) is
either a *local assumption*, written \(x:T\) (\(T\) is a type) or a *local
definition*, written \(x:=t:T\). We use brackets to write local contexts.
A typical example is \([x:T;~y:=u:U;~z:V]\). Notice that the variables
declared in a local context must be distinct. If \(Γ\) is a local context
that declares some \(x\), we
write \(x ∈ Γ\). By writing \((x:T) ∈ Γ\) we mean that either \(x:T\) is an
assumption in \(Γ\) or that there exists some \(t\) such that \(x:=t:T\) is a
definition in \(Γ\). If \(Γ\) defines some \(x:=t:T\), we also write \((x:=t:T) ∈ Γ\).
For the rest of the chapter, \(Γ::(y:T)\) denotes the local context \(Γ\)
enriched with the local assumption \(y:T\). Similarly, \(Γ::(y:=t:T)\) denotes
the local context \(Γ\) enriched with the local definition \((y:=t:T)\). The
notation \([]\) denotes the empty local context. By \(Γ_1 ; Γ_2\) we mean
concatenation of the local context \(Γ_1\) and the local context \(Γ_2\).

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

A *global assumption* will be represented in the global environment as
\((c:T)\) which assumes the name \(c\) to be of some type \(T\). A *global
definition* will be represented in the global environment as \(c:=t:T\)
which defines the name \(c\) to have 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 global assumption \(c:T\).
Similarly, \(E;~c:=t:T\) denotes the global environment \(E\) enriched with the
global definition \((c:=t:T)\).

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

**Typing rules.**
In the following, we define simultaneously two judgments. The first
one \(\WTEG{t}{T}\) means the term \(t\) is well-typed and has type \(T\) in the
global environment \(E\) and local context \(Γ\). The second judgment \(\WFE{Γ}\)
means that the global environment \(E\) is well-formed and the local
context \(Γ\) 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 \(\Gamma\) and a term \(T\) such that the judgment \(\WTEG{t}{T}\) can be derived from the following rules.

- W-Empty
- \[\frac{% % }{% \WF{[]}{}% }\]

- W-Local-Assum
- \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:T)}% }\]

- W-Local-Def
- \[\frac{% \WTEG{t}{T}% \hspace{3em}% x \not\in \Gamma % \cup E% }{% \WFE{\Gamma::(x:=t:T)}% }\]

- W-Global-Assum
- \[\frac{% \WTE{}{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% c \notin E% }{% \WF{E;~c:T}{}% }\]

- W-Global-Def
- \[\frac{% \WTE{}{t}{T}% \hspace{3em}% c \notin E% }{% \WF{E;~c:=t:T}{}% }\]

- Ax-SProp
- \[\frac{% \WFE{\Gamma}% }{% \WTEG{\SProp}{\Type(1)}% }\]

- Ax-Prop
- \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Prop}{\Type(1)}% }\]

- Ax-Set
- \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Set}{\Type(1)}% }\]

- Ax-Type
- \[\frac{% \WFE{\Gamma}% }{% \WTEG{\Type(i)}{\Type(i+1)}% }\]

- Var
- \[\frac{% \WFE{\Gamma}% \hspace{3em}% (x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}% }{% \WTEG{x}{T}% }\]

- Const
- \[\frac{% \WFE{\Gamma}% \hspace{3em}% (c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$}% }{% \WTEG{c}{T}% }\]

- Prod-SProp
- \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in {\Sort}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\SProp}% }{% \WTEG{\forall~x:T,U}{\SProp}% }\]

- Prod-Prop
- \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \Sort% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Prop}% }{% \WTEG{∀ x:T,~U}{\Prop}% }\]

- Prod-Set
- \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \{\SProp, \Prop, \Set\}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Set}% }{% \WTEG{∀ x:T,~U}{\Set}% }\]

- Prod-Type
- \[\frac{% \WTEG{T}{s}% \hspace{3em}% s \in \{\SProp, \Type{i}\}% \hspace{3em}% \WTE{\Gamma::(x:T)}{U}{\Type(i)}% }{% \WTEG{∀ x:T,~U}{\Type(i)}% }\]

- Lam
- \[\frac{% \WTEG{∀ x:T,~U}{s}% \hspace{3em}% \WTE{\Gamma::(x:T)}{t}{U}% }{% \WTEG{λ x:T\mto t}{∀ x:T,~U}% }\]

- App
- \[\frac{% \WTEG{t}{∀ x:U,~T}% \hspace{3em}% \WTEG{u}{U}% }{% \WTEG{(t\ u)}{\subst{T}{x}{u}}% }\]

- Let
- \[\frac{% \WTEG{t}{T}% \hspace{3em}% \WTE{\Gamma::(x:=t:T)}{u}{U}% }{% \WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}% }\]

Note

**Prod-Prop** and **Prod-Set** typing-rules make sense if we consider the
semantic difference between \(\Prop\) and \(\Set\):

All values of a type that has a sort \(\Set\) are extractable.

No values of a type that has a sort \(\Prop\) are extractable.

Note

We may have \(\letin{x}{t:T}{u}\) well-typed without having \(((λ x:T.~u)~t)\) well-typed (where \(T\) is a type of \(t\)). This is because the value \(t\) associated to \(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:

if \(E[Γ] ⊢ t =_{βδιζη} u\) then \(E[Γ] ⊢ t ≤_{βδιζη} u\),

if \(i ≤ j\) then \(E[Γ] ⊢ \Type(i) ≤_{βδιζη} \Type(j)\),

for any \(i\), \(E[Γ] ⊢ \Set ≤_{βδιζη} \Type(i)\),

\(E[Γ] ⊢ \Prop ≤_{βδιζη} \Set\), hence, by transitivity, \(E[Γ] ⊢ \Prop ≤_{βδιζη} \Type(i)\), for any \(i\) (note: \(\SProp\) is not related by cumulativity to any other term)

if \(E[Γ] ⊢ T =_{βδιζη} U\) and \(E[Γ::(x:T)] ⊢ T' ≤_{βδιζη} U'\) then \(E[Γ] ⊢ ∀x:T,~T′ ≤_{βδιζη} ∀ x:U,~U′\).

if \(\ind{p}{Γ_I}{Γ_C}\) is a universe polymorphic and cumulative (see Chapter Polymorphic Universes) inductive type (see below) and \((t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I\) and \((t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I\) are two different instances of

*the same*inductive type (differing only in universe levels) with constructors\[[c_1 : ∀Γ_P ,∀ T_{1,1} … T_{1,n_1} ,~t~v_{1,1} … v_{1,m} ;~…;~ c_k : ∀Γ_P ,∀ T_{k,1} … T_{k,n_k} ,~t~v_{k,1} … v_{k,m} ]\]and

\[[c_1 : ∀Γ_P' ,∀ T_{1,1}' … T_{1,n_1}' ,~t'~v_{1,1}' … v_{1,m}' ;~…;~ c_k : ∀Γ_P' ,∀ T_{k,1}' … T_{k,n_k}' ,~t'~v_{k,1}' … v_{k,m}' ]\]respectively then

\[E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m'\](notice that \(t\) and \(t'\) are both fully applied, i.e., they have a sort as a type) if

\[E[Γ] ⊢ w_i =_{βδιζη} w_i'\]for \(1 ≤ i ≤ m\) and we have

\[E[Γ] ⊢ T_{i,j} ≤_{βδιζη} T_{i,j}'\]and

\[E[Γ] ⊢ A_i ≤_{βδιζη} A_i'\]where \(Γ_{\mathit{Arr}(t)} = [a_1 : A_1 ;~ … ;~a_l : A_l ]\) and \(Γ_{\mathit{Arr}(t)}' = [a_1 : A_1';~ … ;~a_l : A_l']\).

The conversion rule up to subtyping is now exactly:

- Conv
- \[\frac{% E[Γ] ⊢ U : s% \hspace{3em}% E[Γ] ⊢ t : T% \hspace{3em}% E[Γ] ⊢ T ≤_{βδιζη} U% }{% E[Γ] ⊢ 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
\(λ x_1 :T_1 .~… λ x_k :T_k .~(t_0~t_1 … 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 \(λ x:T.~u_0\) then one step of β-head reduction of \(t\) is:

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\):

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.

## Admissible rules for global environments¶

From the original rules of the type system, one can show the admissibility of rules which change the local context of definition of objects in the global environment. We show here the admissible rules that are used in the discharge mechanism at the end of a section.

**Abstraction.**
One can modify a global declaration by generalizing it over a
previously assumed constant \(c\). For doing that, we need to modify the
reference to the global declaration in the subsequent global
environment and local context by explicitly applying this constant to
the constant \(c\).

Below, if \(Γ\) is a context of the form \([y_1 :A_1 ;~…;~y_n :A_n]\), we write \(∀x:U,~\subst{Γ}{c}{x}\) to mean \([y_1 :∀ x:U,~\subst{A_1}{c}{x};~…;~y_n :∀ x:U,~\subst{A_n}{c}{x}]\) and \(\subst{E}{|Γ|}{|Γ|c}\) to mean the parallel substitution \(E\{y_1 /(y_1~c)\}…\{y_n/(y_n~c)\}\).

**First abstracting property:**

One can similarly modify a global declaration by generalizing it over a previously defined constant \(c\). Below, if \(Γ\) is a context of the form \([y_1 :A_1 ;~…;~y_n :A_n]\), we write \(\subst{Γ}{c}{u}\) to mean \([y_1 :\subst{A_1} {c}{u};~…;~y_n:\subst{A_n} {c}{u}]\).

**Second abstracting property:**

**Pruning the local context.**
If one abstracts or substitutes constants with the above rules then it
may happen that some declared or defined constant does not occur any
more in the subsequent global environment and in the local context.
One can consequently derive the following property.

- First pruning property:
- \[\frac{% \WF{E;~c:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]

- Second pruning property:
- \[\frac{% \WF{E;~c:=u:U;~E′}{Γ}% \hspace{3em}% c~\kw{does not occur in}~E′~\kw{and}~Γ% }{% \WF{E;E′}{Γ}% }\]

## 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 \(\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 \(\Set\), which is extended to a domain in any sort:

- ProdImp
- \[\frac{% E[Γ] ⊢ T : s% \hspace{3em}% s ∈ \Sort% \hspace{3em}% E[Γ::(x:T)] ⊢ U : \Set% }{% E[Γ] ⊢ ∀ x:T,~U : \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 \(\Set\) become:

- Set1
- \[\frac{% s ∈ \{\Prop, \Set\}% }{% [I:\Set|I→ s]% }\]

- Set2
- \[\frac{% I~\kw{is a small inductive definition}% \hspace{3em}% s ∈ \{\Type(i)\}% }{% [I:\Set|I→ s]% }\]