Synthesizing Implication Lemmas for Interactive Theorem Proving
Ana Brendel, Aishwarya Sivaraman, Todd D. Millstein · Proceedings of the ACM on Programming Languages · 2025
Interactive theorem provers (ITP) enable programmers to formally verify properties of their software systems. One burden for users of ITPs is identifying the necessary helper lemmas to complete a proof, for example those that define key inductive invariants. Existing approaches to lemma synthesis for ITPs have limited, if any, support for synthesizing implications: lemmas of the form P 1 ∧ ⋅⋅⋅ ∧ P n ⇒ Q . In this paper, we propose a technique and associated tool for synthesizing useful implication lemmas. Our approach employs a form of data-driven invariant inference to explore strengthenings of the current proof state, based on sample valuations of the current goal and assumptions. We have implemented our approach in a Rocq tactic called dilemma . We demonstrate its effectiveness in synthesizing necessary helper lemmas for proofs from the Verified Functional Algorithms textbook as well as from prior benchmark suites for lemma synthesis.