Towards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
summary
Presents a Lean tactic that translates theorems into conditional rewrite rules, runs equality saturation with egg on an e-graphs representation, and reconstructs a checked proof term in Lean; handles conditional theorems by adding multi-pattern “fact P” nodes and running type-class synthesis during rule application. Implementation solves four case studies (binomial-chain example, functional-array rewrite suite from the paper formalized in Agda) but can explode e-graphs, surface leftover proof obligations, and sometimes fail when conditions aren’t discoverable.
AI-written summary · about
chapters (11)
- 0:00Pen-and-paper equational reasoning intro
- 1:50Connecting Lean and egg
- 3:15Egraphs and equality saturation
- 6:24Challenges in theorem translation
- 9:14Conditional theorems in rules
- 12:44Type class synthesis in rules
- 14:52Practical examples and evaluation
- 16:16Case study: functional arrays
- 17:22Related work comparison
- 18:23Implementation and conclusion
- 18:43Q&A
related talks
13mA Drag-and-Drop Proof Tactic
19mQED in Context: An Observation Study of Proof Assistant Users
22mAesop: White-Box Best-First Proof Search for Lean
15mAdaptable Traces for Program Explanations
26mIntegrating graphical proofs in Coq
21mLive Verification in an Interactive Proof Assistant
29mType Inference Techniques: Implementation and Formalization, Better Together
13mProgramming with a Read-Eval-Synth Loop