Discoverability of globals

[elidupree]

The existing prototype is pretty good for discoverability of tactics. It doesn't yet approach discoverability of globals – for example, most proofs from the standard library will never be discovered (even if they happen to completely solve a goal through auto with *, you won't actually see the tactics, and the modules you didn't load won't be tried at all)

I believe Coq has various features for discovering globals, which I could use. The most naive approach is to apply and rewrite every global in sequence and show the ones that worked. That still doesn't take care of modules that aren't loaded (which is a complicated issue – there are presumably reasons I shouldn't implicitly tack the whole standard library onto the beginning of the file, and the standard library isn't even necessarily the only library I should be helping with discoverability for).

And a lot of things would want smarts (so as to not make the CPU waste lots of attempts or the user waste lots of effort reading useless goal changes), but general-purpose analysis of "what lemmas might be relevant for what goal types" is hard for a computer alone. There's probably some very interesting things I could do along the lines of "users contributing to hint databases"...