Point & click library rewriting

This file defines rw??, an interactive tactic that suggests rewrites for any expression selected by the user.

rw?? uses a (lazy) RefinedDiscrTree to lookup a list of candidate rewrite lemmas. It excludes lemmas that are automatically generated. Each lemma is then checked one by one to see whether it is applicable. For each lemma that works, the corresponding rewrite tactic is constructed and converted into a String that fits inside mathlib's 100 column limit, so that it can be pasted into the editor when selected by the user.

The RefinedDiscrTree lookup groups the results by match pattern and gives a score to each pattern. This is used to display the results in sections. The sections are ordered by this score. Within each section, the lemmas are sorted by

• rewrites with fewer extra goals come first
• left-to-right rewrites come first
• shorter lemma names come first
• shorter replacement expressions come first (when taken as a string)
• alphabetically ordered by lemma name

The lemmas are optionally filtered to avoid duplicate rewrites, or trivial rewrites. This is controlled by the filter button on the top right of the results.

When a rewrite lemma introduces new goals, these are shown after a ⊢.

TODO

Ways to improve rw??:

• Improve the logic around nth_rw and occurrences, and about when to pass explicit arguments to the rewrite lemma. For example, we could only pass explicit arguments if that avoids using nth_rw. Performance may be a limiting factor for this. Currently, the occurrence is computed by viewKAbstractSubExpr.
• Modify the interface to allow creating a whole rw [.., ..] chain, without having to go into the editor in between. For this to work, we will need a more general syntax, something like rw [..]??, which would be pasted into the editor.
• We could look for rewrites of partial applications of the selected expression. For example, when clicking on (f + g) x, there should still be an add_comm suggestion.

Ways to extend rw??:

• Support generalized rewriting (grw)
• Integrate rewrite search with the calc? widget so that a calc block can be created using just point & click.

Caching

structure Mathlib.Tactic.LibraryRewrite.RewriteLemma : Type

The structure for rewrite lemmas stored in the RefinedDiscrTree.

• name : Lean.Name

  The name of the lemma

• symm : Bool

  symm is true when rewriting from right to left

def Mathlib.Tactic.LibraryRewrite.instBEqRewriteLemma.beq : RewriteLemma → RewriteLemma → Bool

@[implicit_reducible]

instance Mathlib.Tactic.LibraryRewrite.instBEqRewriteLemma : BEq RewriteLemma

def Mathlib.Tactic.LibraryRewrite.instInhabitedRewriteLemma.default : RewriteLemma

@[implicit_reducible]

instance Mathlib.Tactic.LibraryRewrite.instInhabitedRewriteLemma : Inhabited RewriteLemma

@[implicit_reducible]

instance Mathlib.Tactic.LibraryRewrite.instToFormatRewriteLemma : Std.ToFormat RewriteLemma

def Mathlib.Tactic.LibraryRewrite.isMVarSwap (t s : Lean.Expr) : Bool

Return true if s and t are equal up to changing the MVarIds.

@[inline]

def Mathlib.Tactic.LibraryRewrite.eqOrIff? (e : Lean.Expr) : Option (Lean.Expr × Lean.Expr)

Extract the left and right-hand sides of an equality or iff statement.

def Mathlib.Tactic.LibraryRewrite.addRewriteEntry (name : Lean.Name) (cinfo : Lean.ConstantInfo) : Lean.MetaM (List (RewriteLemma × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))

Try adding the lemma to the RefinedDiscrTree.

def Mathlib.Tactic.LibraryRewrite.addLocalRewriteEntry (decl : Lean.LocalDecl) : Lean.MetaM (List ((Lean.FVarId × Bool) × List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry)))

Try adding the local hypothesis to the RefinedDiscrTree.

Computing the Rewrites

def Mathlib.Tactic.LibraryRewrite.getImportCandidates (e : Lean.Expr) : Lean.MetaM (Array (Array RewriteLemma))

Get all potential rewrite lemmas from the imported environment. By setting the librarySearch.excludedModules option, all lemmas from certain modules can be excluded.

