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.

def Lean.MVarId.firstContinuation {α : Type} (results : Lean.MVarId → Nondet Lean.MetaM (List Lean.MVarId)) (cont : List Lean.MVarId → Lean.MetaM α) (g : Lean.MVarId) : Lean.MetaM α

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.

Equations

• Lean.MVarId.firstContinuation results cont g = Nondet.firstM (results g) fun r => Lean.observing? (cont r)

structure Mathlib.Tactic.BacktrackConfig : Type

• 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 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 : Lean.MVarId → Lean.MetaM Bool

  If suspend g, then we do not attempt to apply any further lemmas, 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 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.

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

Equations

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

def Mathlib.Tactic.backtrack (cfg : optParam Mathlib.Tactic.BacktrackConfig { maxDepth := 6, proc := fun x x => pure none, suspend := fun x => pure false, discharge := fun x => 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 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.

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 => pure none, suspend := fun x => pure false, discharge := fun x => 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 => pure none, suspend := fun x => pure false, discharge := fun x => 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)