InducTeX: A MetaCoq plugin for typesetting inductive definitions
summary
Builds a MetaCoq plugin that quotes Coq inductives, inspects constructors in the TemplateMonad and pretty prints them as TeX inference rules, so it prints inference rules directly from the Coq definitions instead of retyping them. Handles implicit arguments with small combinators that map constructor shapes to LaTeX strings, works around missing notation metadata by reusing Coq notation tricks, and can emit HTML via electreon integration. Early prototype works for large relations but takes seconds and needs performance tuning.
AI-written summary · about
chapters (9)
- 0:00InducTeX introduction
- 3:51Plutus compiler certification
- 8:05Translation relations in Coq
- 10:51Building InducTeX with MetaCoq
- 12:57Demo and limitations
- 14:21Custom notation rules
- 16:52Integration with documentation tools
- 18:16Related work and future
- 20:23Conclusion and Q&A
related talks
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants
26mIntegrating graphical proofs in Coq
16mIncremental Proof Development in Dafny with Module-Based Induction
01h 10mMedium-scale automation for proof assistants
21mLive Verification in an Interactive Proof Assistant
29mType Inference Techniques: Implementation and Formalization, Better Together
24mTowards Pen-and-Paper-Style Equational Reasoning in Interactive Theorem Provers by(…)
29mDiagrammatic notations for interactive theorem proving