### Proof by Coinduction

#### Posted by David Corfield

The sophisticated take on mathematical induction is that the natural numbers form the inital algebra of the endofunctor on $Set$, $F: X \to 1 + X$. As such we have a map $\langle 0, s \rangle: 1 + \mathbb{N} \to \mathbb{N}$, picking out the zero and the successor function. As an initial object in the category of $F$-algebras we know that any monomorphism into it must be an isomorphism. So if I have a property, $P$, of the natural numbers which holds for $0$, and for which $P(n)$ implies $P(s(n))$ for all $n$, then the set, $Y$, of natural numbers satisfying $P$ forms an $F$-algebra, $\langle 0, s \rangle: 1 + Y \to Y$, with an obvious monomorphism into $\mathbb{N}$. Hence $Y$ is isomorphic to $\mathbb{N}$ and $P$ holds for all natural numbers.

Now in the case of coalgebras, coinduction is going to rely on the fact that epimorphisms from terminal coalgebras are isomorphisms, i.e., there’s no quotient coalgebra of a terminal coalgebra. So if I want to establish that two elements of a terminal coalgebra are equal all I need do is find an equivalence relation which relates the elements and which is compatible with the coalgebra structure. Equivalence classes cannot contain more than one element, so I know these two elements are the same.

A typical place to use coinduction is with streams. Let $A^{\omega}$ be the set of streams, or infinite sequences, of elements of the set $A$. There is a map $A^{\omega} \to A \times A^{\omega}$ which takes a stream to the pair of its head (first element) and its tail (the rest). So $A^{\omega}$ is a coalgebra for the functor $G: X \to A \times X$, and indeed is the terminal $G$-coalgebra. A relation on $A^{\omega}$ compatible with the coalgebra structure is one for which $\sigma R \tau$ implies that $head(\sigma) = head (\tau)$ and $tail(\sigma) R tail (\tau)$. To establish the identity of two streams, we define a relation with this property such that the streams relate to each other. We can happily use coinduction then to prove things such as the merger of the list of even positioned elements of a list with the list of odd positioned elements of the same list yields the original list.

But do we ever use coinduction for the terminal coalgebra of $F: X \to 1 + X$? This is the extended natural numbers $\mathcal{N} = \mathbb{N} \cup \{\infty\}$ with the predecessor function, which we discussed earlier. To establish whether two extended natural numbers are the same all we need do is find a relation such that either the predecessor is undefined for both numbers or the relation holds of the predecessors of both.

Now Jan Rutten puts coinduction to use to prove commutativity of addition on the conaturals on page 36 of Universal coalgebra: a theory of systems. This relies on the idea that postulating a relation $(n + m) R (m + n)$ is compatible with the coalgebra structure, so they must be equal.

But we might wonder if there isn’t an example like the high school proof of induction of

$\sum_{i = 1}^n i = \frac{1}{2}n(n + 1),$

where you show it true for $n = 0$, and if true for $n$ then true for $(n + 1)$.

This was the best I could come up with. Let me define a binary relation which includes pairs $\langle (\sum_{i = 1}^n i) - m, \frac{1}{2} n(n + 1) - m \rangle$, for all natural numbers $n$ and $m$ such that $n \gt m \geq 0$. We also throw in $\langle 0, 0 \rangle$. To do this properly I would define subtraction coinductively, but we can take it that it works as it should.

Then I claim that this relation is compatible with the destructors. If $(n - 1) \gt m$, then applying the predecessor to each member of a pair yields another pair specified to be in the relation. If $m = (n - 1)$, we check that

$(\sum_{i = 1}^n i) - (m + 1) = (\sum_{i = 1}^n i) - n = \sum_{i = 1}^{n - 1} i.$

On the other hand,

$\frac{1}{2} n(n + 1) - (m + 1) = \frac{1}{2} n(n + 1) - n = \frac{1}{2} (n - 1)n.$

This pair is specified as being related. I probably need to say something about what happens for $n = 1$, but how does this strike people as a proof by coinduction? I guess it’s a tad too similar to induction to merit much attention.

Elsewhere in the blogosphere, Sigfpe has struggled with such matters.

## Re: Proof by Coinduction

Did you mean union?