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

Question

Coq (8.5p1) 似乎在理解 "negative" 表达式如 -(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.，或者用有理数 (Q) 替换整数 (Z)，错误就会消失。对我来说，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 在他的评论中提到的，Require Import QArith. 打开了 Qscope 范围（在部分之外）。但是从 ZArith 导出的模块要么在本地用 Local Open Scope Z_scope. 打开 Z_scope，要么在最后使用 Close Scope Z_scope.。

您可以使用 Print Visibility. 查看当前可用的符号和打开的范围。

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

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

Coq: Unknown interpretation for negative integer expressions

coq