Exercise 2.18
Prove the Compatibility cases in the proof of Lemma 2.11.5.
Lemma 2.11.5 (Subject Reduction) is
If $Γ ⊢L : ρ$ and if $L \to _{β} L^′$, then $Γ ⊢L^′ : ρ$.
The proof of Lemma 2.11.5 is done by induction on the generation of $L \to_β L^′$. That is, all modes of constructing $L \to_β L^′$ are considered, and for each, we show that indeed, given $Γ ⊢L : ρ$ each mode of generating $L \to _{β} L^′$ leads to $Γ ⊢L^′ : ρ$.
There are four modes of generating $L \to_β L^′$, as follows.
(1) Basis. $(λx : σ. M)N →_β M[x := N]$
(2) Compatibility. If $M →_β N$, then $MK →_β NK$
(3) Compatibility. If $M →_β N$, then $KM →_β KN$
(4) Compatibility. If $M →_β N$, then $λx. M →_β λx. N$
The textbook provides a proof for the (1) basis case. We'll provide the proofs for the compatibility cases (2-4).
(2) (Compatibility) If $M →_β N,$ then $MK →_β NK$
In this case $L ≡MK$ and $L^′ ≡NK$.
So, we aim to show that if $Γ ⊢MK : ρ$ and if $MK \to _{β} NK$, then $Γ ⊢NK: ρ$.
We assume:
- the precursor is true, $M →_β N$, and
- induction hypothesis: if $Γ ⊢M : α$ and if $M \to _{β} N$, then $Γ ⊢N : α$
We start with
$$Γ ⊢ MK : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ ⊢ M :γ→ ρ \quad \land \quad Γ ⊢K : γ$$
The induction hypothesis tells us
$$Γ⊢N: γ→ρ$$
And so, finally,
$$Γ⊢NK:ρ$$
So we have shown that if $Γ ⊢MK : ρ$ and if $MK \to _{β} NK$, then $Γ ⊢NK: ρ$.
(3) (Compatibility) If $M →_β N,$ then $KM →_β KN$
In this case $L ≡KM$ and $L^′ ≡KN$.
So, we aim to show that if $Γ ⊢KM : ρ$ and if $KM \to _{β} KN$, then $Γ ⊢KN: ρ$.
We assume:
- the precursor is true, $M →_β N$, and
- induction hypothesis: if $Γ ⊢M : α$ and if $M \to _{β} N$, then $Γ ⊢N : α$
We start with
$$Γ ⊢ KM : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ ⊢ K :γ→ ρ \quad \land \quad Γ ⊢M : γ$$
The induction hypothesis tells us
$$Γ⊢N: γ$$
And so, finally,
$$Γ⊢KN:ρ$$
So we have shown that if $Γ ⊢KM : ρ$ and if $KM \to _{β} KN$, then $Γ ⊢KN: ρ$.
(4) Compatibility. If $M →_β N$, then $λx. M →_β λx. N$
In this case $L ≡λx. M$ and $L^′ ≡λx. N$.
So, we aim to show that if $Γ ⊢λx. M : ρ$ and if $λx. M \to _{β} λx. N$, then $Γ ⊢λx. N: ρ$.
We assume:
- the precursor is true, $M →_β N$, and
- induction hypothesis: if $Γ ⊢M : α$ and if $M \to _{β} N$, then $Γ ⊢N : α$
We start with
$$Γ ⊢λx. M : ρ$$
Then by the Generation Lemma 2.10.7, we must have
$$ Γ, x:α ⊢ M :β \quad \land \quad ρ \equiv α→β$$
The induction hypothesis tells us
$$Γ, x:α ⊢N: β$$
And so, finally,
$$Γ ⊢λx. N : ρ$$
So we have shown that if $Γ ⊢λx. M : ρ$ and if $λx. M \to _{β} λx. N$, then $Γ ⊢λx. N: ρ$.
