7.7. Custom Tactics🔗

Tactics are productions in the syntax category tactic. Given the syntax of a tactic, the tactic interpreter is responsible for carrying out actions in the tactic monad TacticM, which is a wrapper around Lean's term elaborator that keeps track of the additional state needed to execute tactics. A custom tactic consists of an extension to the tactic category along with either:

  • a macro that translates the new syntax into existing syntax, or

  • an elaborator that carries out TacticM actions to implement the tactic.

7.7.1. Tactic Macros🔗

The easiest way to define a new tactic is as a macro that expands into already-existing tactics. Macro expansion is interleaved with tactic execution. The tactic interpreter first expands tactic macros just before they are to be interpreted. Because tactic macros are not fully expanded prior to running a tactic script, they can use recursion; as long as the recursive occurrence of the macro syntax is beneath a tactic that can be executed, there will not be an infinite chain of expansion.

Recursive tactic macro

This recursive implementation of a tactic akin to repeat is defined via macro expansion. When the argument $t fails, the recursive occurrence of rep is never invoked, and is thus never macro expanded.

syntax "rep" tactic : tactic macro_rules | `(tactic|rep $t) => `(tactic| first | $t; rep $t | skip) example : 0 4 := 04 rep (Nat.le 0 0) All goals completed! 🐙

Like other Lean macros, tactic macros are hygienic. References to global names are resolved when the macro is defined, and names introduced by the tactic macro cannot capture names from its invocation site.

When defining a tactic macro, it's important to specify that the syntax being matched or constructed is for the syntax category tactic. Otherwise, the syntax will be interpreted as that of a term, which will match against or construct an incorrect AST for tactics.

7.7.1.1. Extensible Tactic Macros🔗

Because macro expansion can fail, multiple macros can match the same syntax, allowing backtracking. Tactic macros take this further: even if a tactic macro expands successfully, if the expansion fails when interpreted, the tactic interpreter will attempt the next expansion. This is used to make a number of Lean's built-in tactics extensible—new behavior can be added to a tactic by adding a Lean.Parser.Command.macro_rules : commandmacro_rules declaration.

Extending trivial

The trivial, which is used by many other tactics to quickly dispatch subgoals that are not worth bothering the user with, is designed to be extended through new macro expansions. Lean's default trivial can't solve IsEmpty [] goals:

def IsEmpty (xs : List α) : Prop := ¬ xs [] example (α : Type u) : IsEmpty (α := α) [] := α:Type uIsEmpty [] α:Type uIsEmpty []

The error message is an artifact of trivial trying assumption last. Adding another expansion allows trivial to take care of these goals:

def emptyIsEmpty : IsEmpty (α := α) [] := α:Type u_1IsEmpty [] All goals completed! 🐙 macro_rules | `(tactic|trivial) => `(tactic|exact emptyIsEmpty) example (α : Type u) : IsEmpty (α := α) [] := α:Type uIsEmpty [] All goals completed! 🐙
Expansion Backtracking

Macro expansion can induce backtracking when the failure arises from any part of the expanded syntax. An infix version of first can be defined by providing multiple expansions in separate Lean.Parser.Command.macro_rules : commandmacro_rules declarations:

syntax tactic "<|||>" tactic : tactic macro_rules | `(tactic|$t1 <|||> $t2) => pure t1 macro_rules | `(tactic|$t1 <|||> $t2) => pure t2 example : 2 = 2 := 2 = 2 All goals completed! 🐙 <|||> apply And.intro example : 2 = 2 := 2 = 2 apply And.intro <|||> All goals completed! 🐙

Multiple Lean.Parser.Command.macro_rules : commandmacro_rules declarations are needed because each defines a pattern-matching function that will always take the first matching alternative. Backtracking is at the granularity of Lean.Parser.Command.macro_rules : commandmacro_rules declarations, not their individual cases.

7.7.2. The Tactic Monad🔗

Planned Content
  • Relationship to Lean.Elab.Term.TermElabM, Lean.Meta.MetaM

  • Overview of available effects

  • Checkpointing

Tracked at issue #67

🔗def
Lean.Elab.Tactic.Tactic : Type
🔗def
Lean.Elab.Tactic.TacticM (α : Type) : Type
🔗def
Lean.Elab.Tactic.run (mvarId : Lean.MVarId)
    (x : TacticM Unit)
    : Lean.Elab.TermElabM (List Lean.MVarId)
🔗def
Lean.Elab.Tactic.runTermElab {α : Type}
  (k : Lean.Elab.TermElabM α)
  (mayPostpone : Bool := false) : TacticM α

Runs a term elaborator inside a tactic.

This function ensures that term elaboration fails when backtracking, i.e., in first| tac term | other.

7.7.2.1. Control

🔗def
Lean.Elab.Tactic.tryTactic {α : Type}
    (tactic : TacticM α) : TacticM Bool
