Learning/Teaching Coinduction with Coq

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).

Advertisements

One Response to Learning/Teaching Coinduction with Coq

  1. hritcu says:

    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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: