coq – 从实现模块中的模块签名导入表示法

2019年8月4日 202次阅读

如何在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.

最佳答案 恐怕没有办法做到这一点. Coq中模块的状态很奇怪,这意味着模块类型与具有该类型的东西之间的唯一连接是Coq检查定义是否与签名兼容.模块内的Arrow声明实际上并不是一流的实体.因此,不应该有一种方法可以在签名中定义的符号与实现之间建立连接.我想到了两种选择：

>每次想要将它们用于新事物时,请重新声明您的注释.
>不要将模块用于ad-hoc多态.对于规范结构或类型类,多态操作确实在理论中具有一流的状态,从而更容易定义这样的通用符号.例如,在ssreflect：http://ssr.msr-inria.inria.fr/~jenkins/current/eqtype.html的eqtypes的==表示法的定义中查看.

点赞