小编tom*_*ry7的帖子

我想证明,对于每个组都存在一个减去函数,它接受组的一个元素并返回其负数.

我的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我认为可能是一个糟糕的角色.这是什么意思,有没有办法让它可读.

我的第二个问题是如何完成证明,在第一个问题得到解答后可能会更清楚.