Documentation

Lean.Meta.Tactic.SolveByElim

solve_by_elim, apply_rules, and apply_assumption. #

solve_by_elim takes a collection of facts from the local context or supplied as arguments by the user, and performs a backtracking depth-first search by attempting to apply these facts to the goal.

It is a highly configurable tactic, with options to control the backtracking, to solve multiple goals simultaneously (with backtracking between goals), or to supply a discharging tactic for unprovable goals.

apply_rules and apply_assumption are much simpler tactics which do not perform backtracking, but are currently implemented in terms of solve_by_elim with backtracking disabled, in order to be able to share the front-end customisation and parsing of user options. It would be reasonable to further separate these in future.

applyTactics lemmas goal will return an iterator that applies the lemmas to the goal goal and returns ones that succeed.

Providing this to the backtracking tactic, we can perform backtracking search based on applying a list of lemmas.

applyTactics (trace := `name) will construct trace nodes for ``nameindicating which calls toapply` succeeded or failed.

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

    applyFirst lemmas goal applies the first of the lemmas which can be successfully applied to goal, and fails if none apply.

    We use this in apply_rules and apply_assumption where backtracking is not needed.

    Equations
    Instances For

      The default maxDepth for apply_rules is higher.

      Instances For

        Configuration structure to control the behaviour of solve_by_elim:

        • transparency mode for calls to apply
        • whether to use symm on hypotheses and exfalso on the goal as needed,
        • see also BacktrackConfig for hooks allowing flow control.
        Instances For
          def Lean.Meta.SolveByElim.SolveByElimConfig.accept (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (test : Lean.MVarIdLean.MetaM Bool) :

          Create or modify a Config which allows a class of goals to be returned as subgoals.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lean.Meta.SolveByElim.SolveByElimConfig.mainGoalProc (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (proc : Lean.MVarIdLean.MetaM (List Lean.MVarId)) :

            Create or modify a Config which runs a tactic on the main goal. If that tactic fails, fall back to the proc behaviour of cfg.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def Lean.Meta.SolveByElim.SolveByElimConfig.intros (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) :

              Create or modify a Config which calls intro on each goal before applying lemmas.

              Equations
              • cfg.intros = cfg.mainGoalProc fun (g : Lean.MVarId) => do let __do_liftg.intro1P pure [__do_lift.snd]
              Instances For
                def Lean.Meta.SolveByElim.SolveByElimConfig.synthInstance (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) :

                Attempt typeclass inference on each goal, before applying lemmas.

                Equations
                Instances For
                  def Lean.Meta.SolveByElim.SolveByElimConfig.withDischarge (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (discharge : Lean.MVarIdLean.MetaM (Option (List Lean.MVarId))) :

                  Add a discharging tactic, falling back to the original discharging tactic if it fails. Return none to return the goal as a new subgoal, or some goals to replace it.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Lean.Meta.SolveByElim.SolveByElimConfig.introsAfter (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) :

                    Create or modify a SolveByElimConfig which calls intro on any goal for which no lemma applies.

                    Equations
                    • cfg.introsAfter = cfg.withDischarge fun (g : Lean.MVarId) => do let __do_liftg.intro1P pure (some [__do_lift.snd])
                    Instances For
                      def Lean.Meta.SolveByElim.SolveByElimConfig.constructorAfter (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) :

                      Call constructor when no lemmas apply.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Lean.Meta.SolveByElim.SolveByElimConfig.synthInstanceAfter (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) :

                        Create or modify a Config which calls synthInstance on any goal for which no lemma applies.

                        Equations
                        Instances For
                          def Lean.Meta.SolveByElim.SolveByElimConfig.testPartialSolutions (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (test : List Lean.ExprLean.MetaM Bool) :

                          Create or modify a Config which rejects branches for which test, applied to the instantiations of the original goals, fails or returns false.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def Lean.Meta.SolveByElim.SolveByElimConfig.testSolutions (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (test : List Lean.ExprLean.MetaM Bool) :

                            Create or modify a SolveByElimConfig which rejects complete solutions for which test, applied to the instantiations of the original goals, fails or returns false.

                            Equations
                            Instances For
                              def Lean.Meta.SolveByElim.SolveByElimConfig.requireUsingAll (cfg : optParam Lean.Meta.SolveByElim.SolveByElimConfig { maxDepth := 6, proc := fun (x x : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false, newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true, transparency := Lean.Meta.TransparencyMode.default, symm := true, exfalso := true, backtracking := true, intro := true, constructor := true }) (use : List Lean.Expr) :

                              Create or modify a Config which only accept solutions for which every expression in use appears as a subexpression.

                              Equations
                              Instances For

                                Process the intro and constructor options by implementing the discharger tactic.

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

                                  Elaborate a list of lemmas and local context. See mkAssumptionSet for an explanation of why this is needed.

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

                                    Returns the list of tactics corresponding to applying the available lemmas to the goal.

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

                                      Applies the first possible lemma to the goal.

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

                                        Solve a collection of goals by repeatedly applying lemmas, backtracking as necessary.

                                        Arguments:

                                        • cfg : SolveByElimConfig additional configuration options (options for apply, maximum depth, and custom flow control)
                                        • lemmas : List (TermElabM Expr) lemmas to apply. These are thunks in TermElabM to avoid stuck metavariables.
                                        • ctx : TermElabM (List Expr) monadic function returning the local hypotheses to use.
                                        • goals : List MVarId the initial list of goals for solveByElim

                                        Returns a list of suspended goals, if it succeeded on all other subgoals. By default cfg.suspend is false, cfg.discharge fails, and cfg.failAtMaxDepth is true, and so the returned list is always empty. Custom wrappers (e.g. apply_assumption and apply_rules) may modify this behaviour.

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

                                          Run either backtracking search, or repeated application, on the list of goals.

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

                                            If symm is true, then adds in symmetric versions of each hypothesis.

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

                                              A MetaM analogue of the apply_rules user tactic.

                                              We pass the lemmas as TermElabM Expr rather than just Expr, so they can be generated fresh for each application, to avoid stuck metavariables.

                                              By default it uses all local hypotheses, but you can disable this with only := true. If you need to remove particular local hypotheses, call solveByElim directly.

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

                                                mkAssumptionSet builds a collection of lemmas for use in the backtracking search in solve_by_elim.

                                                • By default, it includes all local hypotheses, along with rfl, trivial, congrFun and congrArg.
                                                • The flag noDefaults removes these.
                                                • The flag star includes all local hypotheses, but not rfl, trivial, congrFun, or congrArg. (It doesn't make sense to use star without noDefaults.)
                                                • The argument add is the list of terms inside the square brackets that did not have - and can be used to add expressions or local hypotheses
                                                • The argument remove is the list of terms inside the square brackets that had a -, and can be used to remove local hypotheses. (It doesn't make sense to remove expressions which are not local hypotheses, to remove local hypotheses unless !noDefaults || star, and it does not make sense to use star unless you remove at least one local hypothesis.)

                                                mkAssumptionSet returns not a List expr, but a List (TermElabM Expr) × TermElabM (List Expr). There are two separate problems that need to be solved.

                                                Stuck metavariables #

                                                Lemmas with implicit arguments would be filled in with metavariables if we created the Expr objects immediately, so instead we return thunks that generate the expressions on demand. This is the first component, with type List (TermElabM Expr).

                                                As an example, we have def rfl : ∀ {α : Sort u} {a : α}, a = a, which on elaboration will become @rfl ?m_1 ?m_2.

                                                Because solve_by_elim works by repeated application of lemmas against subgoals, the first time such a lemma is successfully applied, those metavariables will be unified, and thereafter have fixed values. This would make it impossible to apply the lemma a second time with different values of the metavariables.

                                                See https://github.com/leanprover-community/mathlib/issues/2269

                                                Relevant local hypotheses #

                                                solve_by_elim* works with multiple goals, and we need to use separate sets of local hypotheses for each goal. The second component of the returned value provides these local hypotheses. (Essentially using getLocalHyps, along with some filtering to remove hypotheses that have been explicitly removed via only or [-h].)

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