Coq 符号中的重载运算符

Question

我想为几种判断创建符号，例如类型和子类型关系：

Reserved Notation "Г '⊢' t '∈' T" (at level 40).
Reserved Notation "Г '⊢' T '<:' U" (at level 40).

Inductive typing_relation : context -> term -> type -> Prop := ...
where "Γ '⊢' t '∈' T" := (typing_relation Γ t T).

Inductive subtyping_relation : context -> type -> type -> Prop := ...
where "Г '⊢' T '<:' U" := (subtyping_relation Γ T U).

据我了解，Coq 不允许这样做，因为 ⊢ 运算符在这些定义中被重载。

如何让 Coq 根据其参数的类型（例如 term 与 type）（和/或基于其他运算符）推断重载运算符的定义（在本例中为 ⊢）这是符号的一部分，例如∈ vs <:)？

（请注意，不能选择使用不同的符号，因为我的 Coq 程序定义了几种类型和子类型关系。）

编辑：这是一个最小的例子：

Inductive type : Type :=
  | TBool : type.

Inductive term : Type :=
  | tvar : nat -> term.

Definition context := nat -> (option type).

Reserved Notation "G '⊢' t '∈' T" (at level 40).

Inductive typing_relation : context -> term -> type -> Prop :=
 | T_Var : forall G x T,
      G x = Some T ->
      G ⊢ tvar x ∈ T
 where "G '⊢' t '∈' T" := (typing_relation G t T).

Reserved Notation "G '⊢' T '<:' U" (at level 40).

Inductive subtype_relation : context -> type -> type -> Prop :=
  | S_Refl : forall G T,
      G ⊢ T <: T
  where "G '⊢' T '<:' U" := (subtype_relation G T U).

这会导致错误：

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

Answer 1

原因是你不能这样使用<:，因为<:已经被定义为Coq的typecast notation。它的行为就好像它是这样定义的

Reserved Notation "t <: T" (at level 100, right associativity).

这种情况类似于 Coq 参考手册 (§12.1.3) 中描述的情况：

但在最后一种情况下，类型转换的表示法存在冲突。最后一个符号，如命令 Print Grammar constr. 所示，级别为 100。为避免 x : A 被解析为类型转换，有必要将 x 置于 100 以下的级别，通常为 99。

以下是针对您的情况的可能解决方案：

Reserved Notation "G '⊢' t '∈' T" (at level 40, t at level 99).
Reserved Notation "G '⊢' T '<:' U" (at level 40, T at level 99).