1

我正在尝试定义一个提供身份和组合的类。除了其他有用的实例（带有 nil 和连接的列表；与身份和组合的关系 ;-) ），我想要一个函数实例。

给定

Class Cat (C0 : Type) (C1 : C0 -> C0 -> Type) :=
  {   identity : forall a, C1 a a
  ;   compose : forall {a b c : C0}, C1 b c -> C1 a b -> C1 a c
  (*  snip: some laws  *)
  }.

我希望能够定义类似的东西

Instance Cat (->) := { ... }.

但是 Coq 中的操作符不是这样工作的。首先我假设->是一个符号，但Locate "_ -> _".声称这是一个Unknown notation. 使用fun a b => a -> b有点工作，但之后的类型看起来很有趣。

> Check (identity nat).
identity nat
     : (fun a b : Type => a -> b) nat nat

（同样适用Eval compute in，似乎它并没有简化类型。）我更喜欢更具可读性的identity nat : nat -> nat. （目前，对于我正在做的事情，这些类型变得不可读。）

有没有办法得到“原始”->或至少说服 Coq 给我更好的类型？

旁注：我正在构建很多Inductive表示评估语义的 s，我的目标是将“普通”编程语言的子集映射到 Coq 上并返回，转移安全约束并发挥作用。我被迫用不同的构造函数一遍又一遍地证明同样的事情，并希望这能让我一次又一次地证明东西。我相信类别是抽象这一点的正确方法。如果我错了，我会在此处包含此注释，也许有更好的方法可以回避整个->问题。

4

1 回答 1

2

我只能回答部分问题。->不是 and 之类的符号+，exists它{ ... | ... }内置在解析器中，例如forall. 语法a -> b等价于forall x:a, bwhen xis not free in b（我不知道它是否在所有情况下都等价，可能有 wherex不能出现的用法b，你必须使用->）。

原因是函数抽象和应用，以及执行它们的类型，是 Coq 的基础，它们不是从更原始的概念派生的。您不能直接使用fun、 应用程序->或forall，因为它们不是一流的对象。

话虽如此，类型类是一种专门处理应用程序的方法。我对它们不熟悉，所以我不知道是否有办法做你想做的事情。

于 2012-08-31T15:10:24.957 回答