coq - 你能在 Coq 中通过类型签名找到函数吗？

Question

我正在寻找类似于 Haskell 的 Hoogle 之一的实用程序。举例来说，假设我需要一个签名函数 forall n m:nat, n <> m -> m <> n .

当我的 Google 搜索没有产生任何结果时，我会写 Definition foo: forall n m:nat, n <> m -> m <> n.并写 intros; auto with arith.证明这一点。但是有什么方法可以不让这些临时结果污染我的工作区并根据它们的类型搜索它们？我确定我在标准库的某处看到过这种对称性。

Answer 1

有一个 Search命令有点类似于 Hoogle，但更精确一些。以下是您可能用于非对称性的一些搜索。在实践中，如果有很多结果，我会使用第一个并回退到第二个。

Search (_ <> _). (* everything related to not equal *)
Search (?a <> ?b -> ?b <> ?a). (* exactly what you want -
    note that unlike Hoogle, you need to use ?a for a pattern variable *)
Search (?R ?a ?b -> ?R ?b ?a). (* this searches for any symmetry theorem;
    not terribly useful for it's cool that it works *)
Search not "_sym". (* if you know some of the theorem name you can use that, too *)