# Proving commutativeness of an operator using structural induction

Let's suppose we have this language that defines natural numbers: $$\Bbb{N} = O : S \Bbb{N}$$

So a number can either be $O$ (zero) or $S \Bbb{N}$ (the successor of a natural).

Let's define the following function by recursion on $n$: $$sum (O, m) = m$$ $$sum (Sn, m) = sum (n, Sm)$$

What I want to prove is that $sum(n,m) = sum(m,n)$.

So I proceed by structural induction firstly proving that $sum(O,n) = sum(n,O)$, which is trivial.

The real question starts when I want to prove that $sum(n,m) = sum(m,n)$.

Before I prove that $sum(Sn, m) = S(sum(n,m))$ using structural induction on n.

If $n = O$: $sum(SO, m) = sum(O, Sm) = Sm = S(sum(O, m))$ Now suppose $sum(Sn, m) = S(sum(n,m)) \quad (IH)$ and prove that $sum(S(Sn),m) = S(sum(Sn,m))$.

In fact: $sum(S(Sn), m) = sum(Sn, Sm) = S(sum(n, Sm)) \text{by inductive hypothesis IH} = S(sum(Sn,m)) \text{by definition of sum}$

The question is: did I apply correctly the inductive hypothesis? Because IH states that $sum(Sn, m) = S(sum(n,m))$ while I said that $sum(Sn, Sm) = S(sum(n, Sm))$. There is that $Sm$ which is different, but the variable $m$ should not be a problem as it is not used for the induction. Right?

The proof goes along with another passage in which I do the same:

Now I want to prove $sum(n,m) = sum(m,n)$ by structural induction on $m$.

If $m=O$: $sum(n, O) = sum(O, n)$ is trivial.

Now suppose $sum(n, m) = sum(m,n) \qquad (IH1)$ and prove $sum(n, Sm) = sum(Sm, n)$ by structural induction on $n$

If $n=O$: $sum(O, Sm) = sum(Sm, O)$ is trivial.

Now suppose $sum(n, Sm) = sum(Sm, n) \qquad (IH2)$ and prove $sum(Sn, Sm) = sum(Sm, Sn)$.

We have that $sum(Sn, Sm) = S(sum(n, Sm)) \; \text{by preceding lemma} \; = S(sum(Sm, n)) \; \text{by IH2} \; = S(S(sum(m,n))) = S(S(sum(n,m))) \; \text{by IH1} \; = S(sum(Sn, m)) \; \text{by preceding lemma} \; = S(sum(m, Sn) \; \text{by IH1 (?)} \; = sum(Sm, Sn)$ like we wished to prove.

Again, the problem is when I applied IH1 in the last step (the question mark): could I do it?

Formally, your induction hypothesis is (for the first case): "$\forall m, sum(Sn,m) = S(sum(n,m))$", so substituting $Sm$ for $m$ is valid.
You may want to make this clear in the second problem as you do induct on both variables. So in the second example, your IH1 is "$\forall n, sum(n,m)=sum(m,n)$", and IH2 is "$sum(n,Sm)=sum(Sm,n)$", with $n,m$ fixed.