def Mathlib.Tactic.LibraryRewrite.getModuleCandidates (e : Lean.Expr) : Lean.MetaM (Array (Array RewriteLemma))

Get all potential rewrite lemmas from the current file. Exclude lemmas from modules in the librarySearch.excludedModules option.

structure Mathlib.Tactic.LibraryRewrite.Rewrite : Type

A rewrite lemma that has been applied to an expression.

• symm : Bool

  symm is true when rewriting from right to left

• proof : Lean.Expr

  The proof of the rewrite

• replacement : Lean.Expr

  The replacement expression obtained from the rewrite

• stringLength : ℕ

  The size of the replacement when printed

• extraGoals : Array (Lean.MVarId × Lean.BinderInfo)

  The extra goals created by the rewrite

• makesNewMVars : Bool

  Whether the rewrite introduces a new metavariable in the replacement expression.

def Mathlib.Tactic.LibraryRewrite.checkRewrite (thm e : Lean.Expr) (symm : Bool) : Lean.MetaM (Option Rewrite)

If thm can be used to rewrite e, return the rewrite.

def Mathlib.Tactic.LibraryRewrite.checkAndSortRewriteLemmas (e : Lean.Expr) (rewrites : Array RewriteLemma) : Lean.MetaM (Array (Rewrite × Lean.Name))

Try to rewrite e with each of the rewrite lemmas, and sort the resulting rewrites.

def Mathlib.Tactic.LibraryRewrite.getImportRewrites (e : Lean.Expr) : Lean.MetaM (Array (Array (Rewrite × Lean.Name)))

Return all applicable library rewrites of e. Note that the result may contain duplicate rewrites. These can be removed with filterRewrites.

def Mathlib.Tactic.LibraryRewrite.getModuleRewrites (e : Lean.Expr) : Lean.MetaM (Array (Array (Rewrite × Lean.Name)))

Same as getImportRewrites, but for lemmas from the current file.

Rewriting by hypotheses

def Mathlib.Tactic.LibraryRewrite.getHypotheses (except : Option Lean.FVarId) : Lean.MetaM (Lean.Meta.RefinedDiscrTree (Lean.FVarId × Bool))

Construct the RefinedDiscrTree of all local hypotheses.

def Mathlib.Tactic.LibraryRewrite.getHypothesisRewrites (e : Lean.Expr) (except : Option Lean.FVarId) : Lean.MetaM (Array (Array (Rewrite × Lean.FVarId)))

Return all applicable hypothesis rewrites of e. Similar to getImportRewrites.

Filtering out duplicate lemmas

def Mathlib.Tactic.LibraryRewrite.getBinderInfos (fn : Lean.Expr) (args : Array Lean.Expr) : Lean.MetaM (Array Lean.BinderInfo)

Get the BinderInfos for the arguments of mkAppN fn args.

partial def Mathlib.Tactic.LibraryRewrite.isExplicitEq (t s : Lean.Expr) : Lean.MetaM Bool

Determine whether the explicit parts of two expressions are equal, and the implicit parts are definitionally equal.

