Coq：关于“%”和"mod"作为符号

Question

我正在尝试定义模等价关系的表示法：

Inductive mod_equiv : nat -> nat -> nat -> Prop :=
  | mod_intro_same : forall m n, mod_equiv m n n
  | mod_intro_plus_l : forall m n1 n2, mod_equiv m n1 n2 -> mod_equiv m (m + n1) n2
  | mod_intro_plus_r : forall m n1 n2, mod_equiv m n1 n2 -> mod_equiv m n1 (m + n2).

(* 1 *) Notation "x == y 'mod' z" := (mod_equiv z x y) (at level 70).
(* 2 *) Notation "x == y % z" := (mod_equiv z x y) (at level 70).
(* 3 *) Notation "x == y %% z" := (mod_equiv z x y) (at level 70).

Coq 接受这三种表示法。但是，在某些情况下我不能使用符号来陈述定理：

(* 1 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p mod m -> p == n mod m.
(* Works fine as-is, but gives error if `Arith` is imported before:
   Syntax error: 'mod' expected after [constr:operconstr level 200] (in [constr:operconstr]).
*)

(*************************************)

(* 2 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p % m -> p == n % m.
(* Gives the following error:
   Syntax error: '%' expected after [constr:operconstr level 200] (in [constr:operconstr]).
*)

(*************************************)

(* 3 *)
Theorem mod_equiv_sym : forall (m n p : nat), n == p %% m -> p == n %% m.
(* Works just fine. *)

符号 mod 在顶层的 Coq.Init.Nat 和 Coq.Arith.PeanoNat 下定义。为什么新符号 x == y 'mod' z 在一个环境中可以，但在另一个环境中却不行？
符号 % 似乎与内置的 % 符号冲突，但 Coq 解析器给出与 mod 情况几乎相同的错误消息，并且消息在这两种情况下都不是很有帮助。这是有意的行为吗？ IMO，如果解析器无法理解如此琐碎的上下文中的符号，那么首先不应该接受该符号。

Answer 1

你的第一个问题有一个简单的答案。 Coq 的初始状态（部分）由 Coq.Init.Prelude, which (as of this answer 决定）包含行

Require Coq.Init.Nat.

也就是说，Coq.Init.Prelude 未导入，仅在 Require 中可用。仅当包含它们的模块被导入时，符号才处于活动状态。如果符号声明为本地 (Local Notation ...)，则即使导入模块也不会激活符号。

第二个问题比较棘手，它深入研究了 Coq 如何解析符号。让我们从一个有效的例子开始。在Coq.Init.Notations中（实际上是在Coq.Init.Prelude中引入的），"x <= y < z"这个符号是保留的。

Reserved Notation "x <= y < z" (at level 70, y at next level).

在Coq.Init.Peano（也是导入的）中，对符号赋予了意义。我们不会真的担心那部分，因为我们主要关心解析。

要查看保留符号的效果，可以使用白话命令Print Grammar constr.。这将显示一长串用于解析 constr（Coq 语法的基本单元）的所有内容。此符号的条目位于列表的下方。

| "70" RIGHTA
  [ SELF;  "?="; NEXT
  [...]
  | SELF;  "<="; NEXT;  "<"; NEXT
  [...]
  | SELF;  "="; NEXT ]

我们看到符号是右结合的(RIGHTA)¹并且生活在70级。我们还看到符号中的三个变量，x、y和z分别在70级（SELF）、71级（NEXT）和71级（NEXT）解析。²

在解析过程中，Coq 从级别 0 开始并查看下一个标记。直到有一个令牌应该在当前级别解析，级别才会增加。因此，较低级别的符号优先于较高级别的符号。（这在概念上是如何工作的 - 它可能已经优化了一点）。

当找到复杂的符号时，例如在“5 <=”之后，解析器会记住该符号的语法³：SELF; "<="; NEXT; "<"; NEXT。在“5 <=”之后，我们在 71 级解析 y，这意味着如果在低于 71 级时没有任何效果，我们将停止尝试解析 y 并继续。

之后，下一个标记必须是“<”，如果是，那么我们在第71层解析z。

关卡的伟大之处在于它允许与其他符号进行交互而无需括号。例如，在代码 1 * 2 < 3 + 4 <= 5 * 6 中，我们不需要括号，因为 * 和 + 声明在较低级别（分别为 40 和 50）。因此，当我们解析 y（在第 71 级）时，我们能够在继续 <= z 之前解析所有 3 + 4。此外，当我们解析 z 时，我们可以捕获 5 * 6，因为 * 的解析级别低于 z.

的解析级别

好的，既然我们了解了这一点，我们就可以弄清楚你的情况是怎么回事了。

当 Arith（或 Nat）被导入时，mod 成为一个符号。具体来说，我们在第 40 层有一个左结合符号，其语法为 SELF; "mod"; NEXT（使用 Print Grammar constr. 进行检查）。当您定义 mod 符号时，该条目在 70 级与语法 SELF; "=="; constr:operconstr LEVEL "200"; "mod"; NEXT 是右关联的。中间部分只是意味着 y 在 200 级被解析（作为一个 constr - 就像我们讨论过的其他所有内容一样）。

因此，在解析n == p mod m时，我们解析n ==很好，然后在200级开始解析y。由于Arith的mod只是在40级，所以我们将如何解析 p mod m。但随后我们的 x == y mod z 符号就悬而未决了。我们在语句的末尾，mod z 仍然没有被解析。

Syntax error: 'mod' expected after [constr:operconstr level 200] (in [constr:operconstr]).

（错误现在更有意义了吗？）

如果你真的想在使用 Arith 的 mod 符号的同时使用你的 mod 符号，你需要在较低级别解析 y 。由于 x mod y 处于 40 级，我们可以使用

使 y 成为 39 级

Notation "x == y 'mod' z" := (mod_equiv z x y) (at level 70, y at level 39).

由于算术运算在 40 级及以上，这意味着我们需要使用括号编写 5 == (3 * 4) mod 7。

对于你的“%”符号，这会很困难。 “%”通常用于范围定界（例如 (x + y)%nat）并在级别 1 绑定得非常紧密。您可以在级别 0 进行 y 解析，但这意味着根本没有符号可用于y 没有括号。如果可以接受，请继续。

由于“%%”与任何东西（在标准库中）没有冲突，您可以在这里以任何方便的级别自由使用它。您可能希望在较低级别进行 y 解析（y at next level 是非常标准的），但这不是必需的。

右结合性是默认值。显然 Coq 的解析器没有 "no associativity" 选项，所以即使你明确地说 "no associativity"，它仍然被注册为右结合。这在实践中通常不会造成麻烦。
这就是为什么用"y at the next level"保留符号的原因。默认情况下，符号中间的变量在 200 级解析，可以通过保留类似符号 Reserved Notation "x ^ y ^ z" (at level 70). 并使用 Print Grammar constr. 来查看解析级别。正如我们将看到的，这就是 x == y mod z.
如果多个符号以“5 <=”开头会怎样？那个与较低的级别显然会被采用，但如果它们具有相同的级别，它会尝试两者并在不解析时回溯。但是，如果一个符号完成，它不会回溯，即使该选择稍后会导致麻烦。我不确定确切的规则，但我怀疑这取决于首先声明的符号。

Coq：关于“%”和"mod"作为符号

Coq: About "%" and "mod" as a notation symbol

coq

notation