Medium-scale automation for proof assistants
summary
Shows that medium-scale automation produces concise, convincing, robust formal proofs for relation algebra and monoidal category theorems by combining certified decision procedures, rewriting modulo, and notation inference. Implements an m_rewrite tactic plus a certified KA decision procedure (reflection) to solve regular-expression/relations goals, and a string-diagram editor that emits proof script fragments and an MCAT/hcat tactic to discharge diagram equalities. Examples: transitive-relation composition becomes a few rewrites; composing monads reduces to four pattern rewrites. Tools work end-to-end but sometimes need small manual lemma tweaks.
AI-written summary · about
chapters (6)
- 0:00Automation in proof assistants
- 1:24Convincing and reusable proofs
- 9:57Case study: Relations and linear algebra
- 28:25Case study: Monads and string diagrams
- 54:01Robust automation principles
- 1:03:29Q&A
related talks
22mA diagram editor to mechanize categorical proofs
26mIntegrating graphical proofs in Coq
13mA Drag-and-Drop Proof Tactic
07h 18mFull Workshop
22mTowards general white-box automation: a typeclass-guided context cleaner
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
21mEnhancing Proof Stability
29mType Inference Techniques: Implementation and Formalization, Better Together