# Library search #

This file defines tactics `exact?` and `apply?`, (formerly known as `library_search`) and a term elaborator `exact?%` that tries to find a lemma solving the current goal (subgoals are solved using `solveByElim`).

    example : x < x + 1 := exact?%
    example : Nat := by exact?

source
def Lean.Meta.LibrarySearch.solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) :
MetaM (List MVarId)

Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with appropriate arguments for library search.

Equations

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

Instances For

source
inductive Lean.Meta.LibrarySearch.DeclMod :
Type

A "modifier" for a declaration.

- `none` indicates the original declaration,
- `mp` indicates that (possibly after binders) the declaration is an `↔`, and we want to consider the forward direction,
- `mpr` similarly, but for the backward direction.

- none : DeclMod

  the original declaration

- mp : DeclMod

  the forward direction of an `iff`

- mpr : DeclMod

  the backward direction of an `iff`

Instances For

source
instance Lean.Meta.LibrarySearch.instDecidableEqDeclMod :
DecidableEq DeclMod
Equations

- Lean.Meta.LibrarySearch.instDecidableEqDeclMod x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
instance Lean.Meta.LibrarySearch.instInhabitedDeclMod :
Inhabited DeclMod
Equations

- Lean.Meta.LibrarySearch.instInhabitedDeclMod = { default := Lean.Meta.LibrarySearch.instInhabitedDeclMod.default }

source
def Lean.Meta.LibrarySearch.instInhabitedDeclMod.default :
DeclMod
Equations

- Lean.Meta.LibrarySearch.instInhabitedDeclMod.default = Lean.Meta.LibrarySearch.DeclMod.none

Instances For

source
def Lean.Meta.LibrarySearch.instOrdDeclMod.ord :
DeclMod → DeclMod → Ordering
Equations

- Lean.Meta.LibrarySearch.instOrdDeclMod.ord x✝ y✝ = compare x✝.ctorIdx y✝.ctorIdx

Instances For

source
instance Lean.Meta.LibrarySearch.instOrdDeclMod :
Ord DeclMod
Equations

- Lean.Meta.LibrarySearch.instOrdDeclMod = { compare := Lean.Meta.LibrarySearch.instOrdDeclMod.ord }

source
instance Lean.Meta.LibrarySearch.instHashableDeclMod :
Hashable DeclMod
Equations

- Lean.Meta.LibrarySearch.instHashableDeclMod = { hash := Lean.Meta.LibrarySearch.instHashableDeclMod.hash }

source
def Lean.Meta.LibrarySearch.instHashableDeclMod.hash :
DeclMod → UInt64
Equations

- Lean.Meta.LibrarySearch.instHashableDeclMod.hash Lean.Meta.LibrarySearch.DeclMod.none = 0
- Lean.Meta.LibrarySearch.instHashableDeclMod.hash Lean.Meta.LibrarySearch.DeclMod.mp = 1
- Lean.Meta.LibrarySearch.instHashableDeclMod.hash Lean.Meta.LibrarySearch.DeclMod.mpr = 2

Instances For

source
@[reducible]
def Lean.Meta.LibrarySearch.CandidateFinder :
Type

LibrarySearch has an extension mechanism for replacing the function used to find candidate lemmas.

Equations

- Lean.Meta.LibrarySearch.CandidateFinder = (Lean.Expr → Lean.MetaM (Array (Lean.Name × Lean.Meta.LibrarySearch.DeclMod)))

Instances For

source
def Lean.Meta.LibrarySearch.droppedKeys :
List (List LazyDiscrTree.Key)

We drop `.star` and `Eq * * *` from the discriminator trees because they match too much.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.libSearchFindDecls :
Expr → MetaM (Array (Name × DeclMod))

Create function for finding relevant declarations.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.mkHeartbeatCheck (leavePercent : Nat) :
MetaM (MetaM Bool)

Return an action that returns true when the remaining heartbeats is less than the currently remaining heartbeats * leavePercent / 100.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.interleaveWith {α : Type u_1} {β : Type u_2} {γ : Type} (f : α → γ) (x : Array α) (g : β → γ) (y : Array β) :
Array γ

Interleave x y interleaves the elements of x and y until one is empty and then returns final elements in other list.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.abortSpeculation {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExcept Exception m] :
m α

Called to abort speculative execution in library search.

Equations

- Lean.Meta.LibrarySearch.abortSpeculation = throw (Lean.Exception.internal Lean.Meta.LibrarySearch.abortSpeculationId✝)

Instances For

source
def Lean.Meta.LibrarySearch.isAbortSpeculation :
Exception → Bool

Returns true if this is an abort speculation exception.

Equations

- Lean.Meta.LibrarySearch.isAbortSpeculation (Lean.Exception.internal id extra) = (id == Lean.Meta.LibrarySearch.abortSpeculationId✝)
- Lean.Meta.LibrarySearch.isAbortSpeculation x✝ = false

Instances For

source
@[reducible]
def Lean.Meta.LibrarySearch.Candidate :
Type

A library search candidate using symmetry includes the goal to solve, the metavar context for that goal, and the name and orientation of a rule to try using with goal.

Equations

- Lean.Meta.LibrarySearch.Candidate = ((Lean.MVarId × Lean.MetavarContext) × Lean.Name × Lean.Meta.LibrarySearch.DeclMod)

Instances For

source
def Lean.Meta.LibrarySearch.librarySearchSymm (searchFn : CandidateFinder) (goal : MVarId) :
MetaM (Array Candidate)

Run `searchFn` on both the goal and `symm` applied to the goal.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.mkLibrarySearchLemma (lem : Name) (mod : DeclMod) :
MetaM Expr

Create lemma from name and mod.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.tryOnEach (act : Candidate → MetaM (List MVarId)) (candidates : Array Candidate) :
MetaM (Option (Array (List MVarId × MetavarContext)))

Sequentially invokes a tactic `act` on each value in candidates on the current state.

The tactic `act` should return a list of meta-variables that still need to be resolved. If this list is empty, then no variables remain to be solved, and `tryOnEach` returns `none` with the environment set so each goal is resolved.

If the action throws an internal exception with the `abortSpeculationId` id then further computation is stopped and intermediate results returned. If any other exception is thrown, then it is silently discarded.

Equations

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

Instances For

source
def Lean.Meta.LibrarySearch.librarySearch (goal : MVarId) (tactic : Bool → List MVarId → MetaM (List MVarId) := fun (initial : Bool) (g : List MVarId) => solveByElim [] initial g 6) (allowFailure : MVarId → MetaM Bool := fun (x : MVarId) => pure true) (leavePercentHeartbeats : Nat := 10) :
MetaM (Option (Array (List MVarId × MetavarContext)))

Tries to solve the goal either by:

- calling `tactic true`
- or applying a library lemma then calling `tactic false` on the resulting goals.

Typically here `tactic` is `solveByElim`, with the `Bool` flag indicating whether it may retry with `exfalso`.

If it successfully closes the goal, returns `none`. Otherwise, it returns `some a`, where `a : Array (List MVarId × MetavarContext)`, with an entry for each library lemma which was successfully applied, containing a list of the subsidiary goals, and the metavariable context after the application.

(Always succeeds, and the metavariable context stored in the monad is reverted, unless the goal was completely solved.)

(Note that if `solveByElim` solves some but not all subsidiary goals, this is not currently tracked.)

Equations

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

Instances For