The rewrites tactic.

rw? tries to find a lemma which can rewrite the goal.

rw? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as rw [h] or rw [←h].

Future work

We could try discharging side goals via assumption or solve_by_elim.

def Lean.Meta.RewriteResult.by? (r : Lean.Meta.RewriteResult) : Option Lean.Expr

Extract the lemma, with arguments, that was used to produce a RewriteResult.

Equations

• Lean.Meta.RewriteResult.by? r = if Lean.Expr.isAppOfArity r.eqProof `Eq.ndrec 6 = true then some (Lean.Expr.getArg! r.eqProof 5 (Lean.Expr.getAppNumArgs r.eqProof)) else none

def Mathlib.Tactic.Rewrites.forwardWeight : Nat

Weight to multiply the "specificity" of a rewrite lemma by when rewriting forwards.

Equations

• Mathlib.Tactic.Rewrites.forwardWeight = 2

def Mathlib.Tactic.Rewrites.backwardWeight : Nat

Weight to multiply the "specificity" of a rewrite lemma by when rewriting backwards.

Equations

• Mathlib.Tactic.Rewrites.backwardWeight = 1

def Mathlib.Tactic.Rewrites.processLemma (name : Lean.Name) (constInfo : Lean.ConstantInfo) : Lean.MetaM (Array (Array (Lean.Meta.DiscrTree.Key true) × Lean.Name × Bool × Nat))

Prepare the discrimination tree entries for a lemma.

Equations

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

def Mathlib.Tactic.Rewrites.localHypotheses (except : optParam (List Lean.FVarId) []) : Lean.MetaM (Array (Lean.Expr × Bool × Nat))

Select = and ↔ local hypotheses.

Equations

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

def Mathlib.Tactic.Rewrites.addLemma (name : Lean.Name) (constInfo : Lean.ConstantInfo) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) true) : Lean.MetaM (Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) true)

Insert a lemma into the discrimination tree.

Equations

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

def Mathlib.Tactic.Rewrites.buildDiscrTree : IO (Mathlib.Tactic.DiscrTreeCache (Lean.Name × Bool × Nat))

Construct the discrimination tree of all lemmas.

Equations

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

def Mathlib.Tactic.Rewrites.cachePath : IO System.FilePath

Equations

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

opaque Mathlib.Tactic.Rewrites.rewriteLemmas : Mathlib.Tactic.DiscrTreeCache (Lean.Name × Bool × Nat)

Retrieve the current cache of lemmas.

structure Mathlib.Tactic.Rewrites.RewriteResult : Type

• expr : Lean.Expr

  The lemma we rewrote by. This is Expr, not just a Name, as it may be a local hypothesis.

• symm : Bool

  True if we rewrote backwards (i.e. with rw [← h]).

• weight : Nat

  The "weight" of the rewrite. This is calculated based on how specific the rewrite rule was.

• result : Lean.Meta.RewriteResult

  The result from the rw tactic.

• ppResult? : Option String

  Pretty-printed result.

• rfl? : Option Bool

  Can the new goal in result be closed by with_reducible rfl?

• mctx : Lean.MetavarContext

  The metavariable context after the rewrite. This needs to be stored as part of the result so we can backtrack the state.

Data structure recording a potential rewrite to report from the rw? tactic.

def Mathlib.Tactic.Rewrites.RewriteResult.computeRfl (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Update a RewriteResult by filling in the rfl? field if it is currently none, to reflect whether the remaining goal can be closed by with_reducible rfl.

Equations

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

def Mathlib.Tactic.Rewrites.RewriteResult.prepare_ppResult (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Pretty print the result of the rewrite, and store it for later use.

Equations

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

def Mathlib.Tactic.Rewrites.RewriteResult.ppResult (r : Mathlib.Tactic.Rewrites.RewriteResult) : Lean.MetaM String

Pretty print the result of the rewrite. If this will be done more than once you should use prepare_ppResult

Equations

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

def Mathlib.Tactic.Rewrites.solveByElim (goals : List Lean.MVarId) (depth : optParam Nat 6) : Lean.MetaM PUnit

Shortcut for calling solveByElim.

Equations

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

def Mathlib.Tactic.Rewrites.rewritesCore {s : Bool} (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s) (ctx : Lean.MetavarContext) (goal : Lean.MVarId) (target : Lean.Expr) : MLList Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Find lemmas which can rewrite the goal.

This core function returns a monadic list, to allow the caller to decide how long to search. See also rewrites for a more convenient interface.

Equations

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

def Mathlib.Tactic.Rewrites.rewritesDedup {s : Bool} (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s) (mctx : Lean.MetavarContext) (goal : Lean.MVarId) (target : Lean.Expr) : MLList Lean.MetaM Mathlib.Tactic.Rewrites.RewriteResult

Find lemmas which can rewrite the goal, and deduplicate based on pretty-printed results. Note that this builds a HashMap containing the results, and so may consume significant memory.

Equations

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

def Mathlib.Tactic.Rewrites.rewrites {s : Bool} (hyps : Array (Lean.Expr × Bool × Nat)) (lemmas : Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s × Lean.Meta.DiscrTree (Lean.Name × Bool × Nat) s) (goal : Lean.MVarId) (target : Lean.Expr) (stopAtRfl : optParam Bool false) (max : optParam Nat 20) (leavePercentHeartbeats : optParam Nat 10) : Lean.MetaM (List Mathlib.Tactic.Rewrites.RewriteResult)

Find lemmas which can rewrite the goal.

Equations

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

def Mathlib.Tactic.Rewrites.rewrites' : Lean.ParserDescr

rw? tries to find a lemma which can rewrite the goal.

rw? should not be left in proofs; it is a search tool, like apply?.

Suggestions are printed as rw [h] or rw [←h].

Equations

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