Bridging Syntax and Semantics of Lean Expressions in E-Graphs

TL;DR

This paper presents an approach to improve proof automation in Lean by bridging the gap between its expression semantics and the syntactic structure of e-graphs, addressing challenges like bound variables and definitional equality.

Contribution

We introduce a method to connect Lean's semantic expressions with e-graph-based equality saturation, enabling better proof automation despite partial unsoundness.

Findings

Prototype implementation demonstrates feasibility

Handling of bound variables and definitional equality is achieved

Partial unsoundness is acceptable due to Lean's proof checking

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 $\alpha$-equivalence, $\beta$-reduction, and $\eta$-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.