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.

Equations

• Except.emoji x = match x with | Except.error a => Lean.crossEmoji | Except.ok a => Lean.checkEmoji

def List.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.

Equations

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

structure Mathlib.Tactic.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 Mathlib.Tactic.backtrack (cfg : optParam Mathlib.Tactic.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 : optParam Lean.Name Lean.Name.anonymous) (alternatives : Lean.MVarId → Nondet Lean.MetaM (List Lean.MVarId)) (goals : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Attempts to solve the goals, by recursively calling alternatives g on each subgoal that appears. alternatives returns a nondeterministic list of new subgoals generated from a goal.

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

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.

Equations

• Mathlib.Tactic.backtrack cfg trace alternatives goals = Mathlib.Tactic.backtrack.processIndependentGoals cfg trace alternatives goals goals goals

partial def Mathlib.Tactic.backtrack.run (cfg : optParam Mathlib.Tactic.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 : optParam Lean.Name Lean.Name.anonymous) (alternatives : Lean.MVarId → Nondet Lean.MetaM (List Lean.MVarId)) (goals : List Lean.MVarId) (n : Nat) (curr : List Lean.MVarId) (acc : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

• 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 : List Lean.MVarId) => pure none, suspend := fun (x : Lean.MVarId) => pure false, discharge := fun (x : Lean.MVarId) => failure, commitIndependentGoals := false }) (trace : optParam Lean.Name Lean.Name.anonymous) (alternatives : Lean.MVarId → Nondet Lean.MetaM (List Lean.MVarId)) (goals : List Lean.MVarId) (goals : List Lean.MVarId) (remaining : List Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

A wrapper around run, which works on "independent" goals separately first, to reduce backtracking.

def Mathlib.Tactic.backtrack.ppMVarIds (gs : List Lean.MVarId) : Lean.MetaM (List Lean.Format)

Pretty print a list of goals.

Equations

• Mathlib.Tactic.backtrack.ppMVarIds gs = List.mapM (fun (g : Lean.MVarId) => do let __do_lift ← Lean.MVarId.getType g Lean.Meta.ppExpr __do_lift) gs