Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs

Explore a 22-minute video presentation from the EGRAPHS 2024 workshop that delves into automated proof generation for associative and distributive rewriting using e-graphs. Learn about a novel strategy for encoding a dependently-typed inductive language within e-graphs, originally designed for proof assistants. Discover how the presenters tackle automated reasoning about distributivity and associativity by encoding their domain-specific language into egglog. Gain insights into the challenges of proof extraction in egglog and the proposed strategies for building proof trees and implementing extraction in Metatheory.jl. Understand the future plans to interface with Coq for automating proof generation and checking, potentially reducing the overhead in using Coq libraries and enabling broader reasoning about distributive and associative structures.

[EGRAPHS24] Automated Proof Generation for Associative and Distributive Rewriting with E-Graphs