コック：私が得た、上記の場合</p> <pre><code>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. </code></pre> <p>：負の整数式の不明な解釈

Question

コック（8.5p1）は、いくつかのトラブルなど、次の例のように-(x + y)、などの「負」の表現を理解しているようです（-xとCoqIDEで(-(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.

マークは彼のコメントで述べたように、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 
*)