Towards general white-box automation: a typeclass-guided context cleaner
summary
Built a small Ltac2 clarifier called cdestruct that uses typeclass-guided hints to run only safe, non‑backtracking context cleanup: case splits, injection/discriminate, substitution, cbn, and proposition replacement driven by typeclass instances and gated options. The core is ~50 lines; it solves dependent‑map lemmas end‑to‑end without unsafe steps by copying and simplifying blocked obligations. Discrimination‑tree lookup and lack of a proper simplifier cause performance limits; injection is reimplemented to respect opacity. The code sits inside a project and isn’t yet a standalone repo.
AI-written summary · about
chapters (10)
- 0:00White-box automation intro
- 1:27Automation trade-offs
- 3:58Limitations of tactics
- 7:26General proof search architecture
- 8:50Designing clarifier CDstruct
- 11:16Typeclass hints and trees
- 14:26Practical lessons
- 15:49Future challenges
- 17:13Q&A: Forward reasoning
- 20:03Q&A: Hint integration
related talks
01h 10mMedium-scale automation for proof assistants
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
38mType System Foundations for Super-Charged Semantic Code Search
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
29mType Inference Techniques: Implementation and Formalization, Better Together
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
45mAbstraction Considered Harmful (and other opinions about writing maintainable code)
26mJavaScript Tools at Scale Using Type Information