\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} \newcommand{\emptyf}{\textsf{emptyf}} \newcommand{\End}{\kw{End}} \newcommand{\kwend}{\kw{end}} \newcommand{\even}{\textsf{even}} \newcommand{\evenO}{\textsf{even}_\textsf{O}} \newcommand{\evenS}{\textsf{even}_\textsf{S}} \newcommand{\Fix}{\kw{Fix}} \newcommand{\fix}{\kw{fix}} \newcommand{\for}{\textsf{for}} \newcommand{\forest}{\textsf{forest}} \newcommand{\Functor}{\kw{Functor}} \newcommand{\In}{\kw{in}} \newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} \newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} \newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} \newcommand{\injective}{\kw{injective}} \newcommand{\kw}[1]{\textsf{#1}} \newcommand{\length}{\textsf{length}} \newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} \newcommand{\List}{\textsf{list}} \newcommand{\lra}{\longrightarrow} \newcommand{\Match}{\kw{match}} \newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} \newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} \newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} \newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} \newcommand{\mto}{.\;} \newcommand{\nat}{\textsf{nat}} \newcommand{\Nil}{\textsf{nil}} \newcommand{\nilhl}{\textsf{nil\_hl}} \newcommand{\nO}{\textsf{O}} \newcommand{\node}{\textsf{node}} \newcommand{\nS}{\textsf{S}} \newcommand{\odd}{\textsf{odd}} \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} \newcommand{\plus}{\mathsf{plus}} \newcommand{\SProp}{\textsf{SProp}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} \newcommand{\Set}{\textsf{Set}} \newcommand{\Sort}{\mathcal{S}} \newcommand{\Str}{\textsf{Stream}} \newcommand{\Struct}{\kw{Struct}} \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} \newcommand{\trii}{\triangleright_\iota} \newcommand{\Type}{\textsf{Type}} \newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} \newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} \newcommand{\WF}[2]{{\mathcal{W\!F}}(#1)[#2]} \newcommand{\WFE}[1]{\WF{E}{#1}} \newcommand{\WFT}[2]{#1[] \vdash {\mathcal{W\!F}}(#2)} \newcommand{\WFTWOLINES}[2]{{\mathcal{W\!F}}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} \newcommand{\with}{\kw{with}} \newcommand{\WS}[3]{#1[] \vdash #2 <: #3} \newcommand{\WSE}[2]{\WS{E}{#1}{#2}} \newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} \newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} \newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} \newcommand{\zeroone}[1]{[{#1}]} \end{split}\]

Conversion rules

In CIC, there is an internal reduction mechanism. In particular, it can decide if two programs are intentionally equal (one says convertible). Convertibility is described in this section.

β-reduction

We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For instance the identity function over a given type \(T\) can be written \(λx:T.~x\). In any global environment \(E\) and local context \(Γ\), we want to identify any object \(a\) (of type \(T\)) with the application \(((λ x:T.~x)~a)\). We define for this a reduction (or a conversion) rule we call \(β\):

\[E[Γ] ⊢ ((λx:T.~t)~u)~\triangleright_β~\subst{t}{x}{u}\]

We say that \(\subst{t}{x}{u}\) is the β-contraction of \(((λx:T.~t)~u)\) and, conversely, that \(((λ x:T.~t)~u)\) is the β-expansion of \(\subst{t}{x}{u}\).

According to β-reduction, terms of the Calculus of Inductive Constructions enjoy some fundamental properties such as confluence, strong normalization, subject reduction. These results are theoretically of great importance but we will not detail them here and refer the interested reader to [Coq85].

ι-reduction

A specific conversion rule is associated to the inductive objects in the global environment. We shall give later on (see Section Well-formed inductive definitions) the precise rules but it just says that a destructor applied to an object built from a constructor behaves as expected. This reduction is called ι-reduction and is more precisely studied in [PM93a][Wer94].

δ-reduction

We may have variables defined in local contexts or constants defined in the global environment. It is legal to identify such a reference with its value, that is to expand (or unfold) it into its value. This reduction is called δ-reduction and shows as follows.

Delta-Local
\[\frac{% \WFE{\Gamma}% \hspace{3em}% (x:=t:T) ∈ Γ% }{% E[Γ] ⊢ x~\triangleright_Δ~t% }\]
Delta-Global
\[\frac{% \WFE{\Gamma}% \hspace{3em}% (c:=t:T) ∈ E% }{% E[Γ] ⊢ c~\triangleright_δ~t% }\]

ζ-reduction

Coq allows also to remove local definitions occurring in terms by replacing the defined variable by its value. The declaration being destroyed, this reduction differs from δ-reduction. It is called ζ-reduction and shows as follows.

Zeta
\[\frac{% \WFE{\Gamma}% \hspace{3em}% \WTEG{u}{U}% \hspace{3em}% \WTE{\Gamma::(x:=u:U)}{t}{T}% }{% E[Γ] ⊢ \letin{x}{u:U}{t}~\triangleright_ζ~\subst{t}{x}{u}% }\]

η-expansion

Another important concept is η-expansion. It is legal to identify any term \(t\) of functional type \(∀ x:T,~U\) with its so-called η-expansion

\[λx:T.~(t~x)\]

for \(x\) an arbitrary variable name fresh in \(t\).

Note

We deliberately do not define η-reduction:

\[λ x:T.~(t~x)~\not\triangleright_η~t\]

This is because, in general, the type of \(t\) need not to be convertible to the type of \(λ x:T.~(t~x)\). E.g., if we take \(f\) such that:

\[f ~:~ ∀ x:\Type(2),~\Type(1)\]

then

\[λ x:\Type(1).~(f~x) ~:~ ∀ x:\Type(1),~\Type(1)\]

We could not allow

\[λ x:\Type(1).~(f~x) ~\triangleright_η~ f\]

because the type of the reduced term \(∀ x:\Type(2),~\Type(1)\) would not be convertible to the type of the original term \(∀ x:\Type(1),~\Type(1)\).

Proof Irrelevance

It is legal to identify any two terms whose common type is a strict proposition \(A : \SProp\). Terms in a strict propositions are therefore called irrelevant.

Convertibility

Let us write \(E[Γ] ⊢ t \triangleright u\) for the contextual closure of the relation \(t\) reduces to \(u\) in the global environment \(E\) and local context \(Γ\) with one of the previous reductions β, δ, ι or ζ.

We say that two terms \(t_1\) and \(t_2\) are βδιζη-convertible, or simply convertible, or equivalent, in the global environment \(E\) and local context \(Γ\) iff there exist terms \(u_1\) and \(u_2\) such that \(E[Γ] ⊢ t_1 \triangleright … \triangleright u_1\) and \(E[Γ] ⊢ t_2 \triangleright … \triangleright u_2\) and either \(u_1\) and \(u_2\) are identical up to irrelevant subterms, or they are convertible up to η-expansion, i.e. \(u_1\) is \(λ x:T.~u_1'\) and \(u_2 x\) is recursively convertible to \(u_1'\), or, symmetrically, \(u_2\) is \(λx:T.~u_2'\) and \(u_1 x\) is recursively convertible to \(u_2'\). We then write \(E[Γ] ⊢ t_1 =_{βδιζη} t_2\).

Apart from this we consider two instances of polymorphic and cumulative (see Chapter Polymorphic Universes) inductive types (see below) convertible

\[E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'\]

if we have subtypings (see below) in both directions, i.e.,

\[E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m'\]

and

\[E[Γ] ⊢ t~w_1' … w_m' ≤_{βδιζη} t~w_1 … w_m.\]

Furthermore, we consider

\[E[Γ] ⊢ c~v_1 … v_m =_{βδιζη} c'~v_1' … v_m'\]

convertible if

\[E[Γ] ⊢ v_i =_{βδιζη} v_i'\]

and we have that \(c\) and \(c'\) are the same constructors of different instances of the same inductive types (differing only in universe levels) such that

\[E[Γ] ⊢ c~v_1 … v_m : t~w_1 … w_m\]

and

\[E[Γ] ⊢ c'~v_1' … v_m' : t'~ w_1' … w_m '\]

and we have

\[E[Γ] ⊢ t~w_1 … w_m =_{βδιζη} t~w_1' … w_m'.\]

The convertibility relation allows introducing a new typing rule which says that two convertible well-formed types have the same inhabitants.