Coinductive predicates in Lean

Abstract: Coinduction, the mathematical dual of induction, is a fundamental proof principle in computer science, essential for reasoning about infinite structures, concurrent systems, and compiler correctness. While full coinductive data support in proof assistants typically requires foundational support and careful considerations, such as syntactic guardedness checking, focusing on the simpler case of coinductive predicates can recover many important use cases. This is sufficient for defining concepts like bisimulations and other coinductive relations crucial for program verification.

This talk presents our design and implementation of coinductive predicates in Lean 4. Our approach leverages lattice theory and the impredicativity of Lean's propositional universe to encode coinductive predicates and their proof principles directly within Lean's existing type theory, no kernel extensions required. Our implementation supports mutual coinduction, including mixed coinductive and inductive definitions. The talk will also touch on supporting syntax similar to the one for usual inductive types and compiling such definitions to monotone maps.

Joint work with Joachim Breitner (Lean FRO, Germany).

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( video )

Lean Together 2026