Prove if-case of strong normalization of simply typed lambda calculus

Question

I'm following this document on on how to prove strong normalization for the simply typed lambda calculus. I understand how this proof works. The if-case of the proof is left to the reader as an exercise. I tried to solve this exercise, but I'm quite confused on how to continue.

This is what I've found by now:

Case:
$$\cfrac{ \Gamma\vdash e:\mathtt{bool}\qquad \Gamma\vdash e_1:\tau\qquad\Gamma\vdash e_2:\tau} {\Gamma\vdash \mathtt{if}\ e\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2:\tau}$$

We know that $\gamma \vDash \Gamma$. Now we have to prove that $SN_\tau(\gamma(\mathtt{if}\ e\ \mathtt{then}\ e_1\ \mathtt{else}\ e_2))$ holds. By the definition of substitution we know that this is equivalent to proving that $SN_\tau(\mathtt{if}\ \gamma(e)\ \mathtt{then}\ \gamma(e_1)\ \mathtt{else}\ \gamma(e_2))$ holds.

The induction hypothesis tells us that $SN_{bool}(e)$, $SN_\tau(e_1)$ and $SN_\tau(e_2)$ holds.

But how can I continue from here?

PS: These are some of the definitions I've used.

$SN_\tau$ is a logical predicate. It is defined as follows:

$SN_{bool}(e) \equiv \bullet \vdash e : bool \space \land \space e \Downarrow$

$SN_{\tau_1\to\tau_2} \equiv \bullet \vdash e \land \space e \Downarrow \space \land \space (\exists e')(SN_{\tau_1}(e') \implies SN_{\tau_2}(e \space e')) $

$e \Downarrow \space \equiv (\exists v)(e \space \Downarrow \space v)$

$e \Downarrow v \equiv e \mapsto^\star v$

Answer 1

First, notice that the inductive hypothesis actually tells us that $\mathrm{SN}_{\mathit{bool}}(\gamma(e))$, $\mathrm{SN}_{\tau}(\gamma(e_1))$ and $\mathrm{SN}_{\tau}(\gamma(e_2))$ hold.

Since we know that $\mathrm{SN}_{\mathit{bool}}(\gamma(e))$ holds, by the definition of $\mathrm{SN}_{\mathit{bool}}$ we know that $\gamma(e) \Downarrow$. By the definition of $\gamma(e) \Downarrow$, we know that there exists a value $v$ such that $\gamma(e) \mapsto^* v$. Now you can proceed by case analysis on $v$.

For instance, suppose that $\gamma(e) \mapsto^* \mathrm{true}$. Then, by the evaluation rules we have that $\mathtt{if}\; \mathrm{true}\; \mathtt{then}\; \gamma(e_1)\; \mathtt{else\;} \gamma(e_2) \mapsto \gamma(e_1)$. By the inductive hypothesis, $\mathrm{SN}_{\tau}(\gamma(e_1))$ holds. Therefore $\mathrm{SN}_{\tau}(\mathtt{if}\; \gamma(e)\; \mathtt{then}\; \gamma(e_1)\; \mathtt{else\;} \gamma(e_2))$ holds by the lemma (SN preserved by forward/backward reduction).