Point & click suggestions

This file defines #click_suggestions, a command that enables an interactive interface that gives lemma/tactic suggestions for any expression selected by the user.

The library search 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 (in parallel) to see whether it is applicable. For each lemma that works, the corresponding rw/apply/apply at/grw tactic is constructed, 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

• lemmas with fewer extra goals come first
• left-to-right rewrites come before right-to-left rewrites
• 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

• When selecting the whole goal, or a whole hypothesis, try running symm before library search.
• Improve user extensibility:
  • Modifying which tactics are suggested.
  • Modifying which lemmas are suggested.
• The n in nth_rw can be incorrect when the lemma has too many implicit arguments, such as add_pos_of_left or and_comm.
• When selecting multiple expressions, consider doing a rewrite at all these expressions.
• It may be possible to have integrated support for creating sequences of calc blocks, using the suggested rewrites.
• Detect whether we are in conv mode, by detecting the relevant mdata. Though the suggestions seem to work mostly fine in conv mode already.

def Mathlib.Tactic.ClickSuggestions.generateSuggestions (loc : Lean.SubExpr.GoalsLocation) (parentDecl? : Option Lean.Name) (token : ProofWidgets.RefreshToken) : ClickSuggestionsM Unit

Compute the suggestions. Use token for the output.

Equations

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

def Mathlib.Tactic.ClickSuggestions.rpc (props : ProofWidgets.PanelWidgetProps) : Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)

Rpc function for the #click_suggestions widget.

Equations

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

def Mathlib.Tactic.ClickSuggestions.clickSuggestionsComponent : ProofWidgets.Component ProofWidgets.PanelWidgetProps

The component called by the #click_suggestions command.

Equations

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

def Mathlib.Tactic.ClickSuggestions.«command#click_suggestions» : Lean.ParserDescr

#click_suggestions enables a widget in the infoview that gives tactic suggestions for the expression in the tactic state that was (most recently) selected with shift-click. Each suggestion has an insert button for pasting it into the editor, at the position of the cursor.

Theorems are searched for use in apply, apply at, rw and grw. These suggestions are grouped and sorted by the pattern that the 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 suggestions that create new goal(s) with metavariables in them. To see all suggestions, click on the filter button (▼) in the top right.

Equations

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