Exercise 2.16
Prove Lemma 2.10.8 (the ‘Subterm Lemma’).
Let's remind ourselves of Lemma 2.10.8, the Subterm Lemma.
If M is legal, then every sub-term of M is legal.
Definition 1.3.5 defines sub-terms of λ-terms.
(1) (Basis) $Sub(x) = {x}$, for each $x ∈V$.
(2) (Application) $Sub((MN)) = Sub(M)∪Sub(N)∪{(MN)}$.
(3) (Abstraction) $Sub((λx. M)) = Sub(M)∪{(λx. M)}$.
We start by noting that all λ-terms are at the top level one of three forms, a variable, an application, or an abstraction. We can therefore use the (var), (appl) and (abst) construction rules in a structural induction proof.
(var)-rule
We'll consider a precursor judgement $Γ⊢M:α$ from which the (var) rule results in $Γ⊢x:β$ where $x:β \in Γ$.
Our aim is show that if $x$ is legal, then every sub-term of $x$ is legal.
This is trivially true.
Note that we didn't need to use an induction hypothesis.
(appl)-rule
We'll consider two precursors $Γ⊢A;α→β$, and $Γ⊢B:α$. Here $A$ and $B$ are legal terms, a premise for the (appl) rule which gives us $Γ⊢AB:β$.
As an induction hypothesis we'll assume that if $A$ and $B$ are legal, then both their sub-terms are legal.
Our aim is to show that if $AB$ is legal, then every sub-term of $AB$ is legal.
Definition 1.3.5 tells us the sub-terms of $AB$ are $AB$ itself, and the sub-terms of $A$ and $B$. We have $AB$ is legal by assumption. The remain options $A$ and $B$ have legal sub-terms by the induction hypothesis.
(abst)-rule
We'll consider the precursor $Γ, x:α⊢M:β$. Here $M$ is a legal term, a premise for the (abst) rule which gives us $Γ⊢λx.M:α→β$.
As an induction hypotheses we'll assume that if $M$ is legal, then every sub-term of $M$ is legal.
Our aim is to show that if $λx.M$ is legal, then every sub-term of $λx.M$ is legal.
Definition 1.3.5 tells us the sub-terms of $λx.M$ is $λx.M$ itself, and the sub-terms of $M$. The term $λx.M$ is legal by assumption. The induction hypothesis tells us $M$ is legal and so are its sub-terms.
We've shown that if a λ-term is legal, then all its sub-terms are legal, but showing this is true for all three modes of constructing that λ-term.
