1

我目前正在研究证明，我发现自己一遍又一遍地编写这样的代码：

Lemma eq_T: forall (x y : T), {x = y} + {x <> y}
  with eq_trait: forall (x y : trait), {x = y} + {x <> y}
  with eq_pi: forall (x y : pi), {x = y} + {x <> y}.
  Proof.
    decide equality; auto with ott_coq_equality arith.
    decide equality; auto with ott_coq_equality arith.
    decide equality; auto with ott_coq_equality arith.        
  Defined

Hint Resolve eq_T : ott_coq_equality.
Hint Resolve eq_trait : ott_coq_equality.
Hint Resolve eq_pi : ott_coq_equality.

也就是说，我有一些相互归纳的类型，并且我同时推导出所有这些类型的相等性。

我想做的是有某种宏，我可以写

MutualDeriveEquality T, pi, trait

它将机械地生成上述命令，以便我可以将其用于各种互感类型。

我对 LTac 不是很了解，但我不确定它是否适用于这里，因为我不仅要自动生成证明术语，还要自动定义白话中的值。（不过我可能完全错了）。

我想知道的是，有没有办法定义一个可以自动化的“白话宏”？或者这是可以用 LTac 完成的事情吗？或者是在 OCaml 中编写 Coq 插件的唯一方法？

4

1 回答 1

2

你是对的，Ltac 不适合这项任务。目前，无法在 Coq 中自动执行此类任务，但正在为此开发一些工具。参见例如Template Coq或Coq-Elpi。大多数这些工具都处于预发布状态。

作为替代方案，我建议从更抽象的类型描述中生成您自己的 .v 文件，用您选择的语言编写文件生成器。

于 2018-07-05T07:22:12.073 回答