I’m attempting to dip my toes into Coq’s coinduction facilities, and I have no idea where to start. While this topic is ostensibly about the conaturals, I welcome any and all suggestions for beginner-level tutorials on the subject of coinduction in Coq.
Consider the following development:
CoInductive conat: Set :=
| coz: conat
| cosucc: conat -> conat.
CoFixpoint omega: conat := cosucc omega.
Goal omega = cosucc omega.
Proof.
Fail reflexivity.
Abort.
Goal coz <> omega.
Proof.
intro H.
inversion H. (* does not accomplish any progress *)
Abort.
In Certified Programming with Dependent Types Adam Chlipala suggests the definition of an elaborate identity function (which he calls frob) with an associated congruence lemma (frob_eq), and using the later to rewrite the term. Is this truly the most straightforward way to proceed?
Definition frob (n: conat): conat :=
match n with
| coz => coz
| cosucc n => cosucc n
end.
Lemma frob_eq (n: conat): n = frob n.
Proof.
intros.
destruct n; reflexivity.
Qed.
Goal omega = cosucc omega.
Proof.
replace (omega = cosucc omega) with (frob omega = cosucc omega).
- reflexivity.
- rewrite <- frob_eq. reflexivity.
Qed.
Goal coz <> omega.
Proof.
rewrite (frob_eq omega).
simpl.
intro H; inversion H.
Qed.
Coinductive types have changed very little since their inception in Coq, and the advice in Chlipala’s book is still the most straightforward way to get started. In particular, your sample of code looks like a fine application of it. The next limitation you’ll run into, and that CPDT does cover in depth, is that more interesting equations are not provable, so you will need to give up = and define a custom equivalence relation (bisimilarity) on conaturals as a substitute (stream_eq in CPDT).
Shortly after that, I would strongly recommend the paco library to define coinductive predicates such as bisimilarity. This replaces CoInductive declarations in Prop, which are really bad. (You will still use Coinductive in Type, which are less bad.) The library comes with a tutorial (see its README).
That’s pretty much it to get a working understanding of coinductive types in Coq.
A few more remarks beyond that:
There is another reasonable stance: “don’t use coinductive types”. They are a pain to work with, and they’re not essential to the expressiveness of Coq, so it may be simpler to consider alternative encodings that rely on better known principles. For example, conaturals can also be modelled as monotonic functions nat -> bool or (non-constructively) as “naturals plus infinity”, option nat. The counterpoint is that sometimes coinductives might really be the “most natural” way to do something, particularly if you care about how things compute (e.g., for dependently typed programming, for automation, or for extraction).
Although frob_eq provides the easiest way to reason about coinductive types, it is definitely an awkward solution. It’s possible to phrase theorems so it’s not ever needed, but concrete advice on how to actually achieve that is hard to come by. One requirement at least is to avoid propositions indexed by values of coinductive types, a rule which stream_eq (in the CPDT chapter) blatantly breaks. A better behaved variant is the following:
(* This is a _parameterized_ proposition, rather than _indexed_. *)
CoInductive stream_eq (s1 s2 : stream) : Prop :=
| Stream_eq : hd s1 = hd s2 -> stream_eq (tl s1) (tl s2) -> stream_eq s1 s2.
(This also implies that = on streams is a bad idea.)
(This is actually trickier to do for conaturals, and another reason to use paco.)
Another idea to get acquainted with is the distinction between “data” and “codata”, which roughly correspond to inductive vs coinductive types (the distinction is really also relevant to nonrecursive types). Some intuitive patterns for reasoning about data end up being counterproductive when applied to codata. Two papers to read on the topic are Copatterns and Codata in action.