Comparison between proof assistants for coinductive structures and proofs

Question

I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction?

My motivation is that I'd like to formalize some proofs, basically about coinductive λ-calculus (thus involving binders, reductions, quotient up to renaming of bound variables, etc. but also nested inductive and coinductive structures). However, I ask the question imprecisely since I didn't find many general answers on the web.

The proof assistants I am considering are: Coq, Lean and Agda. These are the main three that I'd like to compare, but I'm open to any suggestions.

Answer 1

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet.

• Coq: Coinduction is based on a guardedness condition: every co-recursive call must be guarded by a constructor of the co-inductive type in order to ensure productivity. This is the fairly conventional way to support co-induction, and my understanding is that there are is fairly good tactic support for coinduction.

• Idris You didn't ask for this, but it's worth mentioning that co-induction is roughly similar in Idris as it is in Coq, albeit without the tactics. Productivity is ensured with a guardedness condition. One interesting thing is that Idris separates Lazy from Coinductive, so if all you care about is the order of evaluation, and not co-inductive proofs, laziness is an option there.

• Agda Agda has four different ways to do co-induction.

  Guardedness: Agda allows for co-induction based on a conventional "guardedness" check like Coq and Idris. However, one nice thing about co-induction in Agda is that you can use co-patterns. This crystallizes the idea that, as inductive types are recursive sum types, co-inductive types are dually co-recursive product types. When consuming an inductive type, you have to handle a pattern for each constructor. When producing a co-inductive type, you need to handle the pattern for each destructor i.e. each field of a record.

  Musical notation: This is an "old" way of doing things in Agda. It marks delayed computations with a special $\infty$ modality, and uses $\flat$ and $\sharp$ operators to go between $\infty T$ and $T$. It's not recommended anymore.

  Sized types: These provide an alternative to the guardedness condition, where instead of ensuring that each co-recursive call is guarded by a constructor, it ensures that each co-recursive call has a decreasing size argument. This pairs nicely with co-patterns, but unfortunately, there seem to be some consistency issues

  Guarded cubical Agda: This is, in my opinion, the most promising but least developed (and documented) option for co-induction in Agda. The idea here is that there is a "later" modality $\triangleright$ where values in $\triangleright T$ are members of $T$ that are only available in the future. Atkey and McBride show how this can be used to do co-induction. There's a guarded fixed-point operator with the type $(\triangleright T \to T) \to T$, which is very nice for modelling i.e. non-positive datatypes. The nice thing about this is that the guarded modality plays very nicely with cubical equality, since you get the extensional equalities you need for guarded recursion to work out.

Answer 2

I do not know much about other proof assistants, but as for Coq I can say that there are quite some resources around that you might benefit from. Here is a starting point.

However, the current situation is not perfect. As explained in details in this question, the original – so-called positive – presentation of coinductive types in Coq poses theoretical issues (it breaks subject reduction). There are at least two concurrent solutions: one is to avoid this positive presentation altogether in favor of a negative one, see the caveat in the reference manual; the other is to endorse a new criterion restricting the positive presentation. Both solutions however involve trade-offs that you might have to consider for your project.