Abstract

We present a strategy for encoding a dependently-typed inductive language originally designed for a proof assistant within e-graphs. This language necessitates automated reasoning about distributivity and associativity. We encode our domain-specific language into egglog. Since egglog currently lacks proof extraction, we discuss strategies for building proof trees within egglog and approaches to implementing proof extraction in Metatheory.jl. Once extraction exists, we plan on interfacing with Coq to automate proof generation and checking. Having such a tool would drastically reduce the overhead in using our Coq library and enable reasoning about distributive and associative structures more broadly.

EGRAPHS’24 program