Bridging Syntax and Semantics of Lean Expressions in E-Graphs
summary
Prototype proof automation encodes Lean expressions into egg and uses equality saturation (egg backend) to synthesize explanations that Lean then checks, bridging Lean’s definitional equality (α/β/η/delta) and syntactic e-graphs. Techniques include pregenerated equations for type-class reductions, normalizing/eliminating lets, and runtime dynamic rewrites to perform β/η reductions and to reject invalid binder matches; de Bruijn indices are used and slotted e-graphs are evaluated as an alternative. The prototype runs on real list-reverse proofs, reduces tedious rewrite sequences to a few lemmas, and is available as lean-egg on GitHub.
AI-written summary · about
chapters (11)
- 0:00Bridging Lean and e-graphs
- 2:03Motivation for theorem provers
- 4:50Tediousness in Lean proofs
- 7:19Equality saturation tactics
- 9:47Encoding Lean expressions
- 12:37Definitional equality in Lean
- 17:42Definitional vs syntactic equality
- 19:30Binder problems in e-graphs
- 23:02Invalid rewrite matching
- 24:47Egg tactic for automation
- 26:11Conclusion and future
related talks
30megg: Fast and Extensible Equality Saturation
30mTrustworthy Formal Natural Language Specifications
17mBetter Together: Unifying Datalog and Equality Saturation
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
23mVersioned E-Graphs
15mEquality Saturation Theory Exploration à la Carte
27mLightweight Semantics Engineering with Redex