Intuition on what to perform (structural) induction on or clues when one's stuck while conducting a proof by induction

58 Views Asked by At

Suppose we're working with Peano representation of natural numbers so as to have structural inductive approach and suppose we have an inductive definition for parity of natural numbers as follows:

$ev \in \mathbb{N} \rightarrow EvenParity\\ zero :\ \ ev\ 0 \\ more : \forall n \in \mathbb{N}, ev\ n \rightarrow ev\ (S\ (S\ n))$

So either zero is even, or, given an even $n \in \mathbb{N}$, then application of successor two times $S\ (S\ n))$ also forms an even number.

To finish the definition, suppose these are the only ways to construct an even number.

Now we want to prove the following: $\forall n\ m \in \mathbb{N}, ev\ (n + m) \rightarrow ev\ n \rightarrow ev\ m$

Let us name our hypotheses as follows:

$ev\ (n + m)\ is\ H$
$ev\ n\ \ \ \ \ \ \ \ \ \ \ \ \ is\ H'$

Now there are several ways to continue the proof. We can perform induction on $n$, $m$, $H$ or $H'$.

The proof is rather trivial if one performs induction on $H'$, that is $ev\ n$.
First we need to show $ev\ m$ under the assumption that $n = 0$ (considering the equation $zero$), hence $ev\ (0 + m)$, this reduces to $ev\ m$ which is what we wanted to prove.

Now we need to show $ev\ m$ under the assumption that the number has been built from $more$, that is $n = S\ (S\ n))$. Using the inductive hypothesis $ev\ (n + m) \rightarrow ev\ m$, we see $ev\ m$ follows from $ev\ (n + m)$. From $ev\ (S\ (S\ n) + m))$ we can get $ev\ (S\ (S\ (n + m)))$, from which $ev\ (n + m)$ and we're done.

However, if I try to conduct a similar proof by induction using any of the other possibilities, I get stuck very quickly in the $more$ case.

For example, consider we try induction on $m$ (over the Z | S n structure).
First, $m = 0$, hence we need to show $ev\ 0$. This follows from definition.

However, now we need to show $ev\ (S\ m)$. Here we only know $ev\ (n + S\ m)$, $ev\ n$ and our inductive hypothesis $ev\ (n + m) \rightarrow ev\ m$. The proof gets messy at this point, could perhaps be done by showing that even parity of successor of n follows from uneven, but I am not sure - still, it gets comparatively complicated very quickly.

How does one know what to perform induction on and what are some common clues that a proof leads just about nowhere - for example in the induction over $m$ case, I can see that my hypotheses are close to useless, as I need to show $ev\ (S\ m)$ from $ev\ (n + S\ m)$, $ev\ n$ and $ev\ (n + m) \rightarrow ev\ m$.