9
$\begingroup$

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.

$\endgroup$
3

2 Answers 2

7
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ Concerning sized types, can you comment on how that inconsistency snuck into Agda and stayed for so many years? Even after sized-types have been made "unsafe" by fiat, how do we know that there are no more inconsistencies in the "safe" part? And does Agda's "safe" simply mean "we have not found an inconsistency yet"? Thanks. $\endgroup$
    – user21820
    Mar 25 at 15:18
  • $\begingroup$ Andreas Abel would know more, but my understanding is that sized types are proved to be consistent for non-dependent types and dependent types without propositional equality. But adding equality breaks things. Safe for any proof assistant always means "we haven't found an inconsistency yet." There are models of proof assistants that are proven to be consistent, but they're generally more limited than the full languages, and even then, there can be bugs so that proof assistants don't fully match the model. $\endgroup$ Mar 25 at 22:12
  • $\begingroup$ Thanks for your helpful response! Has there been any discussion online about why people at first thought adding equality would be okay in the presence of sized types? And do you have a rough idea of what fraction of formalized mathematics in Agda is done within a fragment that has been proven consistent relative to ZFC (assuming no bugs)? $\endgroup$
    – user21820
    Mar 26 at 3:53
3
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.