Documentation

Mathlib.Tactic.Widget.LibraryRewrite

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

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??:

Ways to extend rw??:

Caching #

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

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

    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
        @[inline]

        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 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 : Nat

                    The size of the replacement when printed

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

                                  @[specialize #[]]
                                  def Mathlib.Tactic.LibraryRewrite.filterRewrites {α : Type} (e : Lean.Expr) (rewrites : Array α) (replacement : αLean.Expr) (makesNewMVars : αBool) :

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

                                      • The extra goals created by the rewrite

                                      • 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

                                          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

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

                                                          Represent a Rewrite as MessageData.

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

                                                            Represent a section of rewrites 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.
                                                                Instances For