Correctness of Alpha-Equivalence

By induction on $s$, for all $t$, $E_1$, and $E_2$. For each shape of $s$, exactly one rule of Figure 11.1 can conclude the judgment, and its premises match the equations for $\db{\cdot}{}$.

If $s = \Sort{u}$, both sides hold exactly when $t = \Sort{u}$, by the rule $\alpha$-Sort and by the equation for universes.

If $s = x$, the nameless forms can be equal only if $t$ is a variable $y$, since a nameless variable (a number or a name) never equals a $\Pi$, a $\lambda$, an application, or a universe. If $x \in E_1$, then $\db{x}{E_1} = \#\mathrm{idx}(E_1, x)$, and equality holds exactly when $y \in E_2$ and $\mathrm{idx}(E_2, y) = \mathrm{idx}(E_1, x)$, which is the premise of $\alpha$-Bound. If $x \notin E_1$, then $\db{x}{E_1} = x$, and equality holds exactly when $y \notin E_2$ and $y = x$, which is the premise of $\alpha$-Free. A number never equals a name, matching the absence of a rule for a variable that is bound on one side only.

If $s = \tPi{x}{A}{B}$, equality holds exactly when $t = \tPi{y}{A'}{B'}$ with $\db{A}{E_1} = \db{A'}{E_2}$ and $\db{B}{E_1, x} = \db{B'}{E_2, y}$. By the induction hypothesis, applied to $A$ and to $B$, these two equations are exactly the premises of $\alpha$-Pi. The cases $\lambda$ and application are the same, using $\alpha$-Lam and $\alpha$-App.

By induction on $t$, for all $E_1$ and $E_2$. The variable case is exactly the assumption: a free variable $v$ becomes the same number, or stays the same name, on both sides. Universes are unaffected by $E$, and applications follow from the induction hypothesis for both parts.

Under a binder $x$, the lists $E_1, x$ and $E_2, x$ again agree on the free variables of the body. The variable $x$ has position $0$ in both. Any other free variable $v$ of the body is a free variable of $t$, so by assumption its position is the same in $E_1$ and $E_2$; appending $x$ increases that position by one on both sides, or leaves it undefined on both sides. The induction hypothesis for the body then applies, and the annotation is handled by the induction hypothesis with the original lists.

By induction on the size of $B$, for all $E$ and $E'$. Write $L_x = E, x, E'$ and $L_y = E, y, E'$; they differ in exactly one entry, at the same position.

If $B = x$, then $\subst{B}{x}{y} = y$. Since $x, y \notin E'$, the last occurrence of $x$ in $L_x$ and the last occurrence of $y$ in $L_y$ are both the distinguished entry, so $\mathrm{idx}(L_x, x)$ and $\mathrm{idx}(L_y, y)$ both equal the length of $E'$, and the nameless forms are the same number.

If $B = v$ with $v \neq x$, then $v \neq y$ because $y \notin \FV(B)$, and $\subst{B}{x}{y} = v$. The position of $v$ is the same in $L_x$ and $L_y$, since $v$ is neither of the entries that differ, or it is undefined in both.

Universes and applications are immediate from the definitions and the induction hypothesis.

Let $B = \tPi{w}{C}{D}$; the case of $\lambda$ is the same. The annotation $C$ is handled by the induction hypothesis in each case below, so we consider only the body. There are three cases, following the definition of substitution in Chapter 11.

Case $w = x$. The binder shadows $x$, so $\subst{B}{x}{y} = \tPi{x}{\subst{C}{x}{y}}{D}$, and we need $\db{D}{L_x, x} = \db{D}{L_y, x}$. We apply Lemma B.2. The variable $x$ has position $0$ in both lists, because it was just appended. Any other $v \in \FV(D)$ differs from $y$, since $y \notin \FV(B)$, so its position is the same in both lists, or undefined in both.

