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)。

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

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

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

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

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

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