# Proving equivalence of two substitutions by induction

I'm trying to prove the following reduction: $$t\{x:=u\}\{y:=v\} = t\{y:=v\}\{x:=u\{y:=v\}\}$$ under the following assumptions:

1. $$x \neq y$$
2. $$x$$ is not a free variable of $$v$$ (in symbols, $$x \notin \operatorname{fv}(v)$$).

My idea is to do it by induction, but I'm a bit stuck with the base case. I would appreciate if someone can explain to me how to write such a proof. I'm including what I tried, which is wrong or incomplete.

Base case: $$t = m$$ is just a variable.

On the left side we have:

if m = x ⟹ u{y:=v} (if u=y then v else u)
else     ⟹ m{y:=v} (if m=y then v else m)


On the right side we have:

if m=y ⟹ v{x:=u{y:=v}} (if u=y then v{x:=v} else u{x:=u}
so we get either (v=x ⟹ v else v) or (u=x ⟹ u else u)
else   ⟹ m{x:=u{y:=v}} (if m=y then m{x:=v} else m{x:=u}
so we get either v or m


I understand we end up getting the same four branches, but is that considered really a proof? Is this the proper way to write such a proof and conclude the base case? Also, the given assumptions didn't help much here, so I think I'm missing the part where I need to use those assumptions...

I think once the base case is proven, we can do the following:

Case $$t = t_1t_2$$:

$$t\{x:=u\}\{y:=v\} \Longrightarrow t_1t_2\{x:=u\}\{y:=v\} \Longrightarrow \\ t_1\{x:=u\}\{y:=v\} t_2\{x:=u\}\{y:=v\},$$ and we have just proven in the base case that $$t_1\{x:=u\}\{y:=v\} = t_1\{y:=v\}\{x:=u\{y:=v\}\}$$ and $$t_2\{x:=u\}\{y:=v\} = t_2\{y:=v\}\{x:=u\{y:=v\}\}$$, so \begin{align} &t_1\{x:=u\}\{y:=v\} t_2\{x:=u\}\{y:=v\} \\ =& t_1\{y:=v\}\{x:=u\{y:=v\}\} t_2\{y:=v\}\{x:=u\{y:=v\}\} \\ = &t_1t_2\{x:=u\}\{y:=v\} \\ = &t_1t_2\{y:=v\}\{x:=u\{y:=v\}\}. \end{align}

Now only case left is $$t= \lambda m . t$$. So we have $$(\lambda m . t)\{x:=u\}\{y:=v\}$$, which can be directly re-written as $$\lambda m . t\{x:=u\}\{y:=v\}$$, which is the base case again...

Could someone please help me finish this proof correctly and explain to me the right way to do it?

• Your text is impossible to read. This is not how one would write a proof. I started rewriting your proof, but since your question is about how to write proofs, I abandoned my attempt. Consult some lecture notes to see how proofs are usually written. – Yuval Filmus Jan 13 at 8:48
• @YuvalFilmus thx for taking the time to rewrite my question and answer me with such clear explanation ! – user206904 Jan 13 at 11:30

First, let us show that the two assumptions are necessary. Here is an example showing what goes wrong when $$x = y$$. Take $$t = x$$, $$u = 1$$, $$v = 2$$. We have $$x\{x := 1\}\{x := 2\} = 1\{x := 2\} = 1,$$ whereas $$x\{x := 2\}\{x := 1\{x := 2\}\} = 2\{x := 1\} = 2.$$

Next, here is an example showing what goes wrong when $$x$$ is not free in $$v$$. Take $$t = y$$, $$x = 1$$, $$y = x$$. We have $$y \{x := 1\}\{y := x\} = y\{y := x\} = x,$$ whereas $$y \{y := x\}\{x := 1\{y := x\}\} = x\{x := 1\} = 1.$$

Now let's do the base case more carefully. The term $$t$$ is just a variable. We have to consider three possibilities: $$t=x$$, $$t=y$$, $$t \neq x,y$$.

If $$t=x$$ then $$t\{x := u\} = u$$, and so the left-hand side is $$u\{y := v\} = u\{y := v\}$$. On the other hand, $$t\{y := v\} = x$$ (since $$x \neq y$$), and so the right-hand side is $$x\{x := u\{y := v\}\} = u \{y := v\}$$.

If $$t=y$$ then $$t\{x := u\} = y$$ (since $$y \neq x$$), and so the left-hand side is $$y\{y := v\} = v$$. On the other hand, $$t\{y := v\} = v$$, and so the right-hand side is $$v\{ x:= u\{y := v\} \} = v$$, since $$x$$ doesn't appear freely in $$v$$.

Finally, if $$t \neq x,y$$ then both sides are just equal to $$t$$, since the substitutions have no effect.

Next, the rest of the proof. The proof for function application is essentially as you wrote it. Let us denote the left-hand side by $$L(t)$$ and the right-hand side by $$R(t)$$. If $$t = t_1t_2$$ then $$L(t) = L(t_1) L(t_2) \stackrel{(\ast)}= R(t_1) R(t_2) = R(t),$$ where $$(\ast)$$ is due to the induction hypothesis.

Finally, we need to handle abstraction. Let $$t = \lambda m.s$$. Applying $$\alpha$$-conversion, we can assume without loss of generality that $$m \neq x,y$$. This implies that $$L(t) = \lambda m.L(s) = \lambda m.R(s) = R(t).$$ To see why $$\alpha$$-conversion is necessary, try doing the proof when $$m=x$$ or $$m=y$$. The case $$m=x$$ works out fine, but you will encounter a problem when $$m=y$$.