Exercise 3.19
Prove: if $Γ ⊢ L : σ$, then $Γ$ is a λ2-context.
Let's first remind ourselves of the definition 3.4.4 of a λ2-context.
(1) $∅$ is a λ2-context; $dom(∅) = ()$, the empty list.
(2) If $Γ$ is a λ2-context, $α ∈\mathbb{V}$ and $α \notin dom(Γ)$, then $Γ, α : ∗$ is a λ2-context; $dom(Γ,α : ∗) = (dom(Γ), α)$, i.e. $dom(Γ)$ concatenated with $α$.
(3) If $Γ$ is a λ2-context, if $ρ ∈ \mathbb{T}2$ such that $α ∈dom(Γ)$ for all free type variables $α$ occurring in $ρ$ and if $x \notin dom(Γ)$, then $Γ, x : ρ$ is a λ2-context; $dom(Γ,x : ρ) = (dom(Γ), x)$.
We'll use structural induction on $Γ$ to prove the statement.
Base Case
The base case is $Γ≡\emptyset$. The statement we need to prove for the base case is
$$ ( Γ ≡\emptyset ⊢ L : σ ) \implies Γ \text{ is a λ2 context}$$
The definition 3.4.4 (1) tells us the empty set $\emptyset$ is a λ2 context, so the base case is proven.
Induction Step
The induction hypothesis is as follows
$$ ( Γ^{\prime} ≡\emptyset ⊢ L : σ ) \implies Γ^{\prime} \text{ is a λ2 context}$$
We need to prove that for any $L$ constructed from $Γ^{\prime}$ using each of the two constructors of definition 3.4.4 (2) and (3), the following statement is true.
$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$
Let's consider each in turn.
Type Variable Constructor
Using definition 3.4.4 (2), if $Γ^{\prime}$ is a λ2-context, $α ∈\mathbb{V}$ and $α \notin dom(Γ^{\prime})$, then $Γ = Γ^{\prime}, α : ∗$ is a λ2-context.
The Thinning Lemma tells us that if $ Γ^{\prime} ⊢ L : σ$, then $Γ = Γ^{\prime}, α : ∗ ⊢ L : σ$.
So we have
$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$
Object Variable Constructor
Using definition 3.4.4 (3), if $Γ$ is a λ2-context, and if $ρ ∈ \mathbb{T}2$ such that $α ∈dom(Γ)$ for all free type variables $α$ occurring in $ρ$ and if $x \notin dom(Γ)$, then $Γ, x : ρ$ is a λ2-context.
The Thinning Lemma tells us that if $ Γ^{\prime} ⊢ L : σ$, then $Γ = Γ^{\prime}, x : ρ ⊢ L : σ$.
So again we have
$$ ( Γ ⊢ L : σ ) \implies Γ\text{ is a λ2 context}$$
Conclusion
We showed the statement
$$ ( Γ ≡\emptyset ⊢ L : σ ) \implies Γ \text{ is a λ2 context}$$
is true for the base case of $Γ≡\emptyset$, and also for $Γ$ constructed using any of the two constructors from the definition of a λ2 context.
So by structural induction, the statement is true in general.
