# 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`.

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

Instances For

source
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'])

Instances For

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

source
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

Instances For

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

Instances For

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

Return syntax for the rewrite tactic `rw [e]`.

Equations

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

Instances For

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

Equations

- Mathlib.Tactic.tacticPasteString tac range = do let __do_lift ← Lean.PrettyPrinter.ppTactic tac pure (__do_lift.pretty 100 range.start.character range.start.character)

Instances For

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

Return the tactic string that does the unfolding.

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For