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.

def Lean.MVarId.symmSaturate (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Equations

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

def Std.Tactic.tacticSymm_saturate : Lean.ParserDescr

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Equations

• Std.Tactic.tacticSymm_saturate = Lean.ParserDescr.node `Std.Tactic.tacticSymm_saturate 1024 (Lean.ParserDescr.nonReservedSymbol "symm_saturate" false)

def Std.Tactic.SolveByElim.applyTactics (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) (transparency : optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.default) (lemmas : List Lean.Expr) (g : Lean.MVarId) : Nondet Lean.MetaM (List Lean.MVarId)

applyTactics lemmas goal will return a list of tactics, corresponding to applying each one of the lemmas to the goal goal.

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.

def Std.Tactic.SolveByElim.applyFirst (cfg : optParam Lean.Meta.ApplyConfig { newGoals := Lean.Meta.ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, allowSynthFailures := false, approx := true }) (transparency : optParam Lean.Meta.TransparencyMode Lean.Meta.TransparencyMode.default) (lemmas : List Lean.Expr) (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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

• Std.Tactic.SolveByElim.applyFirst cfg transparency lemmas g = Nondet.head (Std.Tactic.SolveByElim.applyTactics cfg transparency lemmas g)

structure Std.Tactic.SolveByElim.ApplyRulesConfigextends Std.Tactic.BacktrackConfig , Lean.Meta.ApplyConfig : Type

The default maxDepth for apply_rules is higher.

• maxDepth : Nat
• proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
• suspend : Lean.MVarId → Lean.MetaM Bool
• discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
• commitIndependentGoals : Bool
• newGoals : Lean.Meta.ApplyNewGoals
• synthAssignedInstances : Bool
• allowSynthFailures : Bool
• approx : Bool
• transparency : Lean.Meta.TransparencyMode

  Transparency mode for calls to apply.

• symm : Bool

  Also use symmetric versions (via @[symm]) of local hypotheses.

• exfalso : Bool

  Try proving the goal via exfalso if solve_by_elim otherwise fails. This is only used when operating on a single goal.

structure Std.Tactic.SolveByElim.Configextends Std.Tactic.SolveByElim.ApplyRulesConfig : Type

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.

• maxDepth : Nat
• proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
• suspend : Lean.MVarId → Lean.MetaM Bool
• discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
• commitIndependentGoals : Bool
• newGoals : Lean.Meta.ApplyNewGoals
• synthAssignedInstances : Bool
• allowSynthFailures : Bool
• approx : Bool
• transparency : Lean.Meta.TransparencyMode
• symm : Bool
• exfalso : Bool
• backtracking : Bool

  Enable backtracking search.

• intro : Bool

  Trying calling intro if no lemmas apply.

• constructor : Bool

  Try calling constructor if no lemmas apply.

instance Std.Tactic.SolveByElim.instCoeConfigBacktrackConfig : Coe Std.Tactic.SolveByElim.Config Std.Tactic.BacktrackConfig

Equations

• Std.Tactic.SolveByElim.instCoeConfigBacktrackConfig = { coe := fun (x : Std.Tactic.SolveByElim.Config) => x.toApplyRulesConfig.toBacktrackConfig }

def Std.Tactic.SolveByElim.elabConfig : Lean.Syntax → Lean.Elab.TermElabM Std.Tactic.SolveByElim.Config

Allow elaboration of Config arguments to tactics.

Equations

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

def Std.Tactic.SolveByElim.elabApplyRulesConfig : Lean.Syntax → Lean.Elab.TermElabM Std.Tactic.SolveByElim.ApplyRulesConfig

Allow elaboration of ApplyRulesConfig arguments to tactics.

Equations

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

These functions could be lifted up to BacktrackConfig, but we'd still need to keep copies here.

def Std.Tactic.SolveByElim.Config.accept (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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.MVarId → Lean.MetaM Bool) : Std.Tactic.SolveByElim.Config

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.

def Std.Tactic.SolveByElim.Config.mainGoalProc (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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.MVarId → Lean.MetaM (List Lean.MVarId)) : Std.Tactic.SolveByElim.Config

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.

def Std.Tactic.SolveByElim.Config.intros (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) : Std.Tactic.SolveByElim.Config

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

Equations

• Std.Tactic.SolveByElim.Config.intros cfg = Std.Tactic.SolveByElim.Config.mainGoalProc cfg fun (g : Lean.MVarId) => do let __do_lift ← Lean.MVarId.intro1P g pure [__do_lift.snd]

def Std.Tactic.SolveByElim.Config.synthInstance (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) : Std.Tactic.SolveByElim.Config

Attempt typeclass inference on each goal, before applying lemmas.

Equations

• Std.Tactic.SolveByElim.Config.synthInstance cfg = Std.Tactic.SolveByElim.Config.mainGoalProc cfg fun (g : Lean.MVarId) => do Lean.MVarId.synthInstance g pure []

def Std.Tactic.SolveByElim.Config.withDischarge (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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.MVarId → Lean.MetaM (Option (List Lean.MVarId))) : Std.Tactic.SolveByElim.Config

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.

def Std.Tactic.SolveByElim.Config.introsAfter (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) : Std.Tactic.SolveByElim.Config

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

Equations

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

def Std.Tactic.SolveByElim.Config.constructorAfter (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) : Std.Tactic.SolveByElim.Config

Call constructor when no lemmas apply.

Equations

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

def Std.Tactic.SolveByElim.Config.synthInstanceAfter (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) : Std.Tactic.SolveByElim.Config

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

Equations

• Std.Tactic.SolveByElim.Config.synthInstanceAfter cfg = Std.Tactic.SolveByElim.Config.withDischarge cfg fun (g : Lean.MVarId) => do Lean.MVarId.synthInstance g pure (some [])

def Std.Tactic.SolveByElim.Config.testPartialSolutions (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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.Expr → Lean.MetaM Bool) : Std.Tactic.SolveByElim.Config

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.

def Std.Tactic.SolveByElim.Config.testSolutions (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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.Expr → Lean.MetaM Bool) : Std.Tactic.SolveByElim.Config

Create or modify a Config which rejects complete solutions 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.

def Std.Tactic.SolveByElim.Config.requireUsingAll (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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) : Std.Tactic.SolveByElim.Config

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

Equations

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

def Std.Tactic.SolveByElim.Config.processOptions (cfg : Std.Tactic.SolveByElim.Config) : Std.Tactic.SolveByElim.Config

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

Equations

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

def Std.Tactic.SolveByElim.elabContextLemmas (g : Lean.MVarId) (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (ctx : Lean.Elab.TermElabM (List Lean.Expr)) : Lean.MetaM (List Lean.Expr)

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.

def Std.Tactic.SolveByElim.applyLemmas (cfg : Std.Tactic.SolveByElim.Config) (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (ctx : Lean.Elab.TermElabM (List Lean.Expr)) (g : Lean.MVarId) : Nondet Lean.MetaM (List Lean.MVarId)

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.

def Std.Tactic.SolveByElim.applyFirstLemma (cfg : Std.Tactic.SolveByElim.Config) (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (ctx : Lean.Elab.TermElabM (List Lean.Expr)) (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Applies the first possible lemma to the goal.

Equations

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

def Std.Tactic.SolveByElim.solveByElim (cfg : Std.Tactic.SolveByElim.Config) (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (ctx : Lean.Elab.TermElabM (List Lean.Expr)) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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

Arguments:

• cfg : Config 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.

def Std.Tactic.SolveByElim.solveByElim.run (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (ctx : Lean.Elab.TermElabM (List Lean.Expr)) (cfg : Std.Tactic.SolveByElim.Config) : List Lean.MVarId → Lean.MetaM (List Lean.MVarId)

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.

def Lean.MVarId.applyRules (cfg : Std.Tactic.SolveByElim.Config) (lemmas : List (Lean.Elab.TermElabM Lean.Expr)) (only : optParam Bool false) (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

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.

def Std.Tactic.SolveByElim.mkAssumptionSet (noDefaults : Bool) (star : Bool) (add : List Lean.Term) (remove : List Lean.Term) (use : Array Lean.Ident) : Lean.MetaM (List (Lean.Elab.TermElabM Lean.Expr) × Lean.Elab.TermElabM (List Lean.Expr))

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 local_context, 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.

def Std.Tactic.SolveByElim.mkAssumptionSet.elab' (t : Lean.Term) : Lean.Elab.TermElabM Lean.Expr

Run elabTerm.

Equations

• Std.Tactic.SolveByElim.mkAssumptionSet.elab' t = Lean.Elab.Term.elabTerm t.raw none true true

def Std.Tactic.SolveByElim.erase : Lean.ParserDescr

Syntax for omitting a local hypothesis in solve_by_elim.

Equations

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

def Std.Tactic.SolveByElim.star : Lean.ParserDescr

Syntax for including all local hypotheses in solve_by_elim.

Equations

• Std.Tactic.SolveByElim.star = Lean.ParserDescr.nodeWithAntiquot "star" `Std.Tactic.SolveByElim.star (Lean.ParserDescr.symbol "*")

def Std.Tactic.SolveByElim.arg : Lean.ParserDescr

Syntax for adding or removing a term, or *, in solve_by_elim.

Equations

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

def Std.Tactic.SolveByElim.args : Lean.ParserDescr

Syntax for adding and removing terms in solve_by_elim.

Equations

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

def Std.Tactic.SolveByElim.using_ : Lean.ParserDescr

Syntax for using all lemmas labelled with an attribute in solve_by_elim.

Equations

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

def Std.Tactic.SolveByElim.parseArgs (s : Option (Lean.TSyntax `Std.Tactic.SolveByElim.args)) : Bool × List Lean.Term × List Lean.Term

Parse the lemma argument of a call to solve_by_elim. The first component should be true if * appears at least once. The second component should contain each term tin the arguments. The third component should contain t for each -t in the arguments.

Equations

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

def Std.Tactic.SolveByElim.parseUsing (s : Option (Lean.TSyntax `Std.Tactic.SolveByElim.using_)) : Array Lean.Ident

Parse the using ... argument for solve_by_elim.

Equations

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

def Std.Tactic.SolveByElim.solveByElimSyntax : Lean.ParserDescr

solve_by_elim calls apply on the main goal to find an assumption whose head matches and then repeatedly calls apply on the generated subgoals until no subgoals remain, performing at most maxDepth (defaults to 6) recursive steps.

solve_by_elim discharges the current goal or fails.

solve_by_elim performs backtracking if subgoals can not be solved.

By default, the assumptions passed to apply are the local context, rfl, trivial, congrFun and congrArg.

The assumptions can be modified with similar syntax as for simp:

• solve_by_elim [h₁, h₂, ..., hᵣ] also applies the given expressions.
• solve_by_elim only [h₁, h₂, ..., hᵣ] does not include the local context, rfl, trivial, congrFun, or congrArg unless they are explicitly included.
• solve_by_elim [-h₁, ... -hₙ] removes the given local hypotheses.
• solve_by_elim using [a₁, ...] uses all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

solve_by_elim* tries to solve all goals together, using backtracking if a solution for one goal makes other goals impossible. (Adding or removing local hypotheses may not be well-behaved when starting with multiple goals.)

Optional arguments passed via a configuration argument as solve_by_elim (config := { ... })

• maxDepth: number of attempts at discharging generated subgoals
• symm: adds all hypotheses derived by symm (defaults to true).
• exfalso: allow calling exfalso and trying again if solve_by_elim fails (defaults to true).
• transparency: change the transparency mode when calling apply. Defaults to .default, but it is often useful to change to .reducible, so semireducible definitions will not be unfolded when trying to apply a lemma.

See also the doc-comment for Std.Tactic.BacktrackConfig for the options proc, suspend, and discharge which allow further customization of solve_by_elim. Both apply_assumption and apply_rules are implemented via these hooks.

Equations

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

def Std.Tactic.SolveByElim.solveByElim.processSyntax (cfg : optParam Std.Tactic.SolveByElim.Config { toApplyRulesConfig := { toBacktrackConfig := { 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 }, toApplyConfig := { 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 }) (only : Bool) (star : Bool) (add : List Lean.Term) (remove : List Lean.Term) (use : Array Lean.Ident) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Wrapper for solveByElim that processes a list of Terms that specify the lemmas to use.

Equations

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

def Std.Tactic.SolveByElim.applyAssumptionSyntax : Lean.ParserDescr

apply_assumption looks for an assumption of the form ... → ∀ _, ... → head where head matches the current goal.

You can specify additional rules to apply using apply_assumption [...]. By default apply_assumption will also try rfl, trivial, congrFun, and congrArg. If you don't want these, or don't want to use all hypotheses, use apply_assumption only [...]. You can use apply_assumption [-h] to omit a local hypothesis. You can use apply_assumption using [a₁, ...] to use all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

apply_assumption will use consequences of local hypotheses obtained via symm.

If apply_assumption fails, it will call exfalso and try again. Thus if there is an assumption of the form P → ¬ Q, the new tactic state will have two goals, P and Q.

You can pass a further configuration via the syntax apply_rules (config := {...}) lemmas. The options supported are the same as for solve_by_elim (and include all the options for apply).

Equations

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

def Std.Tactic.SolveByElim.applyRulesSyntax : Lean.ParserDescr

apply_rules [l₁, l₂, ...] tries to solve the main goal by iteratively applying the list of lemmas [l₁, l₂, ...] or by applying a local hypothesis. If apply generates new goals, apply_rules iteratively tries to solve those goals. You can use apply_rules [-h] to omit a local hypothesis.

apply_rules will also use rfl, trivial, congrFun and congrArg. These can be disabled, as can local hypotheses, by using apply_rules only [...].

You can use apply_rules using [a₁, ...] to use all lemmas which have been labelled with the attributes aᵢ (these attributes must be created using register_label_attr).

You can pass a further configuration via the syntax apply_rules (config := {...}). The options supported are the same as for solve_by_elim (and include all the options for apply).

apply_rules will try calling symm on hypotheses and exfalso on the goal as needed. This can be disabled with apply_rules (config := {symm := false, exfalso := false}).

You can bound the iteration depth using the syntax apply_rules (config := {maxDepth := n}).

Unlike solve_by_elim, apply_rules does not perform backtracking, and greedily applies a lemma from the list until it gets stuck.

Equations

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