# Generating induction principles for nested inductive types in MetaCoq

## Abstract:

One of the most used proof strategies is proof by induction. Coq can automatically state and prove a structural induction principle for inductive types. For a wide range of types, this is very useful but for some types, it is too weak. This paper shows an implementation of stronger induction principles on nested inductive types using the MetaCoq framework.

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~:=~tree~(xs:\mathcal{L}~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 : \mathcal{L}~roseTree, P~(tree~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: \mathcal{L}~roseTree, \color{blue}{(\forall t, t\in xs \to P~t) \to} P~(tree~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.

## Main References:

• Tassi, Enrico. "Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq." (2019)
• Sozeau, Matthieu, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. "The MetaCoq Project." (2019)
• Anand, Abhishek, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. "Towards certified meta-programming with typed T emplate-C oq." In International Conference on Interactive Theorem Proving, pp. 20-39. Springer, Cham, 2018.