Case $w \notin \{x, y\}$. No renaming is needed, and $\subst{B}{x}{y} = \tPi{w}{\subst{C}{x}{y}}{\subst{D}{x}{y}}$. The induction hypothesis for $D$, with $E'$ extended by $w$ (which is allowed since $w$ is neither $x$ nor $y$), gives $\db{D}{L_x, w} = \db{\subst{D}{x}{y}}{L_y, w}$, which is what the body requires.

Case $w = y$. The binder would capture $y$, so substitution renames it to a fresh $z \notin \FV(D) \cup \{x, y\}$:

We need $\db{D}{L_x, y} = \db{\subst{(\subst{D}{y}{z})}{x}{y}}{L_y, z}$, and we get there in two steps. First, the induction hypothesis for $D$, renaming its last binder $y$ to $z$ (with $E$ taken as $L_x$ and $E'$ empty; the hypotheses hold because $z \neq y$, $z \notin \FV(D)$, and the list after the binder is empty), gives $\db{D}{L_x, y} = \db{\subst{D}{y}{z}}{L_x, z}$. Second, the induction hypothesis for $\subst{D}{y}{z}$, which has the size of $D$ and has no free $y$, with $E'$ extended by $z$, gives $\db{\subst{D}{y}{z}}{L_x, z} = \db{\subst{(\subst{D}{y}{z})}{x}{y}}{L_y, z}$. Chaining the two equations gives the claim.

First part. Let $s \sim t$ mean that $\db{s}{E} = \db{t}{E}$ for every $E$. This relation is an equivalence, since equality is. It is a congruence, because $\db{\cdot}{}$ is defined constructor by constructor: if the parts of two terms have equal nameless forms under the appropriate lists, so do the terms. Finally, $\sim$ contains the defining equation of $\alphaeq$: if $y \notin \FV(B)$, then

and the bodies are equal by Lemma B.3 with $E'$ empty; the case $y = x$ is trivial, since then the two terms are identical. The same holds for $\lambda$. Since $\alphaeq$ is the smallest congruence containing that equation, and $\sim$ is a congruence containing it, $s \alphaeq t$ implies $s \sim t$.

Second part. We use induction on the size of $s$, for all $t$ and $E$, assuming $\db{s}{E} = \db{t}{E}$.

If $s$ is a variable, so is $t$, since nameless forms of other shapes are never a number or a name. If both nameless forms are the number $\#i$, both variables are the entry at position $i$ of $E$, so $s = t$. If both are names, then $s = t$ directly. In either case $s \alphaeq t$ by reflexivity.

Universes are equal outright. For applications, the nameless forms of the two parts agree, so the induction hypothesis gives $\alphaeq$ for each part, and the congruence property of $\alphaeq$ gives it for the whole.

Let $s = \tPi{x}{A}{B}$, so that $t = \tPi{y}{A'}{B'}$ with $\db{A}{E} = \db{A'}{E}$ and $\db{B}{E, x} = \db{B'}{E, y}$. The induction hypothesis gives $A \alphaeq A'$. For the bodies, choose $z \notin \FV(B) \cup \FV(B') \cup \{x, y\}$. Lemma B.3 with $E'$ empty gives $\db{B}{E, x} = \db{\subst{B}{x}{z}}{E, z}$ and $\db{B'}{E, y} = \db{\subst{B'}{y}{z}}{E, z}$, so

Since $\subst{B}{x}{z}$ has the size of $B$, which is smaller than the size of $s$, the induction hypothesis gives $\subst{B}{x}{z} \alphaeq \subst{B'}{y}{z}$. Then

by the defining equation (valid since $z \notin \FV(B)$), by congruence, and by the defining equation read backwards (valid since $z \notin \FV(B')$). The case of $\lambda$ is the same.

If $s \alphaeq t$, then $\db{s}{\cdot} = \db{t}{\cdot}$ by the first part of Lemma B.4 (taking $E$ empty), and then $\cdot\,;\cdot \vdash s \alphaeq t$ by Lemma B.1.

Conversely, if $\cdot\,;\cdot \vdash s \alphaeq t$, then $\db{s}{\cdot} = \db{t}{\cdot}$ by Lemma B.1, and then $s \alphaeq t$ by the second part of Lemma B.4.