Documentation

Lean.Meta.Tactic.LibrarySearch

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?
def Lean.Meta.LibrarySearch.solveByElim (required : List Expr) (exfalso : Bool) (goals : List MVarId) (maxDepth : Nat) :

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

Equations
    Instances For

      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
        @[reducible]

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

        Equations
          Instances For

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

            Equations
              Instances For

                Create function for finding relevant declarations.

                Equations
                  Instances For

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

                    Equations
                      Instances For
                        def Lean.Meta.LibrarySearch.interleaveWith {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αγ) (x : Array α) (g : βγ) (y : Array β) :

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

                        Equations
                          Instances For
                            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
                              Instances For

                                Returns true if this is an abort speculation exception.

                                Equations
                                  Instances For
                                    @[reducible]

                                    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
                                      Instances For

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

                                        Equations
                                          Instances For

                                            Create lemma from name and mod.

                                            Equations
                                              Instances For

                                                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
                                                  Instances For
                                                    def Lean.Meta.LibrarySearch.librarySearch (goal : MVarId) (tactic : BoolList MVarIdMetaM (List MVarId) := fun (initial : Bool) (g : List MVarId) => solveByElim [] initial g 6) (allowFailure : MVarIdMetaM Bool := fun (x : MVarId) => pure true) (leavePercentHeartbeats : Nat := 10) :

                                                    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
                                                      Instances For