Coinduction - clear, concise description

Question

I am studying coinduction(not induction) as part of a class on static analysis. Rummaging around the internet, I am simply not finding clear, concise description of:

• What coinduction is
• How coinduction actually proves something(it seems that coinduction is like waving a magic hand in the treatments I've read)
• What propositions require coinductive proof
• How to operate a coinductive proof

Answer 1

My understanding (which may be wrong) goes like this:

Coinduction is a way to prove things about infinite data structures.

Just like induction, it seems like cheating at first. The key thing to realize is that instead of:

1. proving that something works for the base cases
2. proving that it works for each "single step", under the assumption that it works for all (finite) cases
3. then claiming that it therefore works for all (finite) cases (this is induction)

you instead:

1. prove, under the assumption that it works for all non-finite cases, that it works for each "single step"
2. claim that it therefore works for all non-finite cases (this is coinduction, and it's justified since each non-finite case is a (finite) sequence of single steps followed by a non-finite part which works by hypothesis)

Coinduction is a useful proof technique for establishing structurally "obvious" propositions about infinite data structures. Unfortunately (or not?) the fact that it's commonly useful for proving "obvious" things makes it harder to see how it is proving anything at all and not just hand-waving.

This paper is helpful in some ways, and confusing in others (at least those uninitiated in category theory, among whom I count myself).