coq - 如何在 Coq 中有 "0"的多个符号

Question

我已经在 Coq 中定义了域公理，并使用它们来证明简单的属性，如描述的 here .然后，我添加了向量空间公理并在那里证明了简单的性质。由于 0 符号已被我的领域使用:

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

我为我的向量空间使用了有点丑陋的符号:

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

这允许证明以下简单引理:

Lemma mul_0_l: forall (v : V), (eqv (mulv 0 v) 00).

当我将 "00" 更改为 "0V"(更漂亮)时，一切都停止工作，并且出现以下错误:

In environment
v : V
The term "0" has type "F" while it is expected to have type "V".

有没有办法使用“0V”？还是我坚持使用 "00"？

Answer 1

2021 更新:链接的问题已同时得到修复，您应该可以毫无问题地使用“0V”(或任何带前导数字的符号) .

---

令我惊讶的是，无法识别以数字开头的标记； I opened a GitHub issue on it .同时，我相信您可以使用的最接近的东西是范围符号(虽然它长一个字符):

Section test.
  Variable T : Type.
  Variable zero : T.
  Notation "0" := zero.
  
  Variable V : Type.
  Variable zeroV : V.
  
  Notation "0" := zeroV : V_scope.
  Delimit Scope V_scope with V.
  Check 0.   (* 0 : T *)
  Check 0%V. (* 0%V : V *)

---

编辑

正如@JasonGross 在评论中所建议的，您可以Bind Scope 对T 和 两种类型使用相同的符号0 V。不过，这在某些情况下可能会影响可读性。

Section test.
  Variable T : Type.
  Variable zero : T.
  Notation "0" := zero.

  Variable V : Type.
  Variable zeroV : V.

  Notation "0" := zeroV : V_scope.
  Delimit Scope V_scope with V.
  Bind Scope V_scope with V.
  Check 0.   (* 0 : T *)
  Check 0%V. (* 0%V : V *)
  
  Variable mult : T -> V -> V.
  Check mult 0 0.   (* mult 0 0 : V *)
  Check mult 0 0%V. (* mult 0 0 : V *)