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"来代表缺失的功能,并允许您继续您的证明.但请注意,为了完成证明,您需要稍后提供证人.

如何将evars变为实际条款？用实际术语代替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.由于技术原因,这种方法不再受到很好的支持,因此在实践中,你必须通过统一来实例化evars或者提供战术的实际见证.

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