Sine Qua Non premise selection

This is an implementation of the "Sine Qua Non" premise selection algorithm, from "Sine Qua Non for Large Theory Reasoning" by Hodor and Voronkov.

It needs to be tuned and evaluated for Lean.

def Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTheorems (trigger : Name) : CoreM (List (Name × Float))

def Lean.LibrarySuggestions.SineQuaNon.sineQuaNon (names : NameSet) (maxSuggestions : Nat) (depthFactor : Float := 1.5) (frequencyWeight : Float := 1e-2) : MetaM (Array Suggestion)

This isn't exactly what's described in the paper.

We select theorems in a priority order, where the priority is 1.5 ^ (trigger depth) * Π (tolerances).

The 1.5 factor could be tuned.

def Lean.LibrarySuggestions.sineQuaNonSelector (depthFactor : Float := 1.5) : Selector