时间戳

首页 > 解决方案 > 如何在 Coq 中使用多个“0”表示法

coq - 如何在 Coq 中使用多个“0”表示法

问题描述

我在 Coq 中定义了域公理，并使用它们来证明这里描述的简单属性。然后，我添加了向量空间公理并在那里证明了简单的性质。由于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"？

标签： coq

解决方案

2021 年更新：链接问题已在此期间修复，您应该可以"0V"毫无问题地使用（或任何带前导数字的符号）。

令我惊讶的是，无法识别以数字开头的标记。我在上面打开了一个 GitHub 问题。同时，我相信您可以使用的最接近的东西是范围符号（尽管它长了一个字符）：

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对0类型T和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 *)

推荐阅读