Practical and sound equality tests, automatically
summary
A tool called feqb synthesizes sound equality tests and correctness proofs for Coq inductive types used with the Mathematical Components library, handling very large constructor sets, dependent sigma types (e.g. bounded machine words) and container arguments by composing existing tests. Generated tests and proofs are linear in the size of the type (instead of quadratic), implemented in about 800 lines of Coq-Elpi, benchmarked to outperform alternatives, with current limits on mutual inductives and indexed vectors.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:04Equality test synthesis challenges
- 3:13Performance and quadratic complexity
- 6:44Constructor vs field comparison
- 8:51Linear-time equality implementation
- 14:17Implementation details
- 15:21Tool integration
- 16:26Q&A
related talks
27mAn Equations Tutorial
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
42mMetaCoq as a tool to prevent future unsoundness in Coq
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
21mChecking Equivalence in a Non-strict Language
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
19mExtensible Metatheory Mechanization via Family Polymorphism