The Coq mailing list

[José Manuel Rodriguez Caballero <josephcmac AT gmail.com>]

Dear Siddharth,

  The mathematics is not a religion. The question is not if you believe or not. The question is to organize a hierarchy of consistency. I quote Bishop 1967, Chapter 1, A Constructivist Manifesto, page 2:

"The primary concern of mathematics is number, and this means the positive integers. . . . In the words of Kronecker, the positive integers were created by God. Kronecker would have expressed it even better if he had said that the positive integers were created by God for the benefit of man (and other finite beings). Mathematics belongs to man, not to God. We are not interested in properties of the positive integers that have no descriptive meaning for finite man. When a man proves a positive integer to exist, he should show how to find it. If God has mathematics of his own that needs to be done, let him do it himself."

In this wonderful book there is an explanation of why even "induction" is problematic because of impredicativity : https://web.math.princeton.edu/~nelson/books/pa.pdf

Kind Regards,

José M. 

2018-05-11 19:37 GMT+02:00 Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>:

Hi Siddharth,

Long story short, there is a very suitable paper for this question: https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf

Practical coinduction - cs.cornell.edu

www.cs.cornell.edu

http://journals.cambridge.org Downloaded: 10 Feb 2016 IP address: 104.229.211.75 Practical coinduction 3 Although there is a coinductive step but no basis, any difficulty that would arise that

I personally find the two proofs on page 5 and 6 clearly illustrates the dual positions between induction and co-induction.

It's not rarely to see in lots of papers that "accuse" co-inductive proof of being "uncommon' or "not standard", while co-induction is actually as strong as induction, but proves things that cannot be reasoned by induction, and they come hand in hand. It's a common phenomenon that people are much more familiar with one thing, but not its dual.

I would prefer to think induction as a proof of "property P must hold", while co-induction as a proof of "property P cannot fail". In induction, we pretty much discuss two things: we show that P holds for all base cases, and then all other cases will eventually be reduced to those base cases, which requires the structure we look at must be finite.

In co-induction, however, for every case we look at, either the information is sufficient to conclude P, or we must look at the tail. Here is the kick: in proper co-induction, we must have some constructor appear in the head position, which allows the cases to be covered by the previous proof that we begin with.

Another way to look at them is, induction is a "sum" type of proof, which is divided by cases; while co-induction is a "product" type of proof, which is divided by fields from the same constructor.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Siddharth Bhat <siddu.druid AT gmail.com>
Sent: May 11, 2018 1:13:54 PM
To: Coq-Club Club
Subject: [Coq-Club] I don't believe Coinduction; Please help me grok it :)

 

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!