是否可以在 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 }%tyand{ e1 , e2 }%exp例如（使用分隔符tyandexp来消除歧义）。

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

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