How to make ad hoc proof automation less ad hoc
summary
Coq proof automation becomes an instance of ad hoc polymorphism: dependent overloaded theorem records encode both a heap shape and a proof, and Coq’s unification engine uses canonical instances to dispatch and recursively build proofs. The implementation embeds a small logic-programming unification search inside type inference so applying an indom lemma automatically rewrites associative/commutative heaps and constructs the needed subproofs, eliminating manual rewrite boilerplate; the method works on real Coq developments.
AI-written summary · about
chapters (9)
- 0:00Start
- 5:15Ad Hoc Polymorphism
- 6:27Lemma Overloading
- 11:56Overview of Overloading
- 12:33Type Classes
- 15:12Implicit Arguments
- 24:56Implement a Recursion
- 29:15Singleton Heaps
- 33:26Conclusions
related talks
01h 34mFormal Logic Undressed
01h 00mUnconference Coq
20mAll Your Base Are Belong to Us: Sort Polymorphism for Proof Assistants
30mConvenient Algebraic Programming with Coercive Subtyping
35mUsing the Design Recipe in Theory of Computation
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
42mLive-Coding Mathematics Your First Clojure Proof
57mApplied category theory and abstract algebra