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.

The trigger index is computed on first use from the imported library, using that library's symbol frequencies. No index is prepared during module export or stored in olean files. The first query may be expensive for large imported libraries. Index construction does not consume the caller's heartbeat budget, but can be interrupted.

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.