coq - 在实现模块中从模块签名导入符号

Question

如何使 Category 中定义的符号可用 HomCategory ?

Module Type Category.

  Parameter Object : Type.
  Parameter Arrow : Object -> Object -> Type.

  Infix "~>" := Arrow (at level 25) : category_scope.
  Open Scope category_scope.
  Delimit Scope category_scope with category.
  Bind Scope category_scope with Object Arrow.

  Variable id : forall a : Object, a ~> a.
  ...
End Category.

Module HomCategory <: Category.

  Definition Object := Type.
  Definition Arrow(a b : Object) := a -> b.

  Print Scope category_scope. (* Error: Scope category_scope is not declared. *)
  ...
End HomCategory.

Answer 1

恐怕真的没有办法做到这一点。 Coq 中模块的状态很奇怪，这意味着 Module Type 之间的唯一联系这种类型的东西是 Coq 检查定义是否与签名兼容。 Arrow模块内的声明并不是真正的一流实体。因此，不应该有一种方法可以在您的签名中定义的符号和您的实现之间建立联系。我想到了两种选择:

每当您想将它们用于新事物时，请重新声明您的符号。

不要将模块用于临时多态性。对于规范结构或类型类，多态操作在理论上确实具有一流的地位，从而更容易定义此类通用符号。例如查看 == 的定义。 eqtype 的符号ssreflect 中的 s:http://ssr.msr-inria.inria.fr/~jenkins/current/eqtype.html .