\[\begin{split}\newcommand{\as}{\kw{as}} \newcommand{\case}{\kw{case}} \newcommand{\cons}{\textsf{cons}} \newcommand{\consf}{\textsf{consf}} \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}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} \newcommand{\Indp}[4]{\kw{Ind}_{#4}[#1](#2:=#3)} \newcommand{\Indpstr}[5]{\kw{Ind}_{#4}[#1](#2:=#3)/{#5}} \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{\ModImp}[3]{{\kw{Mod}}({#1}:{#2}:={#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

The Rocq Prover has conversion rules that can be used to determine if two terms are equal by definition in CIC, or convertible. Conversion rules consist of reduction rules and expansion rules. Equality is determined by converting both terms to a normal form, then verifying they are syntactically equal (ignoring differences in the names of bound variables by alpha-conversion).

See also

Applying conversion rules, which describes tactics that apply these conversion rules.

Reductions convert terms to something that is incrementally closer to its normal form. For example, zeta-reduction removes `let ident := term1 in term2` constructs from a term by replacing `ident` with `term1` wherever `ident` appears in `term2`. The resulting term may be longer or shorter than the original.

Eval cbv zeta in let i := 1 in i + i.
  = 1 + 1 : nat

Expansions are reductions applied in the opposite direction, for example expanding `2 + 2` to `let i := 2 in i + i`. While applying reductions gives a unique result, the associated expansion may not be unique. For example, `2 + 2` could also be expanded to `let i := 2 in i + 2`. Reductions that have a unique inverse expansion are also referred to as contractions.

The normal form is defined as the result of applying a particular set of conversion rules (beta-, delta-, iota- and zeta-reduction and eta-expansion) repeatedly until it's no longer possible to apply any of them.

Sometimes the result of a reduction tactic will be a simple value, for example reducing `2*3+4` with `cbv beta delta iota` to `10`, which requires applying several reduction rules repeatedly. In other cases, it may yield an expression containing variables, axioms or opaque contants that can't be reduced.

The useful conversion rules are shown below. All of them except for eta-expansion can be applied with conversion tactics such as `cbv`:

> Conversion name | Description
> --- | ---
> beta-reduction | eliminates `fun`
> delta-reduction | replaces a defined variable or constant with its definition
> zeta-reduction | eliminates `let`
> eta-expansion | replaces a term `f` of type `forall a : A, B` with `fun x : A => f x`
> match-reduction | eliminates `match`
> fix-reduction | replaces a `fix` with a beta-redex; recursive calls to the symbol are replaced with the `fix` term
> cofix-reduction | replaces a `cofix` with a beta-redex; recursive calls to the symbol are replaced with the `cofix` term
> iota-reduction | match-, fix- and cofix-reduction together

Applying conversion rules describes tactics that only apply conversion rules. (Other tactics may use conversion rules in addition to other changes to the proof state.)

## α-conversion

Two terms are α-convertible if they are syntactically equal ignoring differences in the names of variables bound within the expression. For example `forall x, x + 0 = x` is α-convertible with `forall y, y + 0 = y`. (Internally, Rocq represents these two terms using de Bruijn indices, so explicit α-conversion is not necessary.)

## β-reduction

β-reduction reduces a beta-redex, which is a term in the form `(fun x => t) u`. (Beta-redex is short for "beta-reducible expression", a term from lambda calculus. See Beta reduction for more background.)

Formally, in any global environment \(E\) and local context \(Γ\), the beta-reduction rule is:

Beta
  \[\frac{% % }{% 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}\).

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

δ-reduction replaces variables defined in local contexts or constants defined in the global environment with their values. Unfolding means to replace a constant by its definition. Formally, this is:

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% }\]

Delta-reduction unfolds constants when permitted by their opaqueness settings.

## ι-reduction

A specific conversion rule is associated with 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

ζ-reduction removes let-in definitions in terms by replacing the defined variable by its value. One way this reduction differs from δ-reduction is that the declaration is removed from the term entirely. Formally, this is:

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

## Examples

> Example: Simple delta, fix, beta and match reductions

> `+` is a notation for `Nat.add`, which is defined with a `Fixpoint`.

> Print Nat.add.
>   Nat.add = fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (add p m) end : nat -> nat -> nat Arguments Nat.add (n m)%_nat_scope
> Goal 1 + 1 = 2.
>   1 goal ============================ 1 + 1 = 2
> cbv delta.
>   1 goal ============================ (fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (add p m) end) 1 1 = 2
> cbv fix.
>   1 goal ============================ (fun n m : nat => match n with | 0 => m | S p => S ((fix add (n0 m0 : nat) {struct n0} : nat := match n0 with | 0 => m0 | S p0 => S (add p0 m0) end) p m) end) 1 1 = 2
> cbv beta.
>   1 goal ============================ match 1 with | 0 => 1 | S p => S ((fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p0 => S (add p0 m) end) p 1) end = 2
> cbv match.
>   1 goal ============================ S ((fix add (n m : nat) {struct n} : nat := match n with | 0 => m | S p => S (add p m) end) 0 1) = 2

> The term can be fully reduced with `cbv`:

> Goal 1 + 1 = 2.
>   1 goal ============================ 1 + 1 = 2
> cbv.
>   1 goal ============================ 2 = 2

## 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 definitionally equal, 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.

Other versions v: 9.2

Versions
  dev
  stable
  9.2
  9.1
  9.0
  8.20
  8.19
  8.18
  8.17
  8.16
  8.15
  8.14
  8.13
  8.12
  8.11
  8.10
  8.9
  8.8
  8.7
  8.6
  8.5
  8.4
  8.3
  8.2
  8.1
  8.0

Downloads
  PDF