[Coq-Club] I don't believe Coinduction; Please help me grok it :)

[Siddharth Bhat]

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

[José Manuel Rodriguez Caballero]

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.

Hi Siddharth,
https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf
Practical coinduction - cs.cornell.edu
<https://www.cs.cornell.edu/~kozen/Papers/Structural.pdf>
www.cs.cornell.edu
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*
------------------------------
*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
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!

[Ken Kubota]

Dear José,

If it appears alone, impredicativity (self-reference) shouldn't be a problem.
I have tried to give some reasoning from a philosophical perspective here:
The two characteristics of an antinomy: self-reference and negation
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html <https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-June/msg00048.html>

Similarly, not all mathematicians consider impredicativity (self-reference) as problematic.
For example, Freek Wiedijk doesn't seem to share the common view, as this rather
sceptical quote might indicate:
"Apparently impredicativity is not to be trusted for philosophical reasons." [Wiedijk, 2007, p. 127]
http://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf <http://www.cs.ru.nl/F.Wiedijk/pubs/qed2.pdf>, p. 7


My concern with induction is that it shouldn't be formalized in a way extending
the syntax, as it can be encoded in a perfectly natural way within the formal
(syntactic) language of higher-order logic.
The Principle of Mathematical Induction can simply be expressed in a definition,
see Andrews' definition of N in Q0:
"Noσ stands for [λnσ∀poσ 􏰀 [poσ0σ ∧ ∀xσ􏰀 poσxσ ⊃ poσ􏰀Sσσxσ] ⊃ poσnσ]"
[Andrews, 2002, p. 260], also available online at
http://www.owlofminerva.net/files/fom.pdf <http://www.owlofminerva.net/files/fom.pdf>, p. 5
Peter Andrews explains: “The Induction Principle simply limits the size of the set.”
[Andrews, 2002, p. 259]
The definition of N in the R0 software implementation is available as wff 332 at
http://doi.org/10.4444/100.3 <http://doi.org/10.4444/100.3>, p. 370
The wff 333 is the well-formed formula with type abstraction (type variable t bound
by lambda).

I have to admit that I'm not too familiar with the details of Coq, but I believe that in it
induction is hardwired into the formal language (the syntax), which I consider problematic.

The rationale of expressing all of mathematics from very few means, which Andrews
calls "expressiveness", is discussed at
https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html <https://sympa.inria.fr/sympa/arc/coq-club/2017-02/msg00024.html>


For references, please see: http://doi.org/10.4444/100.111 <http://doi.org/10.4444/100.111>

Kind regards,

Ken Kubota

____________________________________________________


Ken Kubota
http://doi.org/10.4444/100 <http://doi.org/10.4444/100>

Post by José Manuel Rodriguez Caballero
Dear Siddharth,
"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 <https://web.math.princeton.edu/~nelson/books/pa.pdf>
Kind Regards,
José M.