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?
Thanks in advance.
Yes, this is fine.
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.