🔗def
Lean.Elab.Tactic.tryTactic? {α : Type}
    (tactic : TacticM α) : TacticM (Option α)

7.7.2.2. Expressions

🔗def
Lean.Elab.Tactic.ensureHasNoMVars
    (e : Lean.Expr) : TacticM Unit
🔗def
Lean.Elab.Tactic.getFVarId (id : Lean.Syntax)
    : TacticM Lean.FVarId
🔗def
Lean.Elab.Tactic.getFVarIds
    (ids : Array Lean.Syntax)
    : TacticM (Array Lean.FVarId)
🔗def
Lean.Elab.Tactic.sortMVarIdsByIndex
    {m : Type → Type} [Lean.MonadMCtx m]
    [Monad m] (mvarIds : List Lean.MVarId)
    : m (List Lean.MVarId)
🔗def
Lean.Elab.Tactic.sortMVarIdArrayByIndex
    {m : Type → Type} [Lean.MonadMCtx m]
    [Monad m] (mvarIds : Array Lean.MVarId)
    : m (Array Lean.MVarId)

7.7.2.3. Source Locations

🔗def
Lean.Elab.Tactic.withLocation (loc : Location)
    (atLocal : Lean.FVarIdTacticM Unit)
    (atTarget : TacticM Unit)
    (failed : Lean.MVarIdTacticM Unit)
    : TacticM Unit

Runs the given atLocal and atTarget methods on each of the locations selected by the given loc.

  • If loc is a list of locations, runs at each specified hypothesis (and finally the goal if is included), and fails if any of the tactic applications fail.

  • If loc is *, runs at the target first and then the hypotheses in reverse order. If atTarget closes the main goal, withLocation does not run atLocal. If all tactic applications fail, withLocation with call failed with the main goal mvar.

7.7.2.4. Goals

🔗def
Lean.Elab.Tactic.getGoals
    : TacticM (List Lean.MVarId)

Returns the list of goals. Goals may or may not already be assigned.

🔗def
Lean.Elab.Tactic.setGoals
    (mvarIds : List Lean.MVarId) : TacticM Unit
🔗def
Lean.Elab.Tactic.getMainGoal
    : TacticM Lean.MVarId

Return the first goal.

🔗def
Lean.Elab.Tactic.getMainTag : TacticM Lean.Name

Return the main goal tag.

🔗def
Lean.Elab.Tactic.closeMainGoal
  (tacName : Lean.Name) (val : Lean.Expr)
  (checkUnassigned : Bool := true) :
  TacticM Unit

Closes main goal using the given expression. If checkUnassigned == true, then val must not contain unassigned metavariables. Returns true if val was successfully used to close the goal.

🔗def
Lean.Elab.Tactic.focus {α : Type}
    (x : TacticM α) : TacticM α
🔗def
Lean.Elab.Tactic.tagUntaggedGoals
    (parentTag newSuffix : Lean.Name)
    (newGoals : List Lean.MVarId) : TacticM Unit

Use parentTag to tag untagged goals at newGoals. If there are multiple new untagged goals, they are named using <parentTag>.<newSuffix>_<idx> where idx > 0. If there is only one new untagged goal, then we just use parentTag

🔗def
Lean.Elab.Tactic.getUnsolvedGoals
    : TacticM (List Lean.MVarId)
🔗def
Lean.Elab.Tactic.pruneSolvedGoals : TacticM Unit
🔗def
Lean.Elab.Tactic.appendGoals
    (mvarIds : List Lean.MVarId) : TacticM Unit

Add the given goals at the end of the current list of goals.

🔗def
Lean.Elab.Tactic.closeMainGoalUsing
  (tacName : Lean.Name)
  (x :
    Lean.ExprLean.NameTacticM Lean.Expr)
  (checkNewUnassigned : Bool := true) :
  TacticM Unit

Try to close main goal using x target tag, where target is the type of the main goal and tag is its user name.

If checkNewUnassigned is true, then throws an error if the resulting value has metavariables that were created during the execution of x. If it is false, then it is the responsibility of x to add such metavariables to the goal list.

During the execution of x:

  • The local context is that of the main goal.

  • The goal list has the main goal removed.

  • It is allowable to modify the goal list, for example with Lean.Elab.Tactic.pushGoals.

On failure, the main goal remains at the front of the goal list.

7.7.2.5. Term Elaboration

🔗def
Lean.Elab.Tactic.elabTerm (stx : Lean.Syntax)
  (expectedType? : Option Lean.Expr)
  (mayPostpone : Bool := false) :
  TacticM Lean.Expr

Elaborate stx in the current MVarContext. If given, the expectedType will be used to help elaboration but not enforced (use elabTermEnsuringType to enforce an expected type).

🔗def
Lean.Elab.Tactic.elabTermEnsuringType
  (stx : Lean.Syntax)
  (expectedType? : Option Lean.Expr)
  (mayPostpone : Bool := false) :
  TacticM Lean.Expr

