The rw_search tactic

rw_search attempts to solve an equality goal by repeatedly rewriting using lemmas from the library.

If no solution is found, the best sequence of rewrites found before maxHeartbeats elapses is returned.

The search is a best-first search, minimising the Levenshtein edit distance between the pretty-printed expressions on either side of the equality. (The strings are tokenized at spaces, separating delimiters (, ), [, ], and , into their own tokens.)

The implementation avoids completely computing edit distances where possible, only computing lower bounds sufficient to decide which path to take in the search.

Future improvements

We could call simp as an atomic step of rewriting.

The edit distance heuristic could be replaced by something else.

No effort has been made to choose the best tokenization scheme, and this should be investigated. Moreover, the Levenshtein distance function is customizable with different weights for each token, and it would be interesting to try optimizing these (or dynamically updating them, adding weight to tokens that persistently appear on one side of the equation but not the other.)

The rw_search tactic will rewrite by local hypotheses, but will not use local hypotheses to discharge side conditions. This limitation would need to be resolved in the rw? tactic first.

def Mathlib.Tactic.RewriteSearch.splitDelimiters (s : String) : List String

Separate a string into a list of strings by pulling off initial ( or ] characters, and pulling off terminal ), ], or , characters.

Equations

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

partial def Mathlib.Tactic.RewriteSearch.splitDelimiters.auxStart (s : String) (front : String.Pos) (pre : List String) : String.Pos × List String

Pull off leading delimiters.

partial def Mathlib.Tactic.RewriteSearch.splitDelimiters.auxEnd (s : String) (back : String.Pos) (suff : List String) : String.Pos × List String

Pull off trailing delimiters.

def Mathlib.Tactic.RewriteSearch.tokenize (e : Lean.Expr) : Lean.MetaM (List String)

Tokenize a string at whitespace, and then pull off delimiters.

Equations

• Mathlib.Tactic.RewriteSearch.tokenize e = do let __do_lift ← Lean.Meta.ppExpr e let s : String := __do_lift.pretty pure (List.map Mathlib.Tactic.RewriteSearch.splitDelimiters s.splitOn).flatten

structure Mathlib.Tactic.RewriteSearch.SearchNode : Type

Data structure containing the history of a rewrite search.

• mk' :: (
• history : Array (ℕ × Lean.Expr × Bool)

  The lemmas used so far.

• mctx : Lean.MetavarContext

  The metavariable context after rewriting. We carry this around so the search can safely backtrack.

• goal : Lean.MVarId

  The current goal.

• type : Lean.Expr

  The type of the current goal.

• ppGoal : String

  The pretty printed current goal.

• lhs : List String

  The tokenization of the left-hand-side of the current goal.

• rhs : List String

  The tokenization of the right-hand-side of the current goal.

