如何在Coq中使用‘0V’作为向量空间零元符号？

当然可以使用0V作为零向量的记号！你遇到的类型不匹配错误，本质是Coq没有明确区分域的0和向量空间的0V的类型上下文——解决这个问题的核心，是利用Coq的作用域（Scopes）机制为不同代数结构的记号划分独立的命名空间。

具体解决方案 #

1. 声明专属作用域

先为域和向量空间分别声明独立的作用域，让Coq知道哪些记号属于哪个类型系统：

(* 为域结构声明作用域 *)
Declare Scope field_scope.
(* 为向量空间结构声明作用域 *)
Declare Scope vector_space_scope.

2. 绑定记号到对应作用域

把域的记号绑定到field_scope，向量空间的0V等记号绑定到vector_space_scope：

(*******************)
(* Field notations *)
(*******************)
Notation "0" := zero : field_scope.
Notation "1" := one : field_scope.
Infix "+" := add : field_scope.
Infix "*" := mul : field_scope.

(**************************)
(* Vector space notations *)
(**************************)
Notation "0V" := zerov : vector_space_scope.
Notation "11" := onev : vector_space_scope.
Infix "_v" := addv (at level 50, no associativity) : vector_space_scope.
Infix "*_v" := mulv (at level 60, no associativity) : vector_space_scope.

3. 打开作用域（或显式指定）

你可以通过Open Scope命令默认打开需要的作用域，后续代码中Coq会自动匹配对应记号：

(* 默认启用域和向量空间的作用域 *)
Open Scope field_scope.
Open Scope vector_space_scope.

如果遇到类型推断模糊的场景，还可以在表达式后加%作用域名显式指定：

Lemma mul_0_l: forall (v : V), eqv (mulv 0%field_scope v) 0V%vector_space_scope.

进阶：用类型类自动匹配作用域

如果你的域和向量空间是用**类型类（Type Classes）**定义的（这是Coq中抽象代数的标准写法），还可以把作用域和类型类绑定，让Coq自动根据上下文选择记号：
假设你有如下类型类定义：

Class Field (F : Type) := {
  zero : F;
  one : F;
  add : F -> F -> F;
  mul : F -> F -> F;
  (* 省略域的其他公理 *)
}.

Class VectorSpace (F : Type) `{Field F} (V : Type) := {
  zerov : V;
  addv : V -> V -> V;
  mulv : F -> V -> V;
  (* 省略向量空间的其他公理 *)
}.

添加以下绑定后，Coq会自动识别类型对应的作用域：

Bind Scope field_scope with Field.
Bind Scope vector_space_scope with VectorSpace.

验证你的引理 #

修改完成后，原来的引理可以正常编写和证明，Coq能正确区分域的0（类型F）和向量的0V（类型V）：

Lemma mul_0_l: forall (v : V), eqv (mulv 0 v) 0V.
Proof.
(* 你的证明过程 *)
Qed.

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