@[specialize #[]]

def Mathlib.Tactic.LibraryRewrite.filterRewrites {α : Type} (e : Lean.Expr) (rewrites : Array α) (replacement : α → Lean.Expr) (makesNewMVars : α → Bool) : Lean.MetaM (Array α)

Filter out duplicate rewrites, reflexive rewrites or rewrites that have metavariables in the replacement expression.

User interface

def Mathlib.Tactic.LibraryRewrite.tacticSyntax (rw : Rewrite) (occ : Option ℕ) (loc : Option Lean.Name) : Lean.MetaM (Lean.TSyntax `tactic)

Return the rewrite tactic that performs the rewrite.

structure Mathlib.Tactic.LibraryRewrite.RewriteInterface : Type

The structure with all data necessary for rendering a rewrite suggestion

• symm : Bool

  symm is true when rewriting from right to left

• tactic : String

  The rewrite tactic string that performs the rewrite

• replacement : Lean.Expr

  The replacement expression obtained from the rewrite

• replacementString : String

  The replacement expression obtained from the rewrite

• extraGoals : Array Lean.Widget.CodeWithInfos

  The extra goals created by the rewrite

• prettyLemma : Lean.Widget.CodeWithInfos

  The lemma name with hover information

• lemmaType : Lean.Expr

  The type of the lemma

• makesNewMVars : Bool

  Whether the rewrite introduces new metavariables with the replacement.

def Mathlib.Tactic.LibraryRewrite.Rewrite.toInterface (rw : Rewrite) (name : Lean.Name ⊕ Lean.FVarId) (occ : Option ℕ) (loc : Option Lean.Name) (range : Lean.Lsp.Range) : Lean.MetaM RewriteInterface

Construct the RewriteInterface from a Rewrite.

inductive Mathlib.Tactic.LibraryRewrite.Kind : Type

The kind of rewrite

• hypothesis : Kind

  A rewrite with a local hypothesis

• fromFile : Kind

  A rewrite with a lemma from the current file

• fromCache : Kind

  A rewrite with a lemma from an imported file

def Mathlib.Tactic.LibraryRewrite.getRewriteInterfaces (e : Lean.Expr) (occ : Option ℕ) (loc : Option Lean.Name) (except : Option Lean.FVarId) (range : Lean.Lsp.Range) : Lean.MetaM (Array (Array RewriteInterface × Kind) × Array (Array RewriteInterface × Kind))

Return the Interfaces for rewriting e, both filtered and unfiltered.

def Mathlib.Tactic.LibraryRewrite.pattern {α : Type} (type : Lean.Expr) (symm : Bool) (k : Lean.Expr → Lean.MetaM α) : Lean.MetaM α

Render the matching side of the rewrite lemma. This is shown at the header of each section of rewrite results.

def Mathlib.Tactic.LibraryRewrite.renderRewrites (e : Lean.Expr) (results : Array (Array RewriteInterface × Kind)) (init : Option ProofWidgets.Html) (range : Lean.Lsp.Range) (doc : Lean.Server.FileWorker.EditableDocument) (showNames : Bool) : Lean.MetaM ProofWidgets.Html

Render the given rewrite results.

def Mathlib.Tactic.LibraryRewrite.rpc (props : SelectInsertParams) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

The rpc method of the rw?? widget.

def Mathlib.Tactic.LibraryRewrite.LibraryRewriteComponent : ProofWidgets.Component SelectInsertParams

The component called by the rw?? tactic

def Mathlib.Tactic.LibraryRewrite.tacticRw?? : Lean.ParserDescr

rw?? is an interactive tactic that suggests rewrites for any expression selected by the user. To use it, shift-click an expression in the goal or a hypothesis that you want to rewrite. Clicking on one of the rewrite suggestions will paste the relevant rewrite tactic into the editor.

The rewrite suggestions are grouped and sorted by the pattern that the rewrite lemmas match with. Rewrites that don't change the goal and rewrites that create the same goal as another rewrite are filtered out, as well as rewrites that have new metavariables in the replacement expression. To see all suggestions, click on the filter button (▼) in the top right.

def Mathlib.Tactic.LibraryRewrite.Rewrite.toMessageData (rw : Rewrite) (name : Lean.Name) : Lean.MetaM Lean.MessageData

Represent a Rewrite as MessageData.

def Mathlib.Tactic.LibraryRewrite.SectionToMessageData (sec : Array (Rewrite × Lean.Name) × Bool) : Lean.MetaM (Option Lean.MessageData)

Represent a section of rewrites as MessageData.

def Mathlib.Tactic.LibraryRewrite.rw??Command : Lean.ParserDescr

#rw?? e gives all possible rewrites of e. It is a testing command for the rw?? tactic

def Mathlib.Tactic.LibraryRewrite.elabrw??Command : Lean.Elab.Command.CommandElab

Elaborate a #rw?? command.