Rocq中如何定义实例求解器可穿透的透明别名？

针对你遇到的问题，有几种实用方案可以定义能自动展开、不破坏类型类解析的非符号化别名：

1. 使用Notation定义标识符别名 #

别被“符号”这个词限制——Notation完全可以定义普通标识符作为别名，这种别名属于语法层面的替换，不会创建新常量，Coq会自动将其展开为原元素，类型类解析也能正常匹配原元素的实例。

示例：

(* 为list类型定义别名my_list *)
Notation my_list := list.

(* 检查时自动展开为原类型 *)
Check my_list nat. (* 输出：list nat : Set *)

(* 类型类实例直接适配，无需额外定义 *)
Instance my_list_eq_dec A `(EqDec A) : EqDec (my_list A) := list_eq_dec A _.

2. 给Definition添加强制自动展开标记 #

如果一定要用Definition，可以通过Arguments命令的!标记，让Coq在类型检查、类型类解析过程中自动展开这个定义，使其表现得像别名而非新常量。

示例：

Definition my_nat := nat.
(* 强制Coq自动展开my_nat *)
Arguments my_nat !.

(* 检查时直接显示原类型 *)
Check my_nat. (* 输出：nat : Set *)

(* 类型类解析会自动展开my_nat，匹配nat的已有实例 *)
Check eq_dec my_nat. (* 正常调用nat的eq_dec实例 *)

3. 局部场景用Let定义别名 #

如果只是在局部上下文（比如Section内部）需要别名，可以用Let替代Definition。Let定义的名称在离开局部上下文后会被自动展开，不会留下新常量，自然也不会影响类型类解析。

示例：

Section LocalAlias.
Let my_bool := bool.
Check my_bool. (* 输出：bool : Set *)
End LocalAlias.

(* 离开Section后，my_bool会被完全展开，外部无法直接引用 *)

为什么Definition会出问题？ #

Definition本质是创建了一个新的常量，哪怕它的定义和原元素完全一致，Coq也会将其视为不同的实体——类型类实例是绑定到原元素上的，自然无法匹配这个新常量。而上面的方案要么是语法层面的替换，要么是强制Coq自动展开定义，让类型类解析能看到背后的原元素。

内容的提问来源于stack exchange，提问作者Jason Carr