mathlib documentation

tactic.solve_by_elim

solve_by_elim #

A depth-first search backwards reasoner.

solve_by_elim takes a list of lemmas, and repeating tries to apply these against the goals, recursively acting on any generated subgoals.

It accepts a variety of configuration options described below, enabling

At present it has no "premise selection", and simply tries the supplied lemmas in order at each step of the search.

source
meta def tactic.solve_by_elim.mk_assumption_set (no_dflt : bool) (hs : list tactic.simp_arg_type) (attr : list name) :
tactic (list (tactic expr) × tactic (list expr))

mk_assumption_set 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, congr_fun and congr_arg.
  • The flag no_dflt removes these.
  • The argument hs is a list of simp_arg_types, and can be used to add, or remove, lemmas or expressions from the set.
  • The argument attr : list name adds all lemmas tagged with one of a specified list of attributes.

mk_assumption_set returns not a list expr, but a list (tactic expr) × tactic (list expr). There are two separate problems that need to be solved.

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].)

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 (tactic 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

As an optimisation, after we build the list of tactic exprs, we actually run them, and replace any that do not in fact produce metavariables with a simple return tactic.

source
meta structure tactic.solve_by_elim.basic_opt  :
Type

Configuration options for solve_by_elim.

  • accept : list expr → tactic unit determines whether the current branch should be explored. At each step, before the lemmas are applied, accept is passed the proof terms for the original goals, as reported by get_goals when solve_by_elim started. These proof terms may be metavariables (if no progress has been made on that goal) or may contain metavariables at some leaf nodes (if the goal has been partially solved by previous apply steps). If the accept tactic fails solve_by_elim aborts searching this branch and backtracks. By default accept := λ _, skip always succeeds. (There is an example usage in tests/solve_by_elim.lean.)
  • pre_apply : tactic unit specifies an additional tactic to run before each round of apply.
  • discharger : tactic unit specifies an additional tactic to apply on subgoals for which no lemma applies. If that tactic succeeds, solve_by_elim will continue applying lemmas on resulting goals.
source
meta def tactic.solve_by_elim.solve_by_elim_trace (n : ℕ) (f : format) :
tactic unit

A helper function for trace messages, prepending '....' depending on the current search depth.

source
meta def tactic.solve_by_elim.on_success (g : format) (n : ℕ) (e : expr) :
tactic unit

A helper function to generate trace messages on successful applications.

source
meta def tactic.solve_by_elim.on_failure (g : format) (n : ℕ) :
tactic unit

A helper function to generate trace messages on unsuccessful applications.

source
meta def tactic.solve_by_elim.trace_hooks (n : ℕ) :
tactic ((expr → tactic unit) × tactic unit)

A helper function to generate the tactic that print trace messages. This function exists to ensure the target is pretty printed only as necessary.

source
meta def tactic.solve_by_elim.solve_by_elim_aux (opt : tactic.solve_by_elim.basic_opt) (original_goals : list expr) (lemmas : list (tactic expr)) (ctx : tactic (list expr)) :
ℕ → tactic unit

The internal implementation of solve_by_elim, with a limiting counter.

source
meta structure tactic.solve_by_elim.opt  :
Type

Arguments for solve_by_elim:

  • By default solve_by_elim operates only on the first goal, but with backtrack_all_goals := true, it operates on all goals at once, backtracking across goals as needed, and only succeeds if it discharges all goals.
  • lemmas specifies the list of lemmas to use in the backtracking search. If none, solve_by_elim uses the local hypotheses, along with rfl, trivial, congr_arg, and congr_fun.
  • lemma_thunks provides the lemmas as a list of tactic expr, which are used to regenerate the expr objects to avoid binding metavariables. It should not usually be specified by the user. (If both lemmas and lemma_thunks are specified, only lemma_thunks is used.)
  • ctx_thunk is for internal use only: it returns the local hypotheses which will be used.
  • max_depth bounds the depth of the search.
source
meta def tactic.solve_by_elim.opt.get_lemma_thunks (opt : tactic.solve_by_elim.opt) :
tactic (list (tactic expr) × tactic (list expr))

If no lemmas have been specified, generate the default set (local hypotheses, along with rfl, trivial, congr_arg, and congr_fun).

source
meta def tactic.solve_by_elim (opt : tactic.solve_by_elim.opt := {to_basic_opt := {to_apply_any_opt := {to_apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, use_symmetry := tt, use_exfalso := tt}, accept := λ (_x : list expr), tactic.skip, pre_apply := tactic.skip, discharger := tactic.failed unit, max_depth := 3}, backtrack_all_goals := ff, lemmas := none (list expr), lemma_thunks := option.map (λ (l : list expr), list.map return l) none, ctx_thunk := tactic.local_context}) :
tactic unit

solve_by_elim repeatedly tries applying a lemma from the list of assumptions (passed via the opt argument), recursively operating on any generated subgoals, backtracking as necessary.

solve_by_elim succeeds only if it discharges the goal. (By default, solve_by_elim focuses on the first goal, and only attempts to solve that. With the option backtrack_all_goals := tt, it attempts to solve all goals, and only succeeds if it does so. With backtrack_all_goals := tt, solve_by_elim will backtrack a solution it has found for one goal if it then can't discharge other goals.)

If passed an empty list of assumptions, solve_by_elim builds a default set as per the interactive tactic, using the local_context along with rfl, trivial, congr_arg, and congr_fun.

To pass a particular list of assumptions, use the lemmas field in the configuration argument. This expects an option (list expr). In certain situations it may be necessary to instead use the lemma_thunks field, which expects a option (list (tactic expr)). This allows for regenerating metavariables for each application, which might otherwise get stuck.

See also the simpler tactic apply_rules, which does not perform backtracking.

source
meta def tactic.interactive.apply_assumption (lemmas : option (list expr) := none) (opt : tactic.apply_any_opt := {to_apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, use_symmetry := tt, use_exfalso := tt}) (tac : tactic unit := tactic.interactive.skip) :
tactic unit

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

If this fails, apply_assumption will call symmetry and try again.

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

Optional arguments:

  • lemmas: a list of expressions to apply, instead of the local constants
  • tac: a tactic to run on each subgoal after applying an assumption; if this tactic fails, the corresponding assumption will be rejected and the next one will be attempted.
source
meta def tactic.interactive.solve_by_elim (all_goals : interactive.parse (lean.parser.tk "*")?) (no_dflt : interactive.parse interactive.types.only_flag) (hs : interactive.parse tactic.simp_arg_list) (attr_names : interactive.parse interactive.types.with_ident_list) (opt : tactic.solve_by_elim.opt := {to_basic_opt := {to_apply_any_opt := {to_apply_cfg := {md := semireducible, approx := tt, new_goals := tactic.new_goals.non_dep_first, instances := tt, auto_param := tt, opt_param := tt, unify := tt}, use_symmetry := tt, use_exfalso := tt}, accept := λ (_x : list expr), tactic.skip, pre_apply := tactic.skip, discharger := tactic.failed unit, max_depth := 3}, backtrack_all_goals := ff, lemmas := none (list expr), lemma_thunks := option.map (λ (l : list expr), list.map return l) none, ctx_thunk := tactic.local_context}) :
tactic unit

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 max_depth recursive steps.

solve_by_elim discharges the current goal or fails.

solve_by_elim performs back-tracking if subgoals can not be solved.

By default, the assumptions passed to apply are the local context, rfl, trivial, congr_fun and congr_arg.

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

  • solve_by_elim [h₁, h₂, ..., hᵣ] also applies the named lemmas.
  • solve_by_elim with attr₁ ... attrᵣ also applies all lemmas tagged with the specified attributes.
  • solve_by_elim only [h₁, h₂, ..., hᵣ] does not include the local context, rfl, trivial, congr_fun, or congr_arg unless they are explicitly included.
  • solve_by_elim [-id_1, ... -id_n] uses the default assumptions, removing the specified ones.

solve_by_elim* tries to solve all goals together, using backtracking if a solution for one goal makes other goals impossible.

optional arguments passed via a configuration argument as solve_by_elim { ... }

  • max_depth: number of attempts at discharging generated sub-goals
  • discharger: a subsidiary tactic to try at each step when no lemmas apply (e.g. cc may be helpful).
  • pre_apply: a subsidiary tactic to run at each step before applying lemmas (e.g. intros).
  • accept: a subsidiary tactic list expr → tactic unit that at each step, before any lemmas are applied, is passed the original proof terms as reported by get_goals when solve_by_elim started (but which may by now have been partially solved by previous apply steps). If the accept tactic fails, solve_by_elim will abort searching the current branch and backtrack. This may be used to filter results, either at every step of the search, or filtering complete results (by testing for the absence of metavariables, and then the filtering condition).