是否可以在 Coq 中声明类型相关的表示法？

Question

由于 Coq 具有强大的类型推断算法，我想知道我们是否可以根据 Notation 的变量“重载”不同的重写符号。

作为示例，我将借用我的一篇关于在 Coq 中形式化类型化语言语义的工作。在这个形式化中，我有类型对和表达式对，我想对它们各自的构造函数使用相同的符号：{ _ , _ }.

Inductive type: Type := ... | tpair: type -> type -> type | ...
Inductive expr: Type := ... | epair: expr -> expr -> expr | ... 

Notation "{ t1 , t2 }" := tpair t1 t2
Notation "{ e1 , e2 }" := epair e1 e2

我知道最后一条语句会引发错误，因为已经定义了符号；如果有人考虑过绕过它的诡计，或者是否有另一种“官方”方法来做到这一点，我将不胜感激。

Answer 1

重载符号的一种简单方法是使用作用域。事实上，大多数时候你应该使用范围，这样你的符号就不会与你可能包含或可能包含你的其他作品的符号混合。

使用范围定界符，例如可以使用 { t1 , t2 }%ty 和 { e1 , e2 }%exp（使用定界符 ty 和 exp 来消除歧义）。

就是说，为了利用类型信息，有一个涉及类型类的技巧，即拥有一个带有自己的符号的对的通用概念，然后声明它的实例。请参见下面的示例：

Class PairNotation (A : Type) := __pair : A -> A -> A.

Notation "{ x , y }" := (__pair x y).

Instance PairNotationNat : PairNotation nat := {
  __pair n m := n + m
}.

Axiom term : Type.
Axiom tpair : term -> term -> term.

Instance PairNotationTerm : PairNotation term := {
  __pair := tpair
}.

Definition foo (n m : nat) : nat := { n , m }.
Definition bar (u v : term) := { u , v }.

是否可以在 Coq 中声明类型相关的表示法？

Is it possible to declare type-dependent Notation in Coq?

overloading

notation

coq