Search

Search command in Coq's reference manual.

Typical search pattern: Search "prefix" "suffix"* (symbol|pattern)* in library. See here for the MathComp naming conventions.

Search pattern. looks everywhere in lemmas. To only look in the conclusions of lemmas: Search concl:template.

Strings and pattern indications can be interleaved, the command: Search "bij" (_ =1 _). lists all the lemmas whose statement, including premises, features a =1 and whose name contains the string bij.

The Search command does not look inside definitions. This means Search (?x + ?y = ?y + ?x). will not find addnC lemma, but Search commutative addn. will. Notice that Search commutative (_ + _). won't help either.

Search (~~ ?b -> ~~ ?c). does not find the contraposition lemmas from ssrbool because the search mechanism does not insert is_true coercions. See issue #10808 to find out more.

Search "contra" in ssrbool. does not work if ssrbool is imported from mathcomp and not Coq namespace. The same happens for ssreflect and ssrfun modules. Use Search "contra" in ssr.ssrbool instead. See issue #206 for more detail.

Patterns with holes should be surrounded by parentheses: Search (_ + _)..

The Search tool looks only inside (directly or indirectly) Required modules.

There is no Hoogle-like API search engine for Coq at the moment. One cannot search for lemmas in some global environment, e.g. in the opam Coq ecosystem.

To filter out some unwanted results use - prefix: Search eq odd -coprime. This will search for all lemmas that are equations (eq) involving odd numbers (odd), excluding the lemmas about coprimality (-coprime).

To find a lemma saying that ?x - ?x = 0 one either has to know there is self_inverse definition: Search self_inverse subn. or use the following combination of patterns: Search subn 0 -1.. Here, -1 is to exclude irrelevant entries with 1 (S O), 2 (S (S O)), etc. as those contain zeros. In both cases one needs to know the name of the operation behind the - notation (subn).

A case study showing how to use the Search command to prove an arithmetic statement.