tag removed - Co-induction understanding

Here's an informal example of a proof by coinduction.

The extended natural numbers E = {0, 1, 2, ..., ∞} are the final coalgebra for the functor F(X) = 1 + X. (If we have an F-coalgebra X, i.e. a set X with a map f : X -> 1 + X, and an element of X, what we can do is repeatedly apply f until we get the element of 1 rather than a new element of X. Counting the number of times we got new elements of X gives us an element of E. This is the unique F-coalgebra map X -> E.) In Haskell we would write

data Nat = Z | S Nat   -- possible values are Z, S Z, S (S Z), ..., S (S (S ...))

We can define addition:

add :: Nat -> Nat -> Nat
add Z b = b
add (S a1) b = S (add a1 b)

I'll prove that add a Z = a by coinduction. We perform case analysis on a. If a = Z then it follows from the first equation. If a = S a1 then add a Z = add (S a1) Z = S (add a1 Z) = S a1 = a where the next-to-last step used the coinductive hypothesis.

Why isn't that circular reasoning? We were allowed to apply the coinductive hypothesis because we did so inside an application of the "constructor" S. In other words, even if you didn't believe the coinductive hypothesis, you would still conclude that add a Z and a were both of the form Z or both of the form S x--in other words, add a Z and a agree for to one observation. Using that statement where we used the coinductive hypothesis, you find that add a Z and a agree to two observations, etc. Since an element of E is determined by all the finite sequences of observations we can make, it follows that add a Z = a.

(Note that this argument works even when a = S (S (S ...))!)

Exercise: Give a formal version of this argument, using the definition of E as the final F-coalgebra.