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根据其参数类型(例如，⊢对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的排版符号。它的作用就好像它是这样定义的。

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