Nested Inductive Types for Rocq and Lean
summary
Nested nested inductive types like RoseTree now get a syntactic check that classifies well behaved cases and rejects ones that rely on reduction tricks, letting the system new positivity condition decide positivity without computing mutual encodings. The implementation generates modular all predicates and matching eliminators automatically, handles nesting across containers and parameters, and is merged into Rocq 9.2 so large developments (Metaroc) can drop hundreds of lines of boilerplate.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:26What are nested types
- 4:38Support in Rocq and Lean
- 7:09Problems with eliminators
- 9:18New approach for nested types
- 11:52Implementation in Rocq
- 14:41Automatic predicate generation
- 15:54Comparison with old approaches
- 18:22Usability and custom definitions
related talks
34mLanguage Design Where Paradigms Meet
22mA Calculus of Inductive Linear Constructions
51mElpi: rule-based meta-languge for Rocq
29mType Checking with Rewriting Rules
19mCertified Compilers à la Carte
19mMerging Inductive Relations
14mA Limited Case for Reification by Type Inference
01h 03mVerifying Dependent Type-checkers