Core support for coinductive predicates

Stream: lean4

[Wojciech Różowski]

Hi folks!

The latest nightly (nightly-2025-10-08) contains now core support for inductive-like syntax for defining coinductive predicates.

Here is an example of an infinite transition in a relation:

variable (α : Type)
coinductive infSeq (r : α → α → Prop) : α → Prop where
  | step : r a b → infSeq r b → infSeq r a

Out of this, you automatically get the following coinduction proof principle:

infSeq.coinduct (α : Type) (r : α → α → Prop) (pred : α → Prop) (hyp : ∀ (x : α), pred x → ∃ b, r x b ∧ pred b)
  (x✝ : α) : pred x✝ → infSeq α r x✝

To access the coinduction proof principle for a predicate, just postfix its name with .coinduct
For each predicate you get generated all its constructors, as well as casesOn. For example, the constructor you get is:

infSeq.step (α : Type) (r : α → α → Prop) {a b : α} : r a b → infSeq α r b → infSeq α r a

The machinery also supports mutual blocks, as well as mixing inductive and coinductive predicate definitions:

mutual
  coinductive tick : Prop where
  | mk : ¬tock → tick

  inductive tock : Prop where
  | mk : ¬tick → tock
end

Here is an example of the mutual (co)induction proof principle.

mutual_induct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2 → False) (hyp_2 : (pred_1 → False) → pred_2) :
  (pred_1 → tick) ∧ (tock → pred_2)

Under the hood, everything relies on encoding things using lattice theory and checking monotonicity, while sharing a lot of internals with partial_fixpoint. I am super happy to share the details if you have any questions.

If you have any feedback about this feature or you are stuck with using it, I would be more than happy to hear it. Feel free to drop a DM to me at any point or simply reply to this thread.

[Shreyas Srinivas]

Hi Wojciech, I'd like to understand the details a bit more. This is a subject that comes up on the discord every now and then. Is there a write up somewhere that explains the internals?

[Wojciech Różowski]

Sadly, not yet! I am planning to sync at some point with @David Thrane Christiansen and add appropriate sections to the reference manual.

Essentially, the idea is as follows:
Out of a coinductive definition:

coinductive infSeq (r : α → α → Prop) : α → Prop where
  | step : r a b → infSeq r b → infSeq r a

we generate a "flat" inductive, that describes its one-step behaviour:

inductive infSeq (r : α → α → Prop) (infSeq._functor.call : α → Prop)  : α → Prop  :  α → Prop :
| step :   r a b → infSeq._functor.call b → infSeq._functor r infSeq._functor.call a

Such "flat" inductive valued in Prop can be equivalently rewritten to a following form:

def infSeq._functor.existential.{u_1} : {α : Sort u_1} → (α → α → Prop) → (α → Prop) → α → Prop :=
fun {α} r infSeq._functor.call a => ∃ b, r a b ∧ infSeq._functor.call b

Think of it as a disjunction of all constructors.

This definition is used to kick-off the partial_fixpoint machinery (for more details see the reference manual), but specialised to lattice theory. In fact, you can define (co)inductive predicates as a tail-recursive function and using inductive_fixpoint/coinductive_fixpoint termination hint.

Well-definedness of such definitions relies on monotonicity of the map extracted from the rules. We rely on a syntax driven tactic employed by partial_fixpoint and we have ready made monotonicity lemmas, that cover most of the typical examples. In fact, if your (co)inductive definitions are positive or if you mix induction and coinduction all inductive calls in coinductive definitions are in negative positions (and vice versa) then the tactic handles that immediately.

[Robin Arnez]

A few things I've noticed:

1. the implicitness for parameters is wrong (p and q should be implicit in inl):

coinductive MyOr (p q : Prop) : Prop where
  | inl (h : p)
  | inr (h : q)

/-- info: MyOr.inl (p q : Prop) (h : p) : MyOr p q -/
#guard_msgs in
#check MyOr.inl

2. the definitions are slightly verbose, e.g.:

coinductive Test : Prop where
  | thing

/--
info: def Test.thing : Test :=
Eq.mpr (id (congrArg (fun _a => _a) Test.functor_unfold)) (Test._functor.thing Test)
-/
#guard_msgs in
#print Test.thing -- could be `Eq.mpr Test.functor_unfold Test._functor.thing` (with `Test` implicit)

3. match doesn't work:

coinductive Simple (p : Prop) : Prop where
  | test (h : p)

def testMe (x : Simple p) : p :=
  match x with
  | .test _ h => h

4. The partial_fixpoint-based inductive command is often more powerful than the regular one but there doesn't seem to be a way to activate it without putting it into a mutual block with a coinductive:

-- mutual

inductive Simple (p : Prop) : Prop where -- only works when the rest is not commented out
  | test (h : (Simple p → p) → p)

-- coinductive Null (p : Prop) : Prop where

-- end

5. The "coinductive keyword can only be used to define predicates" error sometimes appears in the wrong place (take e.g. the previous example with coinductive Null (p : Prop) where instead, the error will appear on Simple).
6. The induction and coinduction principles use non-standard names (maybe use motive / motive_<n> and <constructor name> instead of pred_<n> and hyp_<n>).

