# Are coinductive proofs necessary?

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

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

• 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 – Charles Stewart Dec 13 '19 at 15:45