Marcel Ullrich: Bachelor's Thesis

Saarland University Computer Science

Generating induction principles for nested inductive types in MetaCoq

Advisors: Yannick Forster


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:


Legal notice, Privacy policy