Coq中不同类型的重载符号

Question

我希望能够为不同的归纳定义定义相同的Coq表示法，并根据其参数类型区分这些表示法。

这是一个最小的示例：

Inductive type : Type :=
| TBool : type.

Inductive term1 : Type :=
| tvar1 : term1.

Inductive term2 : Type :=
| tvar2 : term2.

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

Reserved Notation "G '?' t '::' T" (at level 40, t at level 59).

Inductive typing1 : context -> term1 -> type -> Prop :=
 | T_Var1 : forall G T,
      G ? tvar1 :: T
where "G '?' t1 '::' T" := (typing1 G t1 T)                            
with typing2 : context -> term2 -> type -> Prop :=
 | T_Var2 : forall G T,
      G ? tvar2 :: T
where "G '?' t2 '::' T" := (typing2 G t2 T).

如您所见，这里有一个相互归纳的定义，在该定义中，我希望能够对不同类型的术语（term1和term2）使用相同的符号。

我在尝试编译时遇到的错误是The term "tvar1" has type "term1" while it is expected to have type "term2".。

有没有办法让它工作？

Answer 1

我写信给Coq邮件列表，收到了GaëtanGilbert 的答复，该答复使用类型类解决了我的问题：

Inductive type : Type :=
| TBool : type.

Inductive term1 : Type :=
| tvar1 : term1.

Inductive term2 : Type :=
| tvar2 : term2.

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

Class VDash (A B C : Type) := vdash : A -> B -> C -> Prop.
Notation "G '?' t '::' T" := (vdash G t T) (at level 40, t at level 59).

Inductive typing1 : VDash context term1 type :=
| T_Var1 : forall G T,
    G ? tvar1 :: T

with typing2 : VDash context term2 type :=
| T_Var2 : forall G T,
    G ? tvar2 :: T.