Interactive unfolding

This file defines the interactive tactic unfold?. It allows you to shift-click on an expression in the goal, and then it suggests rewrites to replace the expression with an unfolded version.

It can be used on its own, but it can also be used as part of the library rewrite tactic rw??, where these unfoldings are a subset of the suggestions.

For example, if the goal contains 1+1, then it will suggest rewriting this into one of

• Nat.add 1 1
• 2

Clicking on a suggestion pastes a rewrite into the editor, which will be of the form

• rw [show 1+1 = Nat.add 1 1 from rfl]
• rw [show 1+1 = 2 from rfl] It also takes into account the position of the selected expression if it appears in multiple places, and whether the rewrite is in the goal or a local hypothesis. The rewrite string is created using mkRewrite.

Reduction rules

The basic idea is to repeatedly apply unfoldDefinition? followed by whnfCore, which gives the list of all suggested unfoldings. Each suggested unfolding is in whnfCore normal form.

Additionally, eta-reduction is tried, and basic natural number reduction is tried.

Filtering

HAdd.hAdd in 1+1 actually first unfolds into Add.add, but this is not very useful, because this is just unfolding a notational type class. Therefore, unfoldings of default instances are not presented in the list of suggested rewrites. This is implemented with unfoldProjDefaultInst?.

Additionally, we don't want to unfold into expressions involving match terms or other constants marked as Name.isInternalDetail, and we don't want raw projections. So, all such results are filtered out. This is implemented with isUserFriendly.

def Mathlib.Tactic.InteractiveUnfold.unfoldProjDefaultInst? (e : Lean.Expr) : Lean.MetaM (Option Lean.Expr)

Unfold a class projection if the instance is tagged with @[default_instance]. This is used in the unfold? tactic in order to not show these unfolds to the user. Similar to Lean.Meta.unfoldProjInst?.

def Mathlib.Tactic.InteractiveUnfold.unfolds (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Return the consecutive unfoldings of e.

partial def Mathlib.Tactic.InteractiveUnfold.isUserFriendly (e : Lean.Expr) : Lean.MetaM Bool

Determine whether e contains no internal names or raw projections. We only consider the explicit parts of e, because it may happen that an instance implicit argument is marked as an internal detail, but that is not a problem.

def Mathlib.Tactic.InteractiveUnfold.filteredUnfolds (e : Lean.Expr) : Lean.MetaM (Array Lean.Expr)

Return the consecutive unfoldings of e that are user friendly.

def Mathlib.Tactic.mkRewrite (occ : Option ℕ) (symm : Bool) (e : Lean.Term) (loc : Option Lean.Name) : Lean.CoreM (Lean.TSyntax `tactic)

Return syntax for the rewrite tactic rw [e].

def Mathlib.Tactic.tacticPasteString (tac : Lean.TSyntax `tactic) (range : Lean.Lsp.Range) : Lean.CoreM String

Given tactic syntax tac that we want to paste into the editor, return it as a string. This function respects the 100 character limit for long lines.

def Mathlib.Tactic.InteractiveUnfold.tacticSyntax (e eNew : Lean.Expr) (occ : Option ℕ) (loc : Option Lean.Name) : Lean.MetaM (Lean.TSyntax `tactic)

Return the tactic string that does the unfolding.

def Mathlib.Tactic.InteractiveUnfold.renderUnfolds (e : Lean.Expr) (occ : Option ℕ) (loc : Option Lean.Name) (range : Lean.Lsp.Range) (doc : Lean.Server.FileWorker.EditableDocument) : Lean.MetaM (Option ProofWidgets.Html)

Render the unfolds of e as given by filteredUnfolds, with buttons at each suggestion for pasting the rewrite tactic. Return none when there are no unfolds.

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

The rpc method of the unfold? widget.

def Mathlib.Tactic.InteractiveUnfold.UnfoldComponent : ProofWidgets.Component SelectInsertParams

The component called by the unfold? tactic

def Mathlib.Tactic.InteractiveUnfold.tacticUnfold? : Lean.ParserDescr

Replace the selected expression with a definitional unfolding.

• After each unfolding, we apply whnfCore to simplify the expression.
• Explicit natural number expressions are evaluated.
• Unfolds of class projections of instances marked with @[default_instance] are not shown. This is relevant for notational type classes like +: we don't want to suggest Add.add a b as an unfolding of a + b. Similarly for OfNat n : Nat which unfolds into n : Nat.

To use unfold?, shift-click an expression in the tactic state. This gives a list of rewrite suggestions for the selected expression. Click on a suggestion to replace unfold? by a tactic that performs this rewrite.

def Mathlib.Tactic.InteractiveUnfold.unfoldCommand : Lean.ParserDescr

#unfold? e gives all unfolds of e. In tactic mode, use unfold? instead.

def Mathlib.Tactic.InteractiveUnfold.elabUnfoldCommand : Lean.Elab.Command.CommandElab

Elaborate a #unfold? command.