Exercise 2.15
Give the (var)- and (appl)-cases of the proof of Lemma 2.10.5(1) (the ‘Thinning Lemma’).
Let's remind ourselves of Lemma 2.10.5(1):
(1) (Thinning) Let $Γ^′$ and $Γ^{′′}$ be contexts such that $Γ^′ ⊆Γ^{′′}$. If $Γ^′ ⊢M : σ$, then also $Γ^{′′} ⊢M : σ$.
Quoting the textbook, to prove a general property $P$ for an arbitrary expression $E$ we can proceed by:
- assuming that $P$ holds for all expressions $E^{\prime}$ used to construct $E$ (the induction hypothesis),
- and then proving that $P$ also holds for $E$ itself.
Another simple explanation and illustration of structural induction is here (link).
(var)-case
The (var) rule applied to the precursor judgement
$$J_1 := Γ^′ ⊢ M : ρ$$
produces a new judgement
$$K _1:= Γ^′ ⊢ x : σ$$
if $x:σ \in Γ^′$.
For an induction hypothesis, we assume the Thinning Lemma holds for the precursor judgement $J_1$. That is,
$$J_1 := Γ^′ ⊢ M : ρ \quad \land \quad (Γ^′ \subseteq Γ^{′′}) \quad \implies \quad J_2 := Γ^{′′} ⊢ M : ρ $$
We need to show that the Thinning Lemma holds for the judgement $K_1$ as follows
$$K_1 := Γ^′ ⊢ x : σ \quad \land \quad (Γ^′ \subseteq Γ^{′′}) \quad \implies \quad K_2 := Γ^{′′} ⊢ x : σ $$
Since $x:σ \in Γ^′$ and $Γ^′ \subseteq Γ^{′′}$, it must be that $x:σ \in Γ^{′′}$. Therefore $Γ^{′′} ⊢ x : σ$, and so the judgement $K_2$ is true.
We have shown that if the Thinning Lemma holds for a judgement, it also holds for the judgement resulting from applying the (var) constructor to it, and therefore holds for all judgements produced by the (var) constructor.
(appl)-case
The (appl) rule applied to two precursor judgements
$$J_1 := Γ^′ ⊢ M : α→β \quad \text {and} \quad J_2 := Γ^′ ⊢ N : α $$
produces a new judgement
$$K _1:= Γ^′ ⊢ MN : β$$
For an induction hypothesis, we assume the Thinning Lemma holds for the two precursor judgements $J_1$ and $J_2$. That is,
$$J_1 := Γ^′ ⊢ M : α→β \quad \land \quad (Γ^′ \subseteq Γ^{′′}) \quad \implies \quad J_3 := Γ^{′′} ⊢ M : α→β $$
$$J_2 := Γ^′ ⊢ N : α \quad \land \quad (Γ^′ \subseteq Γ^{′′}) \quad \implies \quad J_4 := Γ^{′′} ⊢ N : α $$
We need to show that the Thinning Lemma holds for the judgement $K_1$ as follows
$$K _1:= Γ^′ ⊢ MN : β \quad \land \quad (Γ^′ \subseteq Γ^{′′}) \quad \implies \quad K_2 := Γ^{′′} ⊢ MN : β $$
Applying the (appl) rule to $J_3$ and $J_4$ gives us this desired judgement $K_2$.
We have shown that if the Thinning Lemma holds for two judgements, it also holds for the judgement that results from the (appl) rule applied to both of them, and therefore holds for all judgements resulting from the (appl) constructor.
