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.