Proof of Subject-Expansion Theorem in Type Theory
I am beginning to study type theory, using <PERSON>'s book "Basic Simple Type Theory", and I would like your help in the proof of a theorem. I would like to know whether my idea for how to prove the theorem is correct or not and if there are better/other ways to do it.
While learning about subject reduction and expansion I came across the following theorem:
2C2. Subject Expansion Theorem If $\Gamma \vdash_{\lambda} Q: \tau$ and $P \vartriangleright_{\beta} Q$ by non-duplicating and non-cancelling contractions, then $\Gamma \vdash_{\lambda} P: \tau$.
The author leaves the proof as an exercise and I am trying to do it. Here's my idea:
First, I wrote that it's sufficient to prove the theorem for a $\beta$-contraction (represented by $\vartriangleright_{1\beta}$) since a $\beta$-reduction (represented by $\vartriangleright_{\beta}$) is simply zero or more steps of $\beta$-contraction.
Next, I noticed that if $P \vartriangleright_{1\beta} Q$ then $P \equiv (\lambda x.M)N$ and $Q \equiv [N/x] M$. I also noticed that there must be exactly one occurrence of $x$ free in $M$, as the $\beta$ contraction is non-duplicating and non-canceling. Then, I tried a proof by induction on $|P|$. There are 3 cases:
Case 1: $M$ is a variable. In this case, since the contraction is non-duplicating and non-canceling, we must have $M \equiv x$. Then, $P \equiv (\lambda x.x)N$ and $Q \equiv N$. After standard calculations, I was able to derive the type of $P$ as being $\tau$.
Case 2: $M$ is an abstraction. In this case $P \equiv (\lambda x. \lambda y. 875
M_1)N$. Then, $Q \equiv [N/x] (\lambda y. M_1)$. My idea here is to use the induction hypothesis to say that $(\lambda x. M_1)N$ and $[N/x]M_1$ must have the same type $\tau_1$ and from there perform calculations to conclude that $P$ and $Q$ must have the same type $\tau$.
Case 3: $M$ is an application. In this case $P \equiv (\lambda x. M_1 M_2)N$. There will only be one free occurrence of $x$ in $(M_1 \ M_2)$ and we consider only the case of this free occurrence happening in $M_1$. (because the other case is analogous). Then, $Q \equiv [N/x] (M_1 \ M_2) = (([N/x] M_1) \ ([N/x] M_2)) = (([N/x] M_1) \ M_2)$. My idea is to use the induction hypothesis to say that $(\lambda x. M_1) N$ and $[N/x] M_1$ must have the same type $\tau_1$ and then performe calculations to prove that $P$ and $Q$ must have the same type $\tau$.
Is my approach to the problem correct? Are there better/other ways to proceed?
Thanks in advance. 875