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.ClickSuggestions.suggestUnfold (e : Lean.Expr) (rwKind : RwKind) : ClickSuggestionsM (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.ClickSuggestions.«command#unfold?_» : 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.