World's most popular travel blog for travel bloggers.

# [Answers] Proof via induction for small-step semantics

, ,
Problem Detail:

I'm doing a course in Computer Programming Languages and I'm trying to prove the following (roughly following Pierce's Types and Programming Languages book):

if $t \rightarrow^* t'$ then $if\; t\; then \; t2 \; else \; t3 \rightarrow^* if\; t'\; then \; t2 \; else \; t3$

I'm a little confused about where to start; as far as I know, I'm supposed to define a base case, then prove it via induction.

I've started my proof by assuming these base cases:

$P(\frac{}{true \rightarrow^* true})$ and $P(\frac{}{false \rightarrow^* false})$.

I'm stuck at this point, and I don't really how know to proceed.

edit: I've added the syntax in an effort to clear things up. #### Answered By : Andrej Bauer

The induction should be on the derivation of $t \to^* t'$:

• If $t \to t'$ in one step, then we get the desired result by the E-IF rule.

• Suppose $t \to^* t'$ because $t \to t'' \to^* t'$. By the E-IF rule we have $$(\mathtt{if}\;t\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to (\mathtt{if}\;t''\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3)$$ and by the induction hypothesis $$(\mathtt{if}\;t''\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to^* (\mathtt{if}\;t'\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3).$$ These two together give us the desired $$(\mathtt{if}\;t\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3) \to^* (\mathtt{if}\;t'\;\mathtt{then}\;t_2\;\mathtt{else}\;t_3).$$