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).
Bio:
Wojciech Różowski is a Research Software Engineer at Lean FRO, where he works on the development of the Lean theorem prover. His research interests include automated reasoning, formal semantics, and program verification. He obtained his PhD at University College London under the supervision of Alexandra Silva, as a member of the Programming Principles, Logic and Verification Group.
