Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs
summary
Encodes a dependently typed DSL for symmetric monoidal categories and the ZX calculus into egglog by computing dependent-type arguments as functions and emitting partial composition checks that reject invalid diagrams. An automatic lemma translator produces rewrites with associativity and distributivity guards; search solves real library structural rewrites in <0.5s, replacing about 25% of repetitive code and turning ~3 minutes of manual proof work into instant rewrites. Plans target egglog proof extraction via Metatheory.jl and Coq.
AI-written summary · about
chapters (12)
- 0:00Problem and motivation
- 2:53E-graphs with COQ
- 6:29Structural rewrites in COQ
- 9:01ZX calculus to E-graphs
- 12:57Dependent types in E-graphs
- 14:01Avoiding E-graph blowup
- 16:27Structural rewrite example
- 17:51Proof production in E-graphs
- 18:32Limitations of E-graph proofs
- 20:00Future work and integration
- 20:42Summary
- 21:04Q&A
related talks
17mBetter Together: Unifying Datalog and Equality Saturation
21mCompositional pre-processing for automated reasoning in dependent type theory
30megg: Fast and Extensible Equality Saturation
22mFrom Rewriting to Fixpoints: Solving Recursive Equations with E-Graphs
14mPredicate E-Graphs with Symbolic Conditional Rewriting
27mAn Equations Tutorial
32mExperience Report: Graph Rewriting with Lexical Effect Handlers
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq