1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.