论文标题
使用MetaCoQ生成归纳类型的归纳原理和条例关系
Generating induction principles and subterm relations for inductive types using MetaCoq
论文作者
论文摘要
我们在Metacoq中实现了三个有关归纳类型的COQ插件。第一个插件是一种简单的语法转换，通过在构造函数类型的混凝土索引上抽象来为电感类型生成替代构造函数。第二个插件重新输入Coq的$ \ texttt {scheme enculct} $命令在metacoq中，并将其扩展到嵌套的归纳类型，例如像玫瑰树这样的类型在其定义中使用$ \ texttt {list} $，类似于tassi的elpi-plugin。第三个插件实现了Metacoq中的方程软件包提供的$ \ texttt {derive subterm} $命令。
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 $\texttt{Scheme Induction}$ command in MetaCoq, and extends it to nested inductive types, e.g. types like rose trees which use $\texttt{list}$ in their definition, similar to the Elpi-plugin by Tassi. The third plugin implements the $\texttt{Derive Subterm}$ command provided by the Equations package in MetaCoq.
