When can the coinduction hypothesis be used?

Question

We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this.

When it comes to coinduction, I'm confused.

One of the answers to another question "What is coinduction?" mentions that there is a notion of a corecursive definition to be well-formed.

A lot of things I (try to) read related to coinduction mostly talk about bisimulation and equivalence. But to the best of my knowledge, those are trying to prove some relationship for two coinductive data structures. For example, they prove that two streams are equivalent. And the coinductive hypothesis is somehow derived from one of the bisimulation's hypothesis. Even so, I think I'm still lost on the requirements of what constitutes well-formedness in the coinductive world.

I can somehow see that the coinduction hypothesis works when proving those kinds of propositions, but I'm still unclear when they can be used to prove more general propositions such as the one mentioned in What is coinduction?. In that link, the proposition states that "something is infinite". This seems like a more generic form of statement one would be interested in proving.

A possibly related question is whether any proposition can be converted and re-stated as a proposition of equivalence or not.

Is there some simple informal reasoning that talks why co-induction works for some well-formedness requirement?

I'm hoping for an explanation like if possible: https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.

Answer 1

First, let me recall least and greatest fixed points for $\subseteq$. We are working relative to some set $U$, the universe. In the case of (co)inductive definitions, $U$ is the set of all terms. A function $f:2^U\to2^U$ (from subsets of $U$ to subsets of $U$) is monotone, if $A\subseteq B$ always implies $f(A)\subseteq f(B)$. A fixed point of $f$ is a set $A$ such that $f(A)=A$.

For monotone $f$ there always is a least fixed point $\mu f$, namely the intersection of all $A\subseteq U$ such that $f(A)\subseteq A$. Least means that for arbitrary fixed points $F$ we always have $\mu f\subseteq F$.

For an example, let $f_{\tt nat}$ be defined by $f_{\tt nat}(A)=\{0\}\cup\{n+1\mid n\in A\}$. The function $f_{\tt nat}$ is the one-step closure function under the constructors $0$ and $+1$. The condition $f_{\tt nat}(A)\subseteq A$ means that $A$ is closed under the constructors $0$ and $+1$. The intersection means that the $\mu f_{\tt nat}$ contains only those elements which are in every set closed under the constructors. These happen to be the natural numbers. The example shows how the inductive definition of natural numbers is the least fixed point of closure under the natural numbers' constructors. Generally, inductively defined sets are least fixed points of closure under constructors.

Dually, for monotone $f$ there also is a greatest fixed point $\nu f$, namely the union of all $A\subseteq U$, such that $f(A)\supseteq A$. Greatest means that for arbitrary fixed points $F$ we always have $\nu f\supseteq F$. To make the duality complete, let us note that intersection is the $\subseteq$-infimum and union the $\subseteq$-supremum and thus the $\supseteq$-infimum. So, in fact, greatest fixed points for $\subseteq$ are just least fixed points for $\supseteq$ and vice versa. (Also, observe that the requirement of monotonicity is the same for $\subseteq$ as for $\supseteq$.)

Now, for proof techniques. Let us begin with the example of induction on natural numbers. To show that some property $P$ holds for all natural numbers, we show that $P(0)$ and that $P(n)$ implies $P(n+1)$. Viewing $P$ as a subset of $U$ (the set of all elements where the property holds), the proof obligation for natural induction is that $P$ is closed under $f_{\tt nat}$. Correctness of the proof technique of natural induction then follows from the definition of least fixed point: If $f_{\tt nat}(P)\subseteq P$, then $P$ is part of the intersection that forms $\mu f_{\tt nat}$, so the property holds throughout $\mu f_{\tt nat}$, that is $\mu f_{\tt nat}\subseteq P$.

Induction is just the generalization of the previous paragraph to arbitrary monotone $f$ instead of $f_{\tt nat}$. Coinduction is the dual of induction: The proof obligation is $f(P)\supseteq P$. This means that if $P$ holds on some element $x$, then $x$ is constructed using only base elements on which $P$ also holds. So, instead of showing that the property survives application of constructors, we have to show that it survives deconstruction. Once the proof obiligation is satisfied, we obtain $\nu f\supseteq P$.

What good is the conclusion $\nu f\supseteq P$? Let us reconsider $P$ not as a property but as a subset of $U$. The conclusion of coinduction establishes that all elements of $P$ are well-formed members of the coinductivly defined set $\nu f$. This is what happens in the example in What is coinduction? showing forall n, Infinite (from n). Here, $f$ is closure under the constructors of Infinite (not of colist!) and $P$ is the set of all terms of the form from n for some n.