Hey everyone, I keep seeing the same CoFixpoint pain points come up in various threads so I figured I'd write up a megathread with all the tricks I've accumulated over about two years of fighting Coq's coinduction checker. Consider this my battle diary 🐱⚔️

§1 — The Guardedness Condition: What It Actually Means

The fundamental rule: every corecursive call must be guarded by at least one constructor of the coinductive type. CoFixpoint is lazy — Coq will only reduce it when it appears as the scrutinee of a match. This is intentional:

Key insight: productivity is undecidable, so Coq uses a conservative syntactic criterion. This means many perfectly productive definitions get rejected. Don't rage-quit — there are workarounds.

§2 — The Unfold Trick

The single most useful trick: when Coq can't see through a CoFixpoint, force it with an eta-expand identity function (often called frob or unfold_stream):

This works because Coq reduces a cofixpoint only when it is the scrutinee of a match statement. The force trick manufactures that match.

§3 — Defining CoInductive Predicates Correctly

For coinductive propositions (as opposed to data), you use CoInductive with a proposition-valued type. The bisimilarity predicate is the classic example:

More tomorrow! This post is already getting long ^^;

Great thread already! One thing that trips me up constantly: why does Qed fail after a proof that seemed to work?

The painful thing about cofix is that the guardedness check is not run during tactic mode — it only runs at Qed. So you can happily build a "proof" and then watch it explode at the end:

The lesson: always double-check that every use of the coinduction hypothesis is under a constructor. If you use CIH "bare" (without first applying a constructor), Coq's kernel will reject it.

Yes exactly! And the reason is subtle: Coq reduces a cofixpoint only when it is the scrutinee of a match statement. So if you have a helper lemma that's opaque (Qed-closed), the guardedness checker can't peek inside it and will fail:

Rule of thumb: any auxiliary lemma used inside a cofix proof should be Defined not Qed, or it needs to be definitionally transparent. Otherwise, the guard checker hits an opaque wall and rejects the whole proof.

Alternatively, avoid the rewrite entirely and use destruct or case to force unfolding directly.

Bookmarking this thread so hard. Can you cover negative vs positive coinductive types? I read in the Coq manual that as of 8.9 they recommend negative coinductives but I'm not clear on why.

Great question! §4 — Positive vs Negative Coinductive Types

Positive coinductives are the traditional constructor-based style you see in most tutorials. But they have a dirty secret: using them can break subject reduction because of issues with dependent pattern-matching and η-equality.

Negative coinductives are defined as CoInductive record types using primitive projections. The Coq manual recommends these since 8.9. The pattern looks like:

The negative style has copattern-based syntax similar to Agda, and preserves subject reduction. You define values by specifying all projections, rather than applying a constructor. The main downside is that some standard tactics work slightly differently.

A key technical issue with positive coinductives: you can derive a term of type evalN infS = infS, but Coq can't reduce it to eq_refl because it can only reduce cofixpoints under a match, not in arbitrary type positions. This inconsistency is why negative coinductives exist.

Speaking of automation: the guardedness check and Coq's automation do not play well together. If you try to use auto or eauto inside a cofix proof, it'll likely break guardedness because these tactics don't know or care about the guard condition. This is a real bottleneck for large coinductive proofs.

For instance: if you use rewrite and it introduces an application of a Setoid library lemma (which is Qed-opaque), the guardedness checker can't inspect that lemma's proof and the whole thing fails.

Notice the careful use of pattern ... at 1 to control exactly which occurrence gets rewritten. This avoids introducing extra proof terms that confuse the guard checker.

OK so this brings me to a question I've been avoiding asking: is there a way to do coinductive proofs that doesn't involve fighting the guard checker at every step? Something more ergonomic?

I've heard people mention paco but I don't really understand how it works.

Oh yes, this is the big one! §5 — Parameterized Coinduction and Paco

The core problem with cofix is that it uses a syntactic guardedness criterion. This means automation tactics have no way to reason about whether a proof is guarded. The result: you can't use eauto, omega, or most other Coq automation inside cofix proofs without breaking things.

Enter parameterized coinduction, introduced by Hur, Neis, Dreyer, and Vafeiadis (POPL 2013). The key idea:

The Paco library implements this for Coq. Instead of writing:

You define a monotone functor for your predicate, and use pcofix:

The magic: pcofix replaces the syntactic guard check with a semantic one, baked into the library's types. You can't "accidentally" use CIH in an unguarded position because the type system prevents it. All of Coq's automation works normally inside pcofix proofs!

Can you explain the accumulation principle in Paco a bit more? I get that there's a relation parameter r, but I'm not clear on when/how you "add things to r".

§6 — The Accumulation Principle

