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))

Equations

• Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTheorems trigger = do let map ← Lean.LibrarySuggestions.SineQuaNon.sineQuaNonTriggerMap✝ pure (Std.TreeMap.getD map trigger [])

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.