Coq eapply 生成带有问号的目标，同时证明函数的存在

Question

我想证明，对于每个组，都存在一个减法函数，它接受组中的一个元素并返回它的负数。

我的 Coq 代码如下：

Record Group:Type := {
G:Set;
plus: G->G->G;
O:G;
assoc: forall x y z:G, plus x (plus y z)=plus (plus x y) z;
neut: forall x:G, plus x O=x /\ plus O x=x;
neg: forall x:G, exists y:G, plus x y=O
}.

Lemma minus_exists(H:Group):exists minus_func:G H->G H, (forall x:G H, plus H x (minus_func(x))=O H).
eapply ex_intro.

最后一个策略产生以下输出：

  H : Group
  ============================
   forall x : G H, plus H x (?12 x) = O H

我的第一个问题是?12，我认为它可能是一个显示不佳的角色。这是什么意思，有没有办法让它可读。

我的第二个问题是如何完成证明，回答完第一个问题后可能会更清楚。

Answer 1

在我的 Coq 版本中，我得到了：

forall x : G H, plus H x (?minus_func x) = O H

稍微好一点。在 Coq 中，以 ?T 形式显示的术语就是我们所说的 “元” 或 “存在变量” (evar)。

术语来自逻辑编程和自动定理证明领域，可以粗略解释为代表“未知术语”。通常，eva在统一过程中扮演变量的角色。整个 Coq 证明引擎都是围绕未知或 evar 的概念构建的。

在您的情况下，eapply ex_intro（或eexists）缺少见证人。 Coq 将创建一个新的“evar”来代表缺失的函数，并允许你继续你的证明。但请注意，为了完成证明，您需要稍后提供证人。

如何将 evas 转化为实际术语？用实际术语替换 evar 的行为称为“实例化”。在许多情况下，实例化将由统一算法执行。例如，如果我们有一个引理：

Lemma f_plus x : plus H x (f x) = O H

我们可以将apply f_plus 和?minus_func 替换为f。另一种方法是使用instantiate 策略，但现在它已经过时了。在我们之前的例子中，你可以写instantiate (1 := f)，这将用f替换?minus_func。由于技术原因，这种方法不再得到很好的支持，因此在实践中，您必须通过统一实例化 evas 或提供策略的实际见证。

我建议您阅读更多关于统一和逻辑编程的内容。

Answer 2

?12 不是一个显示不好的字符，它是一个漏洞。 eapply 策略是一种“应用这个引理/假设，但我手头还没有所有的输入，所以请插入空洞，我会稍后补上”。

通过输入eapply ex_intro（或eexists），您只是在说“存在一个我还不知道的功能，所以请用一个孔替换它，我稍后会提供它”。但是，由于您的引理的全部目的是构建此功能，我不确定您是否走在正确的道路上。尝试在没有任何efoo 策略的情况下证明你的引理，你不需要它们。