Synthesizing Implication Lemmas for Interactive Theorem Proving

Explore a conference presentation that introduces a novel technique for automatically generating implication lemmas in interactive theorem proving systems. Learn about the challenges users face when identifying necessary helper lemmas to complete formal proofs, particularly those defining key inductive invariants. Discover how the proposed data-driven approach employs invariant inference to explore strengthenings of proof states based on sample valuations of current goals and assumptions. Examine the implementation of this technique in the "dilemma" tactic for the Rocq theorem prover and understand how it addresses the limited support for synthesizing implications of the form P1 ∧ ⋯ ∧ Pn ⇒ Q in existing lemma synthesis approaches. Review the effectiveness demonstration through applications to proofs from the Verified Functional Algorithms textbook and prior benchmark suites, gaining insights into how this tool can reduce the burden on interactive theorem prover users by automatically identifying crucial helper lemmas needed for proof completion.