In domains from pure math to program verification, arguably the most popular interactive proof assistants of today are all based on dependent type theory. They expose different tactic languages to guide automated generation of proofs in core logics. Their proof engines are the interface that underlies tactics: keeping track of open goals, detecting proof errors incrementally, and generating proof terms if desired. Use cases like classic math theorems and metatheory of core calculi have in common that intermediate goals never grow especially large, compared to use cases like verifying imperative programs that are thousands of lines long -- the latter may produce proof goals with e.g. one free variable per assignment statement and one hypothesis per free variable explaining what we know about its value, and it is not practical instead to inline those free variables with their defining equations, as we lose sharing and grow goals exponentially. Therefore, if proof assistants are to break into the mainstream of routinely verifying important, large programs, core operations of proof engines must exhibit good asymptotics (effectively linear in goal size), which is not the case for the popular type-theoretic proof assistants today.
We propose a new style of proof engine, optimized for highly automated scripted proofs, that remedies this flaw. Our new engine is based on lambda-DAGs, a technique for representing sets of terms in functional languages with high representation sharing. We evaluate this style with a prototype freestanding implementation called MEngine that outputs Rocq proof terms, demonstrating enormous speedups in important cases motivated by verifying large programs.