Synthesizing Implication Lemmas for Interactive Theorem Proving
summary
Implements a Rocq tactic called dilemma that synthesizes implication lemmas of the form P1 ∧ … ∧ Pn ⇒ Q by data-driven invariant inference over sample valuations, isolating minimal assumption sets and synthesizing weaker guards (e.g., discovering X ∈ L to justify a sorting lemma). Evaluated on 226 locations from the Verified Functional Algorithms textbook and prior benchmarks, it finds exact or similarly useful lemmas in 43% of cases and ships reproducible artifacts.
AI-written summary · about
chapters (11)
- 0:00Lemmas and theorem proving
- 1:03Verifying selection sort
- 3:47Directed lemma synthesis
- 5:51Targeting implication lemmas
- 7:37Minimal assumptions for lemmas
- 9:24Data-driven assumption synthesis
- 10:07Weakening assumptions
- 11:32Two-pass lemma synthesis
- 11:53Future work and limitations
- 12:36Summary
- 13:00Q&A
related talks
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
20mOn Extending Incorrectness Logic with Backwards Reasoning
01h 05mVerifying Infinitely Many Programs at Once
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
27mUnrealizability Logic
26mUnification for Subformula Linking under Quantifiers
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better
23mSpecifying and Verifying Future Conditions