Substitution lemma for types

Question

TAPL (page 549) proposes the following lemma in order to prove soundness of System F type system:

Substitution lemma for types:

$E, X, \Delta \vdash t: T \implies E, [X \mapsto S] \Delta \vdash [X \mapsto S]t: [X \mapsto S]T$

Proof of the T-TApp case:

$ E,X,\Delta \vdash t[A]: [Y \mapsto A]T $

and by rule T-TApp we have:

$ E,X,\Delta \vdash t: \lambda Y . T $

so by induction hypothesis:

$E, [X \mapsto S] \Delta \vdash [X \mapsto S]t: \lambda Y. [X \mapsto S]T$

so applying the T-TApp rule we have:

$E, [X \mapsto S] \Delta \vdash [X \mapsto S]t[A]: [Y \mapsto A][X \mapsto S]T$

however I should need $[Y \mapsto A][X \mapsto S]T = [X \mapsto S][Y \mapsto A]T$

I think I can assume that $A,S$ cannot contain $Y$.

However, what if $A$ contains $X$? Then these types do not coincide.

Assume $T$ contains $Y$. Then the lhs type leaves $X$'s in the result while the rhs type does not leave any.

Other sources

You can find an sketched proof in the proof of lemma 17, page 86 of the following lecture notes. But this case appears to be immediate.

Answer 1

The substitution lemma only holds if what you're substituting is well-formed: $S$ can only contain type variables listed in $E$. In the application of T-TApp, $Y$ is a fresh variable, not present in $E,X,\Delta$. In particular, $Y \ne X$, $Y \notin S$ and $Y \notin A$.

There several ways to model variable names and renaming.

• Shadowing allows a binder inside another binder to use the same name (e.g. $\lambda x. \lambda x. M$), and then the outer name is hidden (shadowed) in the inner construct (any occurence of $x$ in $M$ refers to the inner $x$). If you want to refer to the outer variable (which can happen to perform a beta reduction, for example), you need to first perform an explicit alpha conversion to rename one of the variables.
• Implicit renaming always uses distinct names for any two binders present anywhere in an expression (so you never write $\color{red}{\lambda x. \lambda x. M}$ or even $\color{red}{(\lambda x. M) (\lambda x. M)}$, but $\lambda y. \lambda x. M$ and $(\lambda x.M) (\lambda y.[x \mapsto y]M)$), and there is an implicit alpha conversion after any reduction that duplicates a term. This is called the Barendregt convention.
• Most literature claims to use the Barendregt convention, but in fact uses an intermediate convention where there nested binders never use the same name, but binders that don't overlap each other can use the same name, and there is an implicit alpha conversion step immediately after shadowing occurs. So for example $(\lambda x.M) (\lambda x.M)$ is allowed in writing, but the meta-notation $x$ in the two subterms are supposed to represent two different variables. As far as I remember, TAPL uses this convention.

An environment is a collection of binders, so without shadowing, it cannot define the same variable name more than once (no $\Gamma_1,X,\Gamma_2,X,\Gamma_3$).

Now, let's look at the application of T-TApp. The premise is $\Gamma' \vdash t' : \forall Y. T'$ where $\Gamma' = (E, [X \mapsto S] \Delta)$, $t' = [X \mapsto S] t$ and $T' = [X \mapsto S] T$. From this premise, you can conclude $$\Gamma' \vdash \lambda t'[A'] : [Y \mapsto A'] T'$$ for any well-formed $A'$. You want to prove $\Gamma' \vdash [X \mapsto S] (t[A]) : [X \mapsto S] [Y \mapsto A] T$. So take $A' = [X \mapsto S] A$. The conclusion is $$\Gamma' \vdash ([X \mapsto S] t)[[X \mapsto S] A] : [Y \mapsto [X \mapsto S] A] [X \mapsto S] T$$ and this is indeed $$\Gamma' \vdash [X \mapsto S] (t[A]) : [X \mapsto S] [Y \mapsto A] T$$ since $Y \ne X$ and $Y \notin S$.