CODEWITHSUNDEEP
coq
SzymonPajzert
SzymonPajzert

Reputation: 732

Can you find function by type signature in Coq?

I'm looking for utility similar to one of Hoogle for Haskell. For the sake of example, let's say I need a function of signature forall n m:nat, n <> m -> m <> n.

When my Google searches don't yield any results, I write Definition foo: forall n m:nat, n <> m -> m <> n. and write intros; auto with arith. to prove it. But is there any way to not pollute my workspace with these temporary results and search for them based on their type? I'm sure I've seen this symmetry stated somewhere in standard library.

Upvotes: 6

Views: 708

Answers (1)

Tej Chajed
Tej Chajed

Reputation: 3948

There's a Search command that's somewhat similar to Hoogle, but a bit more precise. Here are some searches you might use for symmetry of not. In practice I would use the first and fall back to the second if there were a lot of results.

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 *)

Upvotes: 6

Related Questions