Coq中不同类型的重载符号 [英] Overloading notation for different types in Coq
问题描述
我希望能够为不同的归纳定义定义相同的Coq表示法,并根据其自变量类型区分这些表示法。
I would like to be able to define the same Coq notations for different inductive definitions, and distinguish the notations based on the types of their arguments.
这里是一个最小的示例:
Here is a minimal example:
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
)使用相同的符号。
As you see, there is a mutually inductive definition, in which I'd like to be able to use the same notation for different types of terms (term1
and term2
).
尝试编译时遇到的错误是术语 tvar1的类型为 term1,而预期类型为 term2 。
。
The error I get when trying to compile this is The term "tvar1" has type "term1" while it is expected to have type "term2".
.
有没有办法使它工作?
推荐答案
我写了一封Coq邮件列表,并收到了答案使用类型类解决了我的问题:
I wrote to the Coq mailing list and received an answer from Gaëtan Gilbert that solved my problem using type classes:
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.
这篇关于Coq中不同类型的重载符号的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!