Search - math-comp/math-comp GitHub Wiki
Search tips, tricks, and gotchas
-
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 stringbij
. -
The
Search
command does not look inside definitions. This meansSearch (?x + ?y = ?y + ?x).
will not findaddnC
lemma, butSearch commutative addn.
will. Notice thatSearch commutative (_ + _).
won't help either. -
Search (~~ ?b -> ~~ ?c).
does not find the contraposition lemmas fromssrbool
because the search mechanism does not insertis_true
coercions. See issue #10808 to find out more. -
Search "contra" in ssrbool.
does not work ifssrbool
is imported frommathcomp
and notCoq
namespace. The same happens forssreflect
andssrfun
modules. UseSearch "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)
Require
d 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
).
Examples
-
To find a lemma saying that
?x - ?x = 0
one either has to know there isself_inverse
definition:Search self_inverse subn.
or use the following combination of patterns:Search subn 0 -1.
. Here,-1
is to exclude irrelevant entries with1
(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.