Proving preservation under substitution System F Omega

Question

I am going over the proofs for the simply typed lambda calculus in the book "Types and Programming languages" by Benjamin Pierce. I am trying to find inspiration for the similar proofs for System F Omega. When I was going over the preservation under substitution proof for the simply typed lambda calculus I was a bit puzzled.

The hypothesis of the proof is:

If $\Gamma ,x:S \vdash t:T $ and $\Gamma \vdash s:S$ then $\Gamma \vdash [x \mapsto s]t : T$

So far I understand the proof quite well, but for the case $T-Abs$ I'm a bit lost. The rule is shown below.

$$ \dfrac{\Gamma ,x:T_1 \vdash t_2 : T_2} {\Gamma \vdash \lambda x:T_1 . t_2 : T_1 \rightarrow T_2} $$

To prove the hypothesis for this case we use the previously proven lemmas weakening and permutation.

We assume that in this proof $x \neq y$ and $y \notin FV(s)$.

First we list the givens:

1. $t = \lambda y:T_2 . t_1$
2. $ T = T_1 \rightarrow T_2$
3. The first subderivation: $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$
4. The second subderivation: $\Gamma \vdash s:S$ by hypothesis.

Step 1 The first step we take is using permutation on the first sub-derivation, yielding: $\Gamma ,y:T_2,x:S \vdash t_1 : T_2$. The reason why this happens is a bit unclear to me. I am assuming that the actual order of the extensions of $\Gamma$ matter for the third step.

Step 2 The second step, which is the one that is unclear to me, is applying weakening to the second sub-derivation: changing $\Gamma \vdash s:S$ into $\Gamma ,y:T_2\vdash s:S$. The reason that I find this odd is that this new form of the sub-derivation is not used anywhere in the proof.

Step 3: By the induction of our hypothesis we know that $\Gamma ,x:S,y:T_2 \vdash t_1 : T_2$ implies $\Gamma ,y:T_2 \vdash [x \mapsto s]t_1 : T_2$. And since we know that, we can apply the $T-Abs$ rule. Since that is what it basically says. We wrap the given sub-derivation in a lambda and we have to remove the $y:T_2$ from the context because it is now introduced by the abstraction we constructed:

$$\Gamma \vdash \lambda y:T_2 . [x \mapsto s]t_1 : T_1 \rightarrow T_2$$

And finally we can move the substitution outside because we assumed that $x \neq y$ and $y \notin FV(s)$.

$$\Gamma \vdash [x \mapsto s]\lambda y:T_2 . t_1 : T_1 \rightarrow T_2$$

And this is exactly what we had to prove.

The problem I have with the second sub-derivation is that we nowhere in the prove actually used it. We never relied on that fact. Any input would be highly appreciated.

Answer 1

Throughout $y$ should have type $T_1$ instead of $T_2$.

Let us be more careful about step 3. We are going to apply the following induction hypothesis:

If $\Gamma, y : T_1, x : S \vdash t_1 : T_2$ and $\Gamma, y : T_1 \vdash s : S$ then $\Gamma, y : T_1 \vdash [x \mapsto s] t_1 : T_2$.

After that we will use abstraction to get $\Gamma \vdash (\lambda y : T_1 . [x \mapsto s] t_1) : T_2$, and finish the proof by observing that $(\lambda y : T_1 . [x \mapsto s] t_1) = [x \mapsto s](\lambda y : T_1 . t_1)$.

So let us make sure that the induction hypothesis is applicable:

1. First we need $\Gamma, y : T_1, x : S \vdash t_1 : T_2$: because $\Gamma, x : S \vdash (\lambda y : T_1 . t_1) : T_1 \to T_2$ by inversion we obtain $\Gamma, x : S, y : T_1 \vdash t_1 : T_2$ and then we use exchange to get $\Gamma, y : T_1, x : S \vdash t_1 : T_2$. This is your step 1. (The exchange is valid because types are non-dependent in this argument.)

2. Second, we need $\Gamma, y : T_1 \vdash s : S$: we already have $\Gamma \vdash s : S$. By weakening we obtain $\Gamma, y : T_1 \vdash s : S$, this is your step 2.

Supplemental: It seems unclear how induction works. To perform a proof by induction we need to specify what the induction is on. In this case the induction is on the derivation of $\Gamma, x : S \vdash t : T$. Thus, we have to look at all the possible cases of deriving $\Gamma, x : S \vdash t : T$. Each inference rule gives us one case, and we've just discussed the case of $\lambda$-abstraction. Each case has its own induction hypotheses, one for each premise of the rule.

Let me give you a simpler example. Suppose we only had the following typing rules:

1. Variables: $$\frac{(x : T) \in \Gamma}{\Gamma \vdash x : T}$$
2. Pairs: $$\frac{\Gamma \vdash e_1 : T_1 \qquad \Gamma \vdash e_2 : T_2}{\Gamma \vdash (e_1, e_2) : T_1 \times T_2}$$
3. First projection: $$\frac{\Gamma \vdash e : T_1 \times T_2}{\Gamma \vdash \mathsf{fst}\,e : T_1}$$

A derivation is a finite tree built from these rules (if you are not clear about that, you should first understand what a derivation is). Suppose we want to show that every derivable judgement has some given property $\phi$. To prove this by induction on the derivation, we need to show three things:

1. Variable case: if $(x : T) \in \Gamma$ then $\Gamma \vdash x : T$ has property $\phi$.

2. Pair case: if $\Gamma \vdash e_1 : T_1$ has property $\phi$ and $\Gamma \vdash e_2 : T_2$ has property $\phi$ then $\Gamma \vdash (e_1, e_2) : T_1 \times T_2$ has property $\phi$.

3. First projection case: if $\Gamma \vdash e : T_1 \times T_2$ has property $\phi$ then $\Gamma \vdash \mathsf{fst}\, e : T_1$ has property $\phi$.

The first case has no induction hypothesis, it is a base case. This is so because the corresponding inference rule has no premises (only the side condition $(x : T) \in \Gamma$). The second case has two induction hypotheses, namely that $\Gamma \vdash e_1 : T_1$ has property $\phi$ and that $\Gamma \vdash e_2 : T_2$ has property $\phi$. This is so because the corresponding inference rules has these two premises. The third case has one induction hypothesis, and you should be able to see why that is if you understood what I am saying.