Egg: An Equality Saturation Tactic in Lean

Abstract: Rewriting is an extremely common proof task supported by efficient and versatile tactics like $\texttt{rw}$ and $\texttt{simp}$. These tactics are, however, limiting in that users need to either provide an explicit order and direction of rewrites, or rely on a fixed simplification direction. In our talk, we present a new (work in progress) tactic for rewriting using equality saturation. This approach allows us to tackle goals which are infeasible for $\texttt{simp}$ without requiring the details needed for $\texttt{rw}$.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2025

Series comments: Most of the talks from the conference are available on YouTube: www.youtube.com/watch?v=ZPPDktjL1Lw&list=PLlF-CfQhukNlzXdQvu1SVt9vcD4--fLlg