Coq 表示法中“<”的语法错误

Question

以下代码：

Reserved Notation "g || t |- x < y" (at level 10).

Inductive SubtypeOf :
  GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
    forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u < u
where "g || t |- x < y" := (SubtypeOf g t x y).

给出以下错误：

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

如果我使用 <: 代替 <，我会得到类似的错误。

但是这段代码工作正常：

Reserved Notation "g || t |- x << y" (at level 10).

Inductive SubtypeOf :
  GammaEnv -> ThetaEnv -> UnsafeType -> UnsafeType -> Set :=
| SubRefl :
    forall (gamma : GammaEnv) (theta : ThetaEnv) (u : UnsafeType) , gamma || theta |- u << u
where "g || t |- x << y" := (SubtypeOf g t x y).

为什么？是否有可以更改为允许 < 或 <: 表示法的优先级设置？是否存在我与之冲突的内置语法，并且在定义符号时需要注意？

Answer 1

Coq 使用 LL1 解析器来处理符号。它还可以输出语法。那么，让我们检查一下我们得到了什么

Reserved Notation "g || t |- x < y" (at level 10).

Print Grammar constr. 输出：

...
| "10" LEFTA
  [ SELF;
    "||";
    constr:operconstr LEVEL "200";        (* subexpression t *)
    "|-";
    constr:operconstr LEVEL "200";        (* subexpression x *)
    "<";
    NEXT
...

这里，

10是我们的优先级；
LEFTA表示左结合性；
200 是内部子表达式的默认优先级。

考虑到较低层级比较高层级结合更紧密这一事实以及 < 层级为 70 的事实（参见 Coq.Init.Notations），我们可以推断 Coq 是尝试将 x < y 部分解析为 x 的子表达式，使用 < 标记，因此出现错误消息。

为了补救这种情况，我们可以通过分配 x 更高的优先级，即较低的级别，明确禁止将第三个参数解析为 less-than 表达式。

Reserved Notation "g || t |- x < y" (at level 10, x at level 69).

Print Grammar constr.

| "10" LEFTA
  [ SELF;
    "||";
    constr:operconstr LEVEL "200";        (* subexpression t *)
    "|-";
    constr:operconstr LEVEL "69";         (* subexpression x *)
    "<";
    NEXT

Coq 表示法中“<”的语法错误

Syntax Error with `<` in Coq Notations

parsing

syntax

operators

coq

notation