Advisors: Yannick Forster
Inductive types and their induction principles are essential components in modern dependent type theory and proof assistants like Coq, where most proofs involve induction and a great deal of predicates are written in an inductive fashion. While Coq automatically generates induction principles, these principles are too weak for nested inductive types. Therefore, one needs to put in additional work to get induction principles that are strong enough. It is folklore that induction principles for nested inductive types require creativity and lots of work. Only recently the underlying principle to generate these induction principles was discovered. We implement a plugin in MetaCoq to automatically generate such induction principles based on the unary parametricity translation. Furthermore, we verify the correctness of parts of the plugin using MetaCoq.
Our goal is to generate not only case analysis and normal induction principles but also stronger principles for example for nested inductive types, as the standard principle of Coq is usually very weak in those cases. For inductive type without nested inductive recursion like binary trees, Coq generates a useful lemma: $$ \begin{align} &\forall P~: binaryTree \to Prop.\\ &P~Node \to\\ &(\forall (a~b : binaryTree). P~a \to P~b \to P~(\mathit{Leaf}~a~b)) \to\\ &\forall b : binaryTree. P~b \end{align} $$ But Coq has problems with inductive principles on nested inductive types. An example are rose trees where the recursion for sub-trees is inside a list: $$ \begin{align} Inductive~roseTree~:=~node~(xs:list~roseTree). \end{align} $$ The generated induction lemma only gives the list but does not perform recursion and therefore no inductive hypothesis is available. $$ \begin{align} &\forall P~: roseTree \to Prop.\\ &(\forall xs : list~roseTree. P~(node~xs)) \to\\ &\forall r : roseTree. P~r \end{align} $$ The desired property is that the statement holds for each subtree in the tree list xs such as in this lemma: $$ \begin{align} &\forall P:roseTree \to Prop.\\ &(\forall xs: list~roseTree. \color{blue}{(\forall t. t\in xs \to P~t) \to} P~(node~xs)) \to\\ &\forall r:roseTree. P~r \end{align} $$ A construction of those stronger lemmas is achieved using MetaCoq for manipulation of the inductive types. We build upon the idea of Tassi to use the unary parametricity translation of types for better induction hypotheses.