Coq:负整数表达式的未知解释

Question

Coq (8.5p1) 似乎在理解“负”表达式(如 -(x + y))时遇到一些困难，如下例所示:

Require Import ZArith.
(* Open Scope Z_scope. *)
Goal (forall x:Z, x + (-x) = 0) 
 -> forall a b c:Z, a + b + c + (-(c+a)) = b.

对于上述内容，我收到错误(对于 CoqIDE 中的 -x 和 (-(c+a))):

Error: Unknown interpretation for notation "- _".

我很困惑为什么会发生这个错误。另外，如果我像注释中那样执行 Open Scope Z_scope. 操作，或者将整数 (Z) 替换为有理数 (Q)，则会出现错误消失了。对我来说，Z 和 Q 在取底片方面应该是相同的。

这背后有什么原因吗？

Answer 1

Coq 引用手册 v8.5:

Remark: Open Scope and Close Scope do not survive the end of sections where they occur. When defined outside of a section, they are exported to the modules that import the module where they occur.

正如 Mark 在评论中提到的，需要导入 QArith。 打开 Qscope 范围(在节之外)。但是从 ZArith 模块导出的模块要么使用 Local Open Scope Z_scope 在本地打开 Z_scope，要么使用 Close Scope Z_scope。在最后。

您可以使用打印可见性。来检查当前可用的符号和打开的范围。

Require Import Coq.ZArith.ZArith.
Print Visibility.
(* does not show anything interesting *)

另一个例子:

Require Import Coq.ZArith.ZArith.
Open Scope Z_scope.    
Print Visibility.
(* ...
   Visible in scope Z_scope
   ...
   "- x" := Z.opp x    (* that's what we want! *)
*)

现在是有理数:

Require Import Coq.QArith.QArith.
Print Visibility.
(* ...
   Visible in scope Q_scope
   ...
   "- x" := Qopp x
*)