Can you find function by type signature in Coq?

Question

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

当我的谷歌搜索没有产生任何结果时，我会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 *)