The Coq mailing list

[Siddharth Bhat <siddu.druid AT gmail.com>]

This title is click-baity, but I believe it captures my feelings adequately.

I am able to "believe" induction on, say, the naturals, since they have a well-founded order. Hence, one can intuit what it means to "perform induction" on these kinds of objects.

On the other hand, how does a Coinduction proof "start"? Or, well, how does one intuit cofix ? I'm now able to perform the proofs in Coq, but I really don't feel like I understand them.

The rough argument that I have in my head to justify Coinduction is as follows:

1. A Coinductive proof technique is used to prove a proposition P on functions that lazily produce infinite amounts of data.

2. We can only observe a finite amount of this infinite data

3. Hence, to prove a Coinductive proposition, we can assume our proposition P holds on the "infinite tail that is unobserved", and we show that adding some new finite data does not break the invariant P.

4. So, when someone "observes" this infinite data to some length, we can assume that the proposition P holds for the "part that remains unobserved", and "work our way backwards" to add all the finite pieces that were observed, while making sure P holds.

How do the experts think about Coinduction? Is my intuition at all correct? I'd love help and feedback on this!

Thanks,

~Siddharth

--

Sending this from my phone, please excuse any typos!