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.