Elaborate stx in the current MVarContext. If given, the expectedType will be used to help elaboration and then a TypeMismatchError will be thrown if the elaborated type doesn't match.

🔗def
Lean.Elab.Tactic.elabTermWithHoles
  (stx : Lean.Syntax)
  (expectedType? : Option Lean.Expr)
  (tagSuffix : Lean.Name)
  (allowNaturalHoles : Bool := false)
  (parentTag? : Option Lean.Name := none) :
  TacticM (Lean.Expr × List Lean.MVarId)

Elaborates stx and collects the MVarIds of any holes that were created during elaboration.

With allowNaturalHoles := false (the default), any new natural holes (_) which cannot be synthesized during elaboration cause elabTermWithHoles to fail. (Natural goals appearing in stx which were created prior to elaboration are permitted.)

Unnamed MVarIds are renamed to share the tag parentTag? (or the main goal's tag if parentTag? is none). If multiple unnamed goals are encountered, tagSuffix is appended to this tag along with a numerical index.

Note:

  • Previously-created MVarIds which appear in stx are not returned.

  • All parts of elabTermWithHoles operate at the current MCtxDepth, and therefore may assign metavariables.

  • When allowNaturalHoles := true, stx is elaborated under withAssignableSyntheticOpaque, meaning that .syntheticOpaque metavariables might be assigned during elaboration. This is a consequence of the implementation.

7.7.2.6. Low-Level Operations

These operations are primarily used as part of the implementation of TacticM or of particular tactics. It's rare that they are useful when implementing new tactics.

7.7.2.6.1. Monad Class Implementations

These operations are exposed through standard Lean monad type classes.

🔗def
Lean.Elab.Tactic.tryCatch {α : Type}
    (x : TacticM α)
    (h : Lean.ExceptionTacticM α) : TacticM α

Non-backtracking try/catch.

🔗def
Lean.Elab.Tactic.liftMetaMAtMain {α : Type}
    (x : Lean.MVarIdLean.MetaM α) : TacticM α
🔗def
Lean.Elab.Tactic.getMainModule
    : TacticM Lean.Name
🔗def
Lean.Elab.Tactic.orElse {α : Type}
    (x : TacticM α) (y : UnitTacticM α)
    : TacticM α

7.7.2.6.2. Macro Expansion

🔗def
Lean.Elab.Tactic.getCurrMacroScope
    : TacticM Lean.MacroScope
🔗def
Lean.Elab.Tactic.adaptExpander
    (exp : Lean.SyntaxTacticM Lean.Syntax)
    : Tactic

Adapt a syntax transformation to a regular tactic evaluator.

7.7.2.6.3. Case Analysis

🔗def
Lean.Elab.Tactic.elabCasesTargets
    (targets : Array Lean.Syntax)
    : TacticM
      (Array Lean.Expr ×
        Array (Lean.Ident × Lean.FVarId))

7.7.2.6.4. Simplifier

🔗def
Lean.Elab.Tactic.elabSimpArgs
    (stx : Lean.Syntax)
    (ctx : Lean.Meta.Simp.Context)
    (simprocs : Lean.Meta.Simp.SimprocsArray)
    (eraseLocal : Bool) (kind : SimpKind)
    : TacticM ElabSimpArgsResult

Elaborate extra simp theorems provided to simp. stx is of the form "[" simpTheorem,* "]" If eraseLocal == true, then we consider local declarations when resolving names for erased theorems (- id), this option only makes sense for simp_all or * is used. When recover := true, try to recover from errors as much as possible so that users keep seeing the current goal.

🔗def
Lean.Elab.Tactic.elabSimpConfig
    (optConfig : Lean.Syntax) (kind : SimpKind)
    : Lean.Elab.TermElabM Lean.Meta.Simp.Config
🔗def
Lean.Elab.Tactic.elabSimpConfigCtxCore
    : Lean.SyntaxLean.Elab.TermElabM
        Lean.Meta.Simp.ConfigCtx
🔗def
Lean.Elab.Tactic.dsimpLocation'
    (ctx : Lean.Meta.Simp.Context)
    (simprocs : Lean.Meta.Simp.SimprocsArray)
    (loc : Location)
    : TacticM Lean.Meta.Simp.Stats

Implementation of dsimp?.

🔗def
Lean.Elab.Tactic.elabDSimpConfigCore
    : Lean.SyntaxLean.Elab.TermElabM Lean.Meta.DSimp.Config

7.7.2.6.5. Attributes

🔗
Lean.Elab.Tactic.tacticElabAttribute
    : Lean.KeyedDeclsAttribute Tactic
🔗unsafe def
Lean.Elab.Tactic.mkTacticAttribute
    : IO (Lean.KeyedDeclsAttribute Tactic)