# 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