# Documentation

Mathlib.Tactic.Backtrack

# backtrack#

A meta-tactic for running backtracking search, given a non-deterministic tactic alternatives : MVarId → Nondet MetaM (List MVarId).

backtrack alternatives goals will recursively try to solve all goals in goals, and the subgoals generated, backtracking as necessary.

In its default behaviour, it will either solve all goals, or fail. A customisable suspend hook in BacktrackConfig allows suspend a goal (or subgoal), so that it will be returned instead of processed further. Other hooks proc and discharge (described in BacktrackConfig) allow running other tactics before alternatives, or if all search branches from a given goal fail.

Currently only solveByElim is implemented in terms of backtrack.

def Except.emoji {ε : Type u_1} {α : Type u_2} :
Except ε αString

Visualize an Except using a checkmark or a cross.

Instances For
def List.tryAllM {m : Type (max u_1 u_2) → Type u_3} {α : Type u_2} {β : Type (max u_1 u_2)} [] [] (L : List α) (f : αm β) :
m (List α × List β)

Run a monadic function on every element of a list, returning the list of elements on which the function fails, and the list of successful results.

Instances For
def Lean.MVarId.firstContinuation {α : Type} (results : ) (cont : ) (g : Lean.MVarId) :

Given any tactic that takes a goal, and returns a sequence of alternative outcomes (each outcome consisting of a list of new subgoals), we can perform backtracking search by repeatedly applying the tactic.

Instances For
• maxDepth : Nat

Maximum recursion depth.

• proc :

An arbitrary procedure which can be used to modify the list of goals before each attempt to apply a lemma. Called as proc goals curr, where goals are the original goals for backtracking, and curr are the current goals. Returning some l will replace the current goals with l and recurse (consuming one step of maximum depth). Returning none will proceed to applying lemmas without changing goals. Failure will cause backtracking. (defaults to none)

• suspend :

If suspend g, then we do not attempt to apply any further lemmas, but return g as a new subgoal. (defaults to false)

• discharge :

discharge g is called on goals for which no lemmas apply. If none we return g as a new subgoal. If some l, we replace g by l in the list of active goals, and recurse. If failure, we backtrack. (defaults to failure)

• commitIndependentGoals : Bool

If we solve any "independent" goals, don't fail.

Configuration structure to control the behaviour of backtrack:

• control the maximum depth and behaviour (fail or return subgoals) at the maximum depth,
• and hooks allowing
• modifying intermediate goals before running the external tactic,
• 'suspending' goals, returning them in the result, and
• discharging subgoals if the external tactic fails.
Instances For
Instances For
def Mathlib.Tactic.backtrack (cfg : optParam Mathlib.Tactic.BacktrackConfig { maxDepth := 6, proc := fun x x => pure none, suspend := fun x => , discharge := fun x => failure, commitIndependentGoals := false }) (trace : ) (alternatives : ) (goals : ) :

Attempts to solve the goals, by recursively calling alternatives g on each subgoal that appears. alternatives returns a nondeterministic list of goals (this is essentially a lazy list of List MVarId, with the extra state required to backtrack in MetaM).

backtrack performs a backtracking search, attempting to close all subgoals.

Further flow control options are available via the Config argument.

Instances For
partial def Mathlib.Tactic.backtrack.run (cfg : optParam Mathlib.Tactic.BacktrackConfig { maxDepth := 6, proc := fun x x => pure none, suspend := fun x => , discharge := fun x => failure, commitIndependentGoals := false }) (trace : ) (alternatives : ) (goals : ) (n : Nat) (curr : ) (acc : ) :
• n : Nat steps remaining.
• curr : List MVarId the current list of unsolved goals.
• acc : List MVarId a list of "suspended" goals, which will be returned as subgoals.
partial def Mathlib.Tactic.backtrack.processIndependentGoals (cfg : optParam Mathlib.Tactic.BacktrackConfig { maxDepth := 6, proc := fun x x => pure none, suspend := fun x => , discharge := fun x => failure, commitIndependentGoals := false }) (trace : ) (alternatives : ) (goals : ) (goals : ) (remaining : ) :