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.

structure Lean.Meta.Tactic.Backtrack.BacktrackConfig : Type

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.

• maxDepth : Nat

  Maximum recursion depth.

• proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))

  An arbitrary procedure which can be used to modify the list of goals before each attempt to generate alternatives. 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 generating alternative without changing goals. Failure will cause backtracking. (defaults to none)

• suspend : Lean.MVarId → Lean.MetaM Bool

  If suspend g, then we do not consider alternatives for g, but return g as a new subgoal. (defaults to false)

• discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))

  discharge g is called on goals for which there were no alternatives. 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. See Lean.MVarId.independent? for the definition of independence.

def Lean.Meta.Tactic.Backtrack.Backtrack.tryAllM {m : Type (max u_1 u_2) → Type u_3} {α : Type u_2} {β : Type (max u_1 u_2)} [Monad m] [Alternative m] (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.

def Lean.Meta.Tactic.Backtrack.backtrack (cfg : Lean.Meta.Tactic.Backtrack.BacktrackConfig := { 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 }) (trace : Lean.Name := Lean.Name.anonymous) (next : Lean.MVarId → Lean.MetaM (Lean.Meta.Iterator (List Lean.MVarId))) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Attempts to solve the goals, by recursively calling next on each subgoal that appears with a callback to reenter backtracking search.

Further flow control options are available via the Config argument.

Returns a list of subgoals which were "suspended" via the suspend or discharge hooks in Config. In the default configuration, backtrack will either return an empty list or fail.