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.

Equations
Instances For
    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.
    Instances For

      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.

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

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

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

      Instances For
        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.MVarIdNondet Lean.MetaM (List Lean.MVarId)) (goals : 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
        Instances For
          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.MVarIdNondet Lean.MetaM (List Lean.MVarId)) (goals : List Lean.MVarId) (n : Nat) (curr : List Lean.MVarId) (acc : 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.MVarIdNondet Lean.MetaM (List Lean.MVarId)) (goals : List Lean.MVarId) (goals : List Lean.MVarId) (remaining : List Lean.MVarId) :

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

          Pretty print a list of goals.

          Equations
          Instances For