# PL: How can I prove the type of something using “Inversion for Typing”?

I'm currently going through this book about programming languages, and in section 4.2, Lemma 4.2 it says this:

Lemma 4.2 (Inversion for Typing). Suppose that $\Gamma \vdash e : \tau$. If $e = \texttt{plus}(e_1;e_2)$, then $\tau = \texttt{num}$, $\Gamma \vdash e_1 : \texttt{num}$, and $\Gamma \vdash e_2 : \texttt{num}$ ...

Proof. These may all be proved by induction on the derivation of the typing judgment $\Gamma \vdash e : \tau$.

I understand that this is obviously true, but I don't understand how I might explicitly write out the proof for this (e.g., what does "induction on the derivation of the typing judgment" mean?)

This is my current understanding:

The derivation of the typing judgement is simply the sequence of rules applied to figure out the type of some expression (in this case, $e$).

For example, if I have $e_1 : \texttt{num}$ and $e_2 : \texttt{num}$, and I wish to find the type of $\texttt{plus}(e_1;e_2)$, I could derive it as follows in one step according to the rules of the language:

$$\frac{\Gamma \vdash e_1 : \texttt{num}, \Gamma \vdash e_2 : \texttt{num}}{\Gamma \vdash \texttt{plus}(e_1;e_2) : \texttt{num}}$$

But I don't know what it means to use induction "on the derivation".

• I answered a similar question about induction on type derivations here, which may be of some use to you. – Daniel Mroz Sep 8 '18 at 22:32
• – D.W. Sep 9 '18 at 0:50