This semester Benjamin Pierce gave a course on Advanced Coq Martial Arts based on Adam Chlipala’s CPDT book. The course was very interactive, with the students giving most of the lectures and being in charge of creating the exercises. Since I wanted to know more about coinduction I taught the coinduction lectures and learned a lot in the process. One of the results of these lectures is a new set of materials for teaching coinduction in Coq:

These materials are based on Adam’s book chapter, Giménez and Castéran’s tutorial, and Xavier Leroy and Herve Grall’s development on coinductive operational semantics. I’ve tried my best to explain things better and to add good exercises.

Another result is a new Coq tactic that allows for aggressive automation of coinductive proofs. Most of the easy proofs now take the form `coind using coind_principle; crush`.

**Update 2012-12-25: **

Here is the way I propose to marry co-induction and aggressive automation in Coq in these teaching materials. It’s actually all very simple. The primitive way of doing co-inductive proofs in Coq is by applying the `cofix` tactic directly. The guardedness check needed by cofix prevents effective automation. This problem is, however, not specific to co-induction: exactly the same problem appears when one uses `fix` directly in inductive proofs. Thus one very rarely uses `fix` directly in proofs. Instead, most often one proves lemmas encoding general *induction principles* (usually with lots of help from Coq) and then simply applies these principles with a bit of help from the `induction` tactic. What I propose is to apply this workflow that works very well for induction also to co-induction.

So instead of building proof terms directly with `cofix` one only uses `cofix` to define general *co-induction principles*. The co-induction principle for a co-inductive n-ary predicate P has the form:

forall R,

(forall x1 ... xn, R x1 ... xn -> P_gen R x1 ... xn) ->

forall x1 ... xn, R x1 ... xn -> P x1 ... xn

Where the predicate R seems very much related to the bisimulation proof technique and has the same type as P. The predicate “P_gen R” above is a variant of P where the recursive calls to P were replaced with calls to R.

Once one has proven such a general co-induction principle (and it’s usually very simple … my hope is that it can be fully automated as it is done for most induction principles) one can use it to write automated proofs by co-induction. The only remaining pain is that one has to manually choose an R whenever instantiating the co-induction principle. Here is where the `coind` tactic comes into play: it automatically instantiates R based on the syntactic shape of the goal (more details of how this works at the end of CoindStart

… it’s actually quite simple). The `coind` tactic doesn’t always choose “the right R”, but one can always strengthen the co-induction hypothesis in these cases. Again, things work very similar to induction, where the only way to strengthen the induction hypothesis is by changing the statement to be shown (not by fiddling with some R).

Just discovered (from one of the authors) that the co-datatype package for Isabelle uses the same simple idea to automate coinduction proofs. I’m flattered 🙂

[1] J.C. Blanchette, J. Hölzl, A. Lochbihler, L. Panny, A. Popescu, D. Traytel

Truly Modular (Co)datatypes for Isabelle/HOL, ITP 2014,

http://people.inf.ethz.ch/trayteld/papers/itp14-codata_impl/codata_impl.pdf