Defining and reasoning about partial (co)recursive functions in Lean
Horatiu Cheval
Authors: Horatiu Cheval, David Nowak and Vlad Rusu
While partial recursive functions are ubiquitous in programming,
proving results about their behavior using dependently typed proof assistants
like Coq or Lean is not straightforward, as they typically require the totality of all functions.
In this talk, we present a new approach for defining and reasoning about
potentially non-terminating functions in such systems, and a work-in-progress formalization
of these methods in the Lean theorem prover.
Our framework, which is based on domain theory,
allows one to embed such partial functions and constructs like while loops into proof assistants,
maintaining one’s ability to write proofs about them.
At the same time, we introduce a domain-theoretical representation of coinductive types
and partial corecursive functions.
This, together with convenient automations, provides an extension to Lean, whose native theory does
not include such notions.
Furthermore, our representation allows one to also write corecursive functions
that would normally not be accepted even in systems with built-in coinductives, like Coq,
as they would violate a required guardedness condition
(like the mirror function on infinitely deep trees),
or they would need to be partial (like the filter function on streams).
Bibliography
- Horac{t}iu Cheval, David Nowak, Vlad Rusu, Formal Definitions and Proofs for Partial (Co)Recursive Functions, https://inria.hal.science/hal-04360660 (2023).