The first two and last two seem to be pretty simple to fix while the third one probably requires some work (e.g. Eq.rec support for match?) and the fourth one requires some thought into what kind of syntax to use.

[Wojciech Różowski]

Thanks @Robin Arnez for such a detailed info.

1. I will look into implicitness of the arguments - to be frank with you I did not notice something like that was the case for inductives.
2. Hmm, I guess this is the matter of the metaprogramming code generating too verbose of a code.
3. Yes, indeed! Match statements are not supported yet. I know that in the near future @Joachim Breitner is planning to look into match compilation pipeline and allow it to be extensible. That's why I delayed working on it for now, and also wanted to see if people would really use match on coinductive predicates in practice.
4. Hmm, that is an interesting point. It is quite easy to allow users to elaborate inductives using the lattice-theoretic approach, but I did not anticipate the interest of users in such a feature. I guess it is nice that you can weaken positivity to monotonicity.
5. Yes, this is on purpose. From what I understand, for inductives, by default if you don't put that it is an arrow into Prop, it is implicitly living in Type. We wanted to follow the same convention and make it clear to the user, that you can only coinductively define things that live in Prop.
6. Fair enough, that is a good hint for the naming scheme.

[Niels Voss]

If core later chooses to add support for coinductive non-Prop types, will this be compatible with the coinductive predicate syntax and semantics? My understanding is that coinductive non-Prop types would currently suffer from a performance issue, but that the issue was fixable.

[Wojciech Różowski]

This is what I would expect. See (5) in my previous message. Precisely, in the situation when the inferred universe is Type u, some coinductive data package could be used, if one decided to implement it and have it in core.

[Niels Voss]

It's been a while since I used coinduction (and even then I hardly did anything with it) but assuming I'm not misremembering, didn't Rocq encounter problem because they supported coinductive types with multiple constructors directly (as opposed to only supporting coinductive records/structures)? Agda seems to call the former approach "Old Coinduction" (see https://agda.readthedocs.io/en/latest/language/coinduction.html#old-coinduction) which is not recommended for some reason?

[Wojciech Różowski]

Ah, I see. So from what I understand, this is related to the approach of adding coinduction to the underlying type theory/kernel. And indeed, Rocq and Agda had some issues with positive formulation of coinductive types via constructors and went for negative formulations via copatterns/destructors.

[Wojciech Różowski]

In our approach, which only applies to (arrows into) Prop, we simply rely on lattice theory and compile constructors to monotone map on lattices, which does not require any kernel extensions and is simply encoded.

[Wojciech Różowski]

From what I remember, in Agda/Rocq there is quite of subtlety of having eta conversions for coinductive types, which can make type checking non-terminating.

[Niels Voss]

I see (or at least I think I might). I'm just wondering if it could potentially be that if Lean chooses to add coinductive non-Prop types in the future, if we would only support coinductive records rather than coinductive types with custom constructors, and if this would mean that coinductive could only ever be used for Prop and that all other coinductive types would have to use costructure or something.

[Wojciech Różowski]

Okay, now I also see what you meant. In the hypothetical scenario, where Lean decides to extend its kernel with coinductive types, I would agree that copatterns/coinductive records approach might be the most reasonable syntax for specifying these and coinductive keyword in current form, would only make sense for those lattice-theoretic predicates.

[Wojciech Różowski]

On the other hand, I could envision someone extending the Qpf framework (which encodes coinductive data via constructions on quotients on polynomial functors) to be able to also handle indices and use it for coinductive data and have coinductive keyword to rely on it when dealing with things beyond predicates.

[Wojciech Różowski]

The reason we focused on predicates is that you can often get by with coinductive predicates only (i.e. you work with bisimulations rather than bisimilarity equivalence classes) and their encoding is quite simple and relies on lattice theory, rather than more involved things like qpf (mentioned earlier) or bnf (in the case of Isabelle).

[Niels Voss]

So if we never extend Lean's kernel (which we probably won't) and we implement coinduction in "userspace" using QPF, then the problems that Rocq and Agda encountered go away?

[Robin Arnez]

Oh for (5) I meant doing something like

    if let some i ← rs.findIdxM? (forallTelescopeReducing ·.type fun _ body => pure body.isProp) then
      throwErrorAt views[i]!.declId "`coinductive` keyword can only be used to define predicates"

rather than always targeting the first one

[Wojciech Różowski]

Ah sorry @Robin Arnez , thanks for hinting that!

[Wojciech Różowski]

Niels Voss said:

So if we never extend Lean's kernel (which we probably won't) and we implement coinduction in "userspace" using QPF, then the problems that Rocq and Agda encountered go away?

Yes, this is what I would expect. For example codata keyword in @Alex Keizer's reimplementation of qpf relies on positive formulation of codata via constructors.

[Alex Keizer]

Indeed, by doing coinductive data in "userspace", as you call it, we don't have to worry about introducing inconsistencies to the type theory, given we don't touch the type theory at all, so we can have positive coinduction without issue.