The technical foundation (due to Hur et al.) is this: for a monotone function f on a complete lattice, define:

In practice, this means: if you're coinductively proving P and during the proof you discover that some auxiliary fact Q is also true by coinduction, you can accumulate Q into your coinduction hypothesis and use it freely thereafter. In contrast, with raw cofix, you'd need separate nested cofix proofs (which are extremely fragile).

The generalized version (gpaco) from Zakowski, He, Hur, Zdancewic (CPP 2020) extends this further with "up-to-tau" reasoning and more powerful closure operators, which is essential for reasoning about interaction trees in compiler verification work.

This is SO much clearer than the paper tbh. One more thing — the lifting issue? I've seen warnings about "lift the continuation" in some blog posts about CoFixpoint and interaction trees. What's going on there?

§7 — The Parameter Lifting Trick

This is a subtle but important one! When defining a CoFixpoint that takes a function parameter (like a continuation k), the guardedness checker can't infer that k is constant across corecursive calls. So this fails:

The fix is to lift the parameter outside the cofixpoint using a wrapper, so the corecursive part has no extra arguments:

The intuition: inside a Section, k is a global constant from Coq's perspective, not a varying argument. The guard checker is happy because it can see the corecursive call is on a structurally "smaller" part with the same fixed k.

Adding to the Section trick: this is also why the interaction trees coq library uses Section blocks liberally when defining monadic bind over potentially infinite computations. The continuation in bind has to be lifted outside the cofixpoint or the whole thing explodes.

Here's the "bind for lazy computations" issue in minimal form:

Wait, does Paco install cleanly with current Coq versions? Last time I tried I got some opam dependency hell 😿

Paco installs fine via opam from the coq-released repo:

It's compatible with Coq 8.13–8.15 as of v4.1.2. For newer Coq (8.16+) you may want to check the GitHub repo for the latest. The coq-community maintained version by Damien Pous (coq-coinduction) is an alternative that uses the companion approach ("Coinduction All The Way Up", LICS 2016) instead — it's even more powerful but has a steeper learning curve.

§8 — The Companion Approach (brief)

Pous's companion theory says: for a monotone f, the "companion" t is the greatest compatible function below f. Any compatible function is subsumed by the companion, and the companion is idempotent (tt = t). This lets you plug in "up-to" techniques compositionally:

One pattern I use constantly and would add to this list: bisimulation up-to (without a library). When doing a manual cofix bisimulation proof, you often want to "close up to" some equivalence. The trick is to maintain an explicit relation that you carry around:

This is the "bisimulation as a greatest fixed point" argument and it's much cleaner than trying to do coinduction on the goal directly.

Amazing thread. Should we make a wiki page for this? I'd love a summary table of all the techniques with pros/cons. Maybe something like:

• Raw cofix — builtin, no deps, terrible for automation
• cofix + Defined lemmas — solves opacity issues, still manual
• Paco (snu-sf) — semantic guardedness, great for predicates, POPL 2013
• gpaco (CPP 2020) — generalized Paco, handles weak bisimulation
• coq-coinduction (Pous) — companion-based, compositional up-to, LICS 2016
• Negative coinductives — use for data, avoids subject reduction issues

FixpointFeline you should write this up as a proper CGPA wiki article honestly uwu

Great idea Cleo! One more tip before I write the wiki page: mutual CoFixpoints. You can define them with with, same as with Fixpoint:

Mutual coinduction in proof mode is trickier — you typically need to formulate it as a single predicate about a pair, or use Paco's pcofix2 / pcofix3 for multivariate relations. The guardedness checker for mutual coinduction checks that each corecursive definition is guarded w.r.t. all others in the mutual block.

Wiki article is in progress, will post link when done! 🐱

tl;dr resources for anyone finding this thread later:

• Adam Chlipala's CPDT, Chapter "Coinductive" — free online, best intro
• Hur et al., POPL 2013 — "The Power of Parameterization in Coinductive Proof"
• Paco library — github.com/snu-sf/paco
• coq-coinduction — github.com/damien-pous/coinduction
• Breitner's blog — "Coinduction in Coq and Isabelle" (great for comparison)
• The Coq reference manual section on coinductive types (Coq 8.9+ for negative coinductives)

This thread deserves a sticky. /cc mods 👀

One thing I'll add: if you're coming from Agda, be warned that Agda's coinduction framework differs significantly from Coq's. Agda uses copatterns and the ∞ type constructor, which sidestep a lot of these issues by design. Coq's negative coinductives (with primitive projections) get closer to Agda's approach but it's still not as smooth.

Also: Agda has a productivity checker that goes beyond syntactic guardedness in some cases. Don't assume your Agda intuitions transfer directly to Coq! 🐾