2
$\begingroup$

I'm on a lambda calculus with parametric polymorphism a la Hindley-Milner Haskell-oriented course and I'm currently facing this exercise which I got stuck on.

Prove that $(\forall m\downarrow, n\downarrow :: N)\space (m+n)-m=n$

Definitions:

$(+)=\backslash m \space n \rightarrow case \space m \space of \space \{0\rightarrow n, Sx \rightarrow S(x+n)\}$

$pred = \backslash n \rightarrow case \space n \space of\{0\rightarrow 0,Sx\rightarrow x\}$

$(-)= \backslash m \space n \rightarrow case \space n \space of \space \{0\rightarrow m,Sx\rightarrow pred(m-x)\}$

Seems super simple but there's a part at which I got stuck. I also can only use the following already proven statements (may not need all):

$1) \space m+0=m$

$2) \space m + Sx = S(m+x)$

$3) \space m+n=n+m$

So here's what I did so far: I decided to prove this by using induction over m

$m=0, \space (0+n)-0=n-0=n$ is true (applying the given definitions for the functions)

$m=x, \space (m+n)-m=n$ is true (Hypothesis)

$m=Sx, \space (Sx+n)-Sx=n$ is true (Thesis)

Proof for $m=Sx$:

$(Sx+n)-Sx=S(x+n)-Sx=pred(S(x+n)-x)$ At which point I got stuck. I obviously have to get that $S$ out of $S(x+n)-n$ to have $(x+n)-n$ and apply the Hypothesis but I can't figure out how. Any ideas?

$\endgroup$
3
$\begingroup$

You need to strengthen your induction hypothesis by generalizing it over $n$:

$$\forall n, (m' + n) − m' = n, \qquad (\text{IH})$$ where $m = S\ m'$.

After that everything is easy:

$$ \begin{array}( (\mathsf{S}\ m' + n) - \mathsf{S}\ m' &= \qquad \text{(by definition of +)} \\ \mathsf{S}\ (m' + n) - \mathsf{S}\ m' &= \qquad \text{(by 2nd statement)} \\ (m' + \mathsf{S}\ n) - \mathsf{S}\ m' &= \qquad \text{(by definition of -)} \\ \mathsf{pred}( (m' + \mathsf{S}\ n) - m') &= \qquad \text{(by IH)} \\ \mathsf{pred}(\mathsf{S}\ n) &= \qquad \text{(by definition of pred)} \\ n \end{array} $$

If you are concerned about whether we're allowed to do that generalization, then I should say that we are. You started your proof of $$\forall m\ n, (m + n) − m = n,$$ by taking some arbitrary $m$ and $n$ and then proceeding by induction on $m$ with the following proposition: $$(m + n) − m = n.$$

But in the example I showed, we assume $m$ and proceed with $$\forall n, (m + n) − m = n,$$ which immediately gives us the generalized induction hypothesis.

$\endgroup$
4
$\begingroup$

Another way is to continue from where you got stuck, in the inductive step. You have:
$(Sx+n)−Sx=S(x+n)−Sx$

Now you can prove the following lemma by induction on y:

Lemma: $Sx - Sy = x - y$

  • case 0: $S(x) - S(0) = pred (S(x) - 0) = pred(S(x)) = x = x - 0$

  • given $Sx - Sy = x - y$, case $Sy$

    $Sx - S(Sy) = pred (Sx - Sy) = pred (x - y) = x - Sy$

then you continue:

$(Sx+n)−Sx=S(x+n)−Sx =^{(lemma)} (x + n) - x =^{(IH)} n $

$\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.