Lambda Calculus Prove Equality Excessive (Haskell-oriented)

Question

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?

Answer 1

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.

Answer 2

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 $