What are some good examples of _Proof by Mutual Induction_?

Question

Sometimes programs rely on mutual recursion to do things. For example, here is an Agda program (taken from here that proves ∀ {m n : ℕ} → even m → even n → even (m + n) and ∀ {m n : ℕ} → odd m → even n → odd (m + n) by using one fact to prove the other during induction. This example is also explained here

import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open import Data.Nat using (ℕ; zero; suc; _+_)

data even : ℕ → Set
data odd : ℕ → Set

data even where
  zero : even zero
  suc : ∀ {n : ℕ} → odd n → even (suc n)

data odd where
  suc : ∀ {n : ℕ} → even n → odd (suc n)

e+e≡e : ∀ {m n : ℕ} → even m → even n → even (m + n)
o+e≡o : ∀ {m n : ℕ} → odd m → even n → odd (m + n)

e+e≡e zero     en = en
e+e≡e (suc om) en = suc (o+e≡o om en)

o+e≡o (suc em) en = suc (e+e≡e em en)

Another example is this (in Haskell) (from here). Suppose you want to identify sequences which keep increasing or decreasing alternately.

alternating :: [Int] -> Bool
alternating l = (updown l) || (downup l)

updown :: [Int] -> Bool
updown [] = True
updown [x] = True
updown (x:y:ys) = (x < y) && (downup (y:ys))

downup:: [Int] -> Bool
downup [] = True
downup [x] = True
downup (x:y:ys) = (x > y) && (updown (y:ys))

What are some other examples of mathematical proofs which are more naturally expressed with mutual induction?

The most non-trivial example I can think of is the proof of Strong Normalization Theorem for Simply Typed Lambda Calculus (see page 42, section 6.2 here). However, this is a very technical property that I suppose mainstream mathematicians are not really interested in.

Answer 1

In my opinion, the strong normalization theorem for simply typed $\lambda$-calculus is not a negligible result, at least in theoretical computer science (which is much closer to mathematics than software development or web programming).

In general, proofs by mutual induction are quite common in theoretical computer science, which deals with discrete objects often defined by induction or mutual induction. In general, a proof by mutual induction of a statement $A$ consists in proving a stronger statement than $A$, usually a statement of the form $A \land B$ (i.e. $A$ and $B$), where $B$ can be seen as an "auxiliary statement". The advantage is that now one can use a stronger induction hypothesis than in a proof of the mere statement $A$ by simple induction.

I guess you are interested in examples of proofs by mutual induction concerning ordinary objects of mathematics. No famous result in ordinary mathematics whose proof makes use of mutual induction in a crucial way crosses my mind. Anyway, the following is a nice example of a property about natural numbers that cannot be proved by simple induction (at least, not in a natural way), but the proof by mutual induction is very easy, because it gives a stronger induction hypothesis.

Let $f, g, h \colon \mathbb{N}\to \{0,1\}$ be functions defined as follows: \begin{align} f(n) &= \begin{cases} 0 &\text{if } n = 0 \\ g(n - 1) &\text{otherwise} \end{cases} & g(n) &= \begin{cases} 1 &\text{if } n = 0 \\ f(n - 1) &\text{otherwise} \end{cases} \\[0.5em] h(n) &= \begin{cases} 0 &\text{if } n = 0 \\ 1- h(n - 1) &\text{otherwise} \end{cases} \end{align}

Proposition. For every $n \in \mathbb{N}$, one has $h(n) = f(n)$.

It does not seem possible to prove the proposition by simple induction, the induction hypothesis in this case is too weak. But the proof is quite easy if you prove the following stronger statement, by (mutual) induction on $n \in \mathbb{N}$:

Proposition'. For every $n \in \mathbb{N}$, one has $h(n) = f(n)$ and $h(n) = 1 - g(n)$.

Proof. By induction on $n \in \mathbb{N}$.

Base case. $f(0) = 0 = h(0)$ and $h(0) = 0 = 1 - 1 = 1- g(0)$.

Inductive step. By induction hypothesis (i.h.), $f(n) = h(n)$ and $h(n) = 1 - g(n)$. Hence, \begin{align} f(n+1) &= g(n) \overset{i.h.}{=} 1 - h(n) = h(n+1) \\ h(n+1) &= 1 - h(n) \overset{i.h.}{=} 1 - f(n) = 1 - g(n+1). \qquad \square \end{align}

Note that in the inductive step, to prove that $f(n+1) = h(n+1)$ we use the inductive hypothesis about the second statement, i.e. $h(n) = 1 - g(n)$. Conversely, to prove that $h(n+1) = 1 - g(n+1)$ we use the inductive hypothesis about the first statement, i.e. $f(n) = h(n)$. This is the essence of mutual induction.

Answer 2

In set theory, there is no shortage of statements whose "natural proofs" are via mutual induction. The first one that comes to mind:

Theorem. For any ordinal $\alpha$, $(J_\alpha; \in)$ (in the Jensen hierarchy) is sound and acceptable.

The basic gist is that you use soundness of $(J_{\alpha}; \in)$ to prove acceptability of $(J_{\alpha+1}; \in)$ and then use the latter to prove soundness of $(J_{\alpha+1}; \in)$.