Bridging Syntax and Semantics of Lean Expressions in E-Graphs
Marcus Rossel, Andrés Goens
TL;DR
The paper tackles bridging Lean's context-dependent expression semantics with the syntactic framework of e-graphs to enable automated equational reasoning via equality saturation. It presents an early prototype that encodes Lean terms in an egg-based e-graph and provides a tactic, egg[eqn_1,...], to generate rewrite sequences while preserving Lean's soundness via the kernel. Core contributions include dynamic rewrites for $eta$- and $\,eta$-reductions, normalization of let-expressions, erasure of proofs to model proof irrelevance, and a substitution-on-e-classes approach with cycle-breaking to implement substitutions within e-graphs. The work discusses unsoundness caveats but demonstrates soundness through Lean's proof checking and reports preliminary tests indicating promising improvements for automated equational reasoning in Lean.
Abstract
Interactive theorem provers, like Isabelle/HOL, Coq and Lean, have expressive languages that allow the formalization of general mathematical objects and proofs. In this context, an important goal is to reduce the time and effort needed to prove theorems. A significant means of achieving this is by improving proof automation. We have implemented an early prototype of proof automation for equational reasoning in Lean by using equality saturation. To achieve this, we need to bridge the gap between Lean's expression semantics and the syntactically driven e-graphs in equality saturation. This involves handling bound variables, implicit typing, as well as Lean's definitional equality, which is more general than syntactic equality and involves notions like $α$-equivalence, $β$-reduction, and $η$-reduction. In this extended abstract, we highlight how we attempt to bridge this gap, and which challenges remain to be solved. Notably, while our techniques are partially unsound, the resulting proof automation remains sound by virtue of Lean's proof checking.