Charla "(Nested) Inductive Types in Lean and Rocq"

Expositor: Nicolas Tabareau (Inria, Francia)

Abstract: Inductive types are a fundamental abstraction mechanism in type theory and proof assistants, supporting the definition of data structures and rich specifications. Nested inductive types extend this mechanism by allowing constructors to use parametric types instantiated with the type being defined (e.g., lists or trees of the type to be defined). They are widely used in large verification projects – including CompCert, Iris, Verinum, and MetaRocq – to express complex, structured specifications. Despite this widespread use, the treatment of nested inductive types in both Lean and Rocq is unsatisfactory. Lean rejects many practical definitions while Rocq accepts definitions for which no usable elimination principle can be defined. Neither system provides reliable automatic generation of elimination principles. As a result, developers must define custom eliminators by hand, leading to fragility, duplication, and significant proof engineering overhead. 

In this talk, I will first provide a gentle introduction to (mutual) inductive types, explaining what they are used for, in which way they are part of the trusted code base and how they are typically used (in a different way) in Lean and in Rocq. 

I will then present a novel validity criterion for nested inductive types based on parametricity that guarantees that they can be elaborated into well-formed mutual inductive types. Under this criterion, the elimination principle for the original nested definition is provably equivalent to that of its elaborated mutual form. Our condition strictly generalizes Lean’s current check while ruling out exactly the problematic cases accepted in Rocq.