• rfl? : Option Bool

  Whether the current goal can be closed by rfl (or none if this hasn't been test yet).

• dist? : Option ℕ

  The edit distance between the tokenizations of the two sides (or none if this hasn't been computed yet).

• )

def Mathlib.Tactic.RewriteSearch.SearchNode.editCost : Levenshtein.Cost String String ℕ

What is the cost for changing a token? Levenshtein.defaultCost just uses constant cost 1 for any token.

It may be interesting to try others. the only one I've experimented with so far is Levenshtein.stringLogLengthCost, which performs quite poorly!

Equations

• Mathlib.Tactic.RewriteSearch.SearchNode.editCost = Levenshtein.defaultCost

def Mathlib.Tactic.RewriteSearch.SearchNode.compute_rfl? (n : SearchNode) : Lean.MetaM SearchNode

Check whether a goal can be solved by rfl, and fill in the SearchNode.rfl? field.

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.compute_dist? (n : SearchNode) : SearchNode

Fill in the SearchNode.dist? field with the edit distance between the two sides.

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.toString (n : SearchNode) : Lean.MetaM String

Represent a search node as string, solely for debugging.

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.mk (history : Array (ℕ × Lean.Expr × Bool)) (goal : Lean.MVarId) (ctx : Option Lean.MetavarContext := none) : Lean.MetaM (Option SearchNode)

Construct a SearchNode.

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.init (goal : Lean.MVarId) : Lean.MetaM (Option SearchNode)

Construct an initial SearchNode from a goal.

Equations

• Mathlib.Tactic.RewriteSearch.SearchNode.init goal = Mathlib.Tactic.RewriteSearch.SearchNode.mk #[] goal

def Mathlib.Tactic.RewriteSearch.SearchNode.push (n : SearchNode) (expr : Lean.Expr) (symm : Bool) (k : ℕ) (g : Lean.MVarId) (ctx : Option Lean.MetavarContext := none) : Lean.MetaM (Option SearchNode)

Add an additional step to the SearchNode history.

Equations

• n.push expr symm k g ctx = Mathlib.Tactic.RewriteSearch.SearchNode.mk (n.history.push (k, expr, symm)) g ctx

def Mathlib.Tactic.RewriteSearch.SearchNode.lastIdx (n : SearchNode) : ℕ

Report the index of the most recently applied lemma, in the ordering returned by rw?.

Equations

• n.lastIdx = match n.history.back? with | some (k, snd) => k | none => 0

instance Mathlib.Tactic.RewriteSearch.SearchNode.instOrd : Ord SearchNode

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.penalty (n : SearchNode) : ℕ

A somewhat arbitrary penalty function. Note that n.lastIdx penalizes using later lemmas from a particular call to rw? at a node, but once we have moved on to the next node these penalties are "forgiven".

(You might in interpret this as encouraging the algorithm to "trust" the ordering provided by rw?.)

I tried out a various (positive) linear combinations of .history.size, .lastIdx, and .ppGoal.length (and also the .log2s of these).

• .lastIdx.log2 is quite good, and the best coefficient is around 1.
• .lastIdx / 10 is almost as good.
• .history.size makes things worse (similarly with .log2).
• .ppGoal.length makes little difference (similarly with .log2). Here testing consisting of running the current rw_search test suite, rejecting values for which any failed, and trying to minimize the run time reported by

lake build &&  \
time (lake env lean test/RewriteSearch/Basic.lean; \
  lake env lean test/RewriteSearch/Polynomial.lean)

With a larger test suite it might be worth running this minimization again, and considering other penalty functions.

(If you do this, please choose a penalty function which is in the interior of the region where the test suite works. I think it would be a bad idea to optimize the run time at the expense of fragility.)

Equations

• n.penalty = n.lastIdx.log2 + n.ppGoal.length.log2

@[reducible, inline]

abbrev Mathlib.Tactic.RewriteSearch.SearchNode.prio (n : SearchNode) : Thunk ℕ

The priority function for search is Levenshtein distance plus a penalty.

Equations

• n.prio = Thunk.pure n.penalty + { fn := fun (x : Unit) => levenshtein Mathlib.Tactic.RewriteSearch.SearchNode.editCost n.lhs n.rhs }

@[reducible, inline]

abbrev Mathlib.Tactic.RewriteSearch.SearchNode.estimator (n : SearchNode) : Type

We can obtain lower bounds, and improve them, for the Levenshtein distance.

Equations

• n.estimator = (Estimator.trivial n.penalty × LevenshteinEstimator Mathlib.Tactic.RewriteSearch.SearchNode.editCost n.lhs n.rhs)

def Mathlib.Tactic.RewriteSearch.SearchNode.rewrite (n : SearchNode) (r : Lean.Meta.Rewrites.RewriteResult) (k : ℕ) : Lean.MetaM (Option SearchNode)

Given a RewriteResult from the rw? tactic, create a new SearchNode with the new goal.

Equations

• n.rewrite r k = Lean.Meta.withMCtx r.mctx do let goal' ← n.goal.replaceTargetEq r.result.eNew r.result.eqProof let __do_lift ← Lean.getMCtx n.push r.expr r.symm k goal' (some __do_lift)

def Mathlib.Tactic.RewriteSearch.SearchNode.rewrites (hyps : Array (Lean.Expr × Bool × ℕ)) (lemmas : Lean.Meta.LazyDiscrTree.ModuleDiscrTreeRef (Lean.Name × Lean.Meta.Rewrites.RwDirection)) (forbidden : Lean.NameSet := ∅) (n : SearchNode) : MLList Lean.MetaM SearchNode

Given a pair of DiscrTree trees indexing all rewrite lemmas in the imported files and the current file, try rewriting the current goal in the SearchNode by one of them, returning a MLList MetaM SearchNode, i.e. a lazy list of next possible goals.

Equations

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

def Mathlib.Tactic.RewriteSearch.SearchNode.search (n : SearchNode) (stopAtRfl stopAtDistZero : Bool := true) (forbidden : Lean.NameSet := ∅) (maxQueued : Option ℕ := none) : MLList Lean.MetaM SearchNode

Perform best first search on the graph of rewrites from the specified SearchNode.

Equations

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

def Mathlib.Tactic.RewriteSearch.tacticRw_search_ : Lean.ParserDescr

rw_search attempts to solve an equality goal by repeatedly rewriting using lemmas from the library.

If no solution is found, the best sequence of rewrites found before maxHeartbeats elapses is returned.

The search is a best-first search, minimising the Levenshtein edit distance between the pretty-printed expressions on either side of the equality. (The strings are tokenized at spaces, separating delimiters (, ), [, ], and , into their own tokens.)

You can use rw_search [-my_lemma, -my_theorem] to prevent rw_search from using the names theorems.

Equations

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