Scrap your boilerplate definitions in 10 lines of Ltac!
summary
Library IDT generates new inductive definitions from existing ones by running Template-Coq code driven by small Ltac constructor-transformer tactics, so dozens of boilerplate lemmas (multi‑step pair reduction cases, inversion lemmas, congruence rules) come from a few lines of script. It builds an “empire” relation encoding all those lemmas, proves a single soundness/completeness theorem, and then applies constructors to extract cases. Metacoq does the heavy lifting under the hood; mutual or universe‑polymorphic types are not yet supported.
AI-written summary · about
chapters (12)
- 0:00Start
- 2:49Boilerplate Lemmas
- 3:31Not Just Being Lazy
- 4:16Key Idea
- 4:36Example
- 6:03Inductive Definition Transformers
- 10:31A Typing Rule
- 10:42Generating Inversion Lemmas
- 11:30Twist
- 12:52Indistinguishability
- 13:09A Congruence Rule
- 14:51Conclusion
related talks
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders
19mExtensible Metatheory Mechanization via Family Polymorphism
25mDeriving Instances with Dependent Types
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
24mCode Extraction from Coq to ML-like languages
27mAn Equations Tutorial
01h 34mFormal Logic Undressed
19mInterpreting OCaml GADTs into Coq