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）推断重载运算符（在本例中为 ⊢）的定义（ and/or 基于作为符号一部分的其他运算符，例如 ∈ 与 <:)？

（请注意，使用不同的符号不是一种选择，因为我的 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).

情况类似于 The Coq Reference Manual (§12.1.3) 中描述的情况：

In the last case though, there is a conflict with the notation for type casts. This last notation, as shown by the command Print Grammar constr. is at level 100. To avoid x : A being parsed as a type cast, it is necessary to put x at a level below 100, typically 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).

Coq 符号中的重载运算符

Overloading operators in Coq notations

operator-overloading

coq