Generating induction principles and subterm relations for inductive types using MetaCoq
arXiv:2006.15135
Abstract
We implement three Coq plugins regarding inductive types in MetaCoq. The first plugin is a simple syntax transformation generating alternative constructors for inductive types by abstracting over concrete indices in the types of the constructors. The second plugin re-implements Coq's command in MetaCoq, and extends it to nested inductive types, e.g. types like rose trees which use in their definition, similar to the Elpi-plugin by Tassi. The third plugin implements the command provided by the Equations package in MetaCoq.
accepted for presentation at the Coq Workshop 2020