[Solved]: Confluence proof for a simple rewriting system

Problem Detail: 

Assume we have a simple language that consists of the terms:

• $\mathtt{true}$
• $\mathtt{false}$
• if $t_1,t_2,t_3$ are terms then so is $\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$

Now assume the following logical evaluation rules:

$$ \begin{gather*} \dfrac{} {\mathtt{if}\: \mathtt{true} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_2} \text{[E-IfTrue]} \quad \dfrac{} {\mathtt{if}\: \mathtt{false} \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to t_3} \text{[E-IfFalse]} \\ \dfrac{t_1 \to t_1'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1' \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3} \text{[E-If]} \\ \end{gather*} $$

Suppose we also add the following funky rule:

$$ \dfrac{t_2 \to t_2'} {\mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3 \to \mathtt{if}\: t_1 \:\mathtt{then}\: t_2' \:\mathtt{else}\: t_3} \text{[E-IfFunny]} $$

For this simple language with the given evaluation rules I wish to prove the following:

Theorem: If $r \rightarrow s$ and $r \rightarrow t$ then there is some term $u$ such that $s \rightarrow u$ and $t \rightarrow u$.

I am proving this by induction on the structure of $r$. Here is my proof so far, it all worked out well, but I am stuck at the very last case. It seems like induction on the structure of $r$ is not sufficing, can anyone help me out?

Proof. By induction on $r$, we will seperate all the forms that $r$ can take:

1. $r$ is a constante, nothing to prove since a normal form does not evaluate to anything.
2. $r=$ if true then $r_2$ else $r_3$. (a) both derivations were done with the E-IfTrue rule. In this case $s=t$, so there is nothing to prove. (b) one deriviation was done with the E-IfTrue rule, the other with the E-Funny rule. Assume $r \rightarrow s$ was done with E-IfTrue, the other case is equivalently proven. We now know that $s = r_2$. We also know that $t =$ if true then $r'_2$ else $r_3$ and that there exists some deriviation $r_2 \rightarrow r'_2$ (the premise). If we now choose $u = r'_2$, we conclude the case.
3. $r=$ if false then $r_2$ else $r_3$. Equivalently proven as above.
4. $r=$ if $r_1$ then $r_2$ else $r_3$ with $r_1 \neq $ true or false. (a) both deriviations were done with the E-If rule. We now know that $s =$ if $r'_1$ then $r_2$ else $r_3$ and $t =$ if $r''_1$ then $r_2$ else $r_3$. We also know that there exists deriviations $r_1 \rightarrow r'_1$ and $r_1 \rightarrow r''_1$ (the premises). We can now use the induction hypothese to say that there exists some term $r'''_1$ such that $r'_1 \rightarrow r'''_1$ and $r''_1 \rightarrow r'''_1$. We now conclude the case by saying $u =$ if $r'''_1$ then $r_2$ else $r_3$ and noticing that $s \rightarrow u$ and $t \rightarrow u$ by the E-If rule. (b) one derivation was done by the E-If rule and one by the E-Funny rule.

This latter case, where one derivation was done by E-If and one by E-Funny is the case I am missing... I can't seem to be able to use the hypotheses.

Help will be much appreciated.

Asked By : codd

Answered By : sepp2k

Okay, so let's consider the case that $r = \mathtt{if}\: t_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$, $s$ has been derived by applying the E-If rule and $t$ has been derived by applying the E-Funny rule: So $s = \mathtt{if}\: t'_1 \:\mathtt{then}\: t_2 \:\mathtt{else}\: t_3$ where $t_1 \rightarrow t'_1$ and $t = \mathtt{if}\: t_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$ where $t_2 \rightarrow t'_2$.

The $u$ we're looking for is $u = \mathtt{if}\: t'_1 \:\mathtt{then}\: t'_2 \:\mathtt{else}\: t_3$. $s \rightarrow u$ follows from rule E-Funny and $t \rightarrow u$ follows from rule E-If.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/1060