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
Solution 1:
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.