I've been exploring corecursion in Coq (specifically, infinite streams of natural numbers) lately and so far any coinductive predicate I've constructed and its coinductive proof can be transformed into an inductive predicate and an inductive proof with a proof that either style proof can be constructed from the other. Certainly the coinductive version is often easier to write, but is there anything that can be proven with coinduction that cannot be with induction? Maybe it is the case for infinite streams but there are other infinite objects where this is not true?

As an example I have the coinductive predicate

$\operatorname{increasing} : \forall s\,n,\; n < \operatorname{head} s \implies \operatorname{increasing} s \implies \operatorname{increasing} (n \operatorname{cons} s)$

and the inductive predicate

$\operatorname{increasing'} : \forall s,\; (\forall n,\; s[n] < s[n+1]) \implies \operatorname{increasing'} s$

and a proof that

$\forall s,\; \operatorname{increasing} s \iff \operatorname{increasing'} s$

Intuitively it seems like the coinductive principle says something like "you can never see a falsification of the predicate" which can be turned around to an inductive argument on the number of observations or equivalently how much of the infinite object you force.

If you'd like to see the Coq development for the increasing predicate it is at https://gist.github.com/3953040

  • $\begingroup$ as a corollary, are coinductive definitions necessary? $\endgroup$ – Rodrigo Oct 21 '19 at 13:36

Inductive proofs can only directly prove properties of the set of finite initial subsequences of streams - it cannot directly prove anything about infinite streams. This is because the induction only "reaches" well-founded elements of the type constructor, while coinductive proofs reach all of these elements and the ill-founded elements, such as the infinite sequence 1,2,3,...

That said, by appeal to the take lemma (two streams that agree on all initial subsequences of given length are the same), you can use inductive proofs to reason about all streams. But you cannot prove the take lemma inductively.

  • 2
    $\begingroup$ if would be curious to see a proof of the fact that "two streams that agree on all initial subsequences of given length are the same" cannot be proven inductively $\endgroup$ – Rodrigo Oct 21 '19 at 13:24
  • $\begingroup$ @Rodrigo From the point of view of dependent type theory, inductive proofs simply are proofs by recursion, and so they are only possible over well-founded types. Because of well-foundedness, I can prove that any nonempty list is distinct from its tail - the tail is shorter than it. $\endgroup$ – Charles Stewart Dec 13 '19 at 14:25
  • $\begingroup$ This "is shorter" is formalisable by the existence of a purely recursive length function: length(n:ns)=1+length(ns). $\endgroup$ – Charles Stewart Dec 13 '19 at 15:42
  • $\begingroup$ But we can construct streams that are not distinct from their tail, e.g., ones=1:ones. The length function is not total on streams: the recursive basis of inductive proofs does not extend to non-wellfounded objects like ones $\endgroup$ – Charles Stewart Dec 13 '19 at 15:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.