Hi,

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

- 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

I have reviewed Wikipedia and a tutorial on co-induction/co-algebras.

My best understanding:

Coinduction is used in propositions such as:

```
f(x) = ... f(x) ...
```

Where `...`

denotes "stuff here that doesn't rely on f(x)".

Then, f(x) is assumed true, and the `...`

is proved. If `...`

holds, then the proposition `f(x)`

holds, out to and including infinity.

The treatments I've read include a *functional* function Q that takes f(x) and returns some f'(x), and somehow that makes it all better.

At an abstract level, I read that coinduction operates over a coalgebra, which is dual to induction/algebras.

This (1) seems awfully like circular reasoning and (2)seems awfully like voodoo. I suspect part of what I'm missing is a careful *and clear* description of coalgebras, plus how we jump from algebra into a coalgebra and back again. The professor declined to go into that part of the subject.

Note: I'm not an algebraicist by study- I write software and my thesis is over low-level software operations. So this is really unfamiliar to me and I'm trying to de-jargon this into my head.

(semi-cross-posted from stackoverflow.com)