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). The problem here is that we may generate lemmas that have as yet unspecified implicit arguments, and these implicit arguments would be filled in by metavariables if we created the actual expr objects now.

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.

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

A helper function to generate trace messages on successful applications.

A helper function to generate trace messages on unsuccessful applications.

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

The internal implementation of solve_by_elim, with a limiting counter.

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

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.

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.

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