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

Equations

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

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

Return the consecutive unfoldings of e.

Equations

• Mathlib.Tactic.InteractiveUnfold.unfolds e = do let e' ← Lean.Meta.whnfCore e Mathlib.Tactic.InteractiveUnfold.unfolds.go e' (if (e == e') = true then #[] else #[e'])

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

Append the unfoldings of e to acc. Assume e is in whnfCore form.

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

Determine whether e contains no internal names.

Equations

• Mathlib.Tactic.InteractiveUnfold.isUserFriendly e = !e.foldConsts false fun (name : Lean.Name) (x : Bool) => x || name.isInternalDetail

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

Return the consecutive unfoldings of e that are user friendly.

Equations

• Mathlib.Tactic.InteractiveUnfold.filteredUnfolds e = do let __do_lift ← Mathlib.Tactic.InteractiveUnfold.unfolds e pure (Array.filter Mathlib.Tactic.InteractiveUnfold.isUserFriendly __do_lift)

def Mathlib.Tactic.mkRewrite (occ : Option Nat) (symm : Bool) (rewrite : String) (loc : Option Lean.Name) : String

Return the rewrite tactic string rw (config := ..) [← ..] at ..

Equations

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

def Mathlib.Tactic.pasteString (e : Lean.Expr) : Lean.MetaM String

Return a string of the expression suitable for pasting into the editor.

We ignore any options set by the user.

We set pp.universes to false because new universe level metavariables are not understood by the elaborator.

We set pp.unicode.fun to true as per Mathlib convention.

Equations

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

def Mathlib.Tactic.InteractiveUnfold.tacticString (e unfold : Lean.Expr) (occ : Option Nat) (loc : Option Lean.Name) : Lean.MetaM String

Return the tactic string that does the unfolding.

Equations

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

def Mathlib.Tactic.InteractiveUnfold.renderUnfolds (e : Lean.Expr) (occ : Option Nat) (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.

Equations

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

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

The component called by the unfold? tactic

Equations

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

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.

Equations

• Mathlib.Tactic.InteractiveUnfold.tacticUnfold? = Lean.ParserDescr.node `Mathlib.Tactic.InteractiveUnfold.tacticUnfold? 1024 (Lean.ParserDescr.nonReservedSymbol "unfold?" false)

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

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

Equations

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

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

Elaborate a #unfold? command.

Equations

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