Generating a shortlist of candidate lemmas for suggestions

Discrimination tree lookup

This file defines how to build and match with the discrimination trees, for premises that are

• imported
• from the current module
• local hypotheses

Performance note

When importing all of mathlib, building the discrimination trees takes on the order of 10-15 seconds. This is because of two distinct performance bottlenecks:

1. Looping through the environment, and computing all of the discrimination tree entries is expensive, and is done in parallel to speed it up.
2. Building the final discrimination tree by inserting all of the computed entries is less expensive, but it cannot be done in parallel, because a single datastructure is being built.

These two bottlenecks cost about the same amount of time. Luckily, we can already start doing (2) as soon as any of the parallel tasks from (1) have finished. So, we build the discrimination tree (on the main thread) at the same time that the entries are being computed on various parallel threads.

structure Mathlib.Tactic.ClickSuggestions.Choice : Type

A choice of which discrimination trees to build.

• rw : Bool

  Build the rw discrimination tree?

• grw : Bool

  Build the grw discrimination tree?

• app : Bool

  Build the apply discrimination tree?

• appAt : Bool

  Build the apply at discrimination tree?

structure Mathlib.Tactic.ClickSuggestions.PreDiscrTrees : Type

Structure used for constructing the root nodes of the 4 discrimination trees.

• rw : Lean.Meta.RefinedDiscrTree.PreDiscrTree RwLemma

  The rw discrimination tree root.

• grw : Lean.Meta.RefinedDiscrTree.PreDiscrTree GrwLemma

  The grw discrimination tree root.

• app : Lean.Meta.RefinedDiscrTree.PreDiscrTree ApplyLemma

  The apply discrimination tree root.

• appAt : Lean.Meta.RefinedDiscrTree.PreDiscrTree ApplyAtLemma

  The apply at discrimination tree root.

opaque Mathlib.Tactic.ClickSuggestions.rwRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree RwLemma))

The global ref for looking up rw lemmas.

opaque Mathlib.Tactic.ClickSuggestions.grwRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree GrwLemma))

The global ref for looking up grw lemmas.

opaque Mathlib.Tactic.ClickSuggestions.appRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree ApplyLemma))

The global ref for looking up apply lemmas.

opaque Mathlib.Tactic.ClickSuggestions.appAtRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree ApplyAtLemma))

The global ref for looking up apply at lemmas.

def Mathlib.Tactic.ClickSuggestions.computeImportDiscrTrees (choice : Choice) : Lean.CoreM Unit

Compute the discrimination trees for import theorems.

Equations

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

def Mathlib.Tactic.ClickSuggestions.computeModuleDiscrTrees (choice : Choice) (parentDecl? : Option Lean.Name) : Lean.CoreM PreDiscrTrees

Compute the discrimination trees for the theorems in the current file.

Equations

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

def Mathlib.Tactic.ClickSuggestions.computeLCtxDiscrTrees (choice : Choice) (lctx : Lean.LocalContext) (fvarId? : Option Lean.FVarId) : Lean.MetaM PreDiscrTrees

Compute the discrimination trees for the local variables in lctx. We restrict to the varaibles in lctx to avoid using introduced bound variables.

Equations

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

def Mathlib.Tactic.ClickSuggestions.getImportMatches {α : Type} (ref : IO.Ref (Option (Lean.Meta.RefinedDiscrTree α))) (e : Lean.Expr) : Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)

Get the discrimination tree matches with theorems from imported files.

Equations

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

def Mathlib.Tactic.ClickSuggestions.getMatches {α : Type} (tree : Lean.Meta.RefinedDiscrTree α) (e : Lean.Expr) : Lean.MetaM (Lean.Meta.RefinedDiscrTree.MatchResult α)

Get the discrimination tree matches from tree.

Equations

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