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 usingnth_rw
. Performance may be a limiting factor for this. Currently, the occurrence is computed byviewKAbstractSubExpr
. - 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 likerw [..]??
, 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 anadd_comm
suggestion.
Ways to extend rw??
:
- Support generalized rewriting (
grw
) - Integrate rewrite search with the
calc?
widget so that acalc
block can be created using just point & click.
Caching #
Equations
- One or more equations did not get rendered due to their size.
Return true
if s
and t
are equal up to changing the MVarId
s.
Equations
Instances For
The main loop of isMVarSwap
. Returning none
corresponds to a failure.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Extract the left and right hand sides of an equality or iff statement.
Equations
Instances For
Try adding the lemma to the RefinedDiscrTree
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try adding the local hypothesis to the RefinedDiscrTree
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Computing the Rewrites #
Get all potential rewrite lemmas from the imported environment.
By setting the librarySearch.excludedModules
option, all lemmas from certain modules
can be excluded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Get all potential rewrite lemmas from the current file. Exclude lemmas from modules
in the librarySearch.excludedModules
option.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A rewrite lemma that has been applied to an expression.
- symm : Bool
symm
istrue
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 : Nat
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.
Instances For
If thm
can be used to rewrite e
, return the rewrite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to rewrite e
with each of the rewrite lemmas, and sort the resulting rewrites.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return all applicable library rewrites of e
.
Note that the result may contain duplicate rewrites. These can be removed with filterRewrites
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Same as getImportRewrites
, but for lemmas from the current file.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rewriting by hypotheses #
Construct the RefinedDiscrTree
of all local hypotheses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return all applicable hypothesis rewrites of e
. Similar to getImportRewrites
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Filtering out duplicate lemmas #
Get the BinderInfo
s for the arguments of mkAppN fn args
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Determine whether the explicit parts of two expressions are equal, and the implicit parts are definitionally equal.
Filter out duplicate rewrites, reflexive rewrites or rewrites that have metavariables in the replacement expression.
Equations
- One or more equations did not get rendered due to their size.
Instances For
User interface #
Return the rewrite tactic that performs the rewrite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure with all data necessary for rendering a rewrite suggestion
- symm : Bool
symm
istrue
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.
Instances For
Construct the RewriteInterface
from a Rewrite
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return the Interfaces for rewriting e
, both filtered and unfiltered.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Render the matching side of the rewrite lemma. This is shown at the header of each section of rewrite results.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Render the given rewrite results.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Render one section of rewrite results.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Render the list of rewrite results in one section.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The component called by the rw??
tactic
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- Mathlib.Tactic.LibraryRewrite.tacticRw?? = Lean.ParserDescr.node `Mathlib.Tactic.LibraryRewrite.tacticRw?? 1024 (Lean.ParserDescr.nonReservedSymbol "rw??" false)
Instances For
Represent a Rewrite
as MessageData
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
#rw?? e
gives all possible rewrites of e
. It is a testing command for the rw??
tactic
Equations
- One or more equations did not get rendered due to their size.
Instances For
Elaborate a #rw??
command.
Equations
- One or more equations did not get rendered due to their size.