This is a complicated problem. I know some Coq developers are trying to build a search tool, but the problem is there are many ways to state a theorem and you want to not only find statements that exactly correspond to your request, but also those that are convertible to it. And there it gets ugly.