7.7. Custom Tactics🔗

Tactics are productions in the syntax category tactic. xref macro for syntax_cats 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 := by⊢ 0 ≤ 4
  rep (apply Nat.le.stepa.a.a.a⊢ Nat.le 0 0)
  apply Nat.le.reflAll 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, xref 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 (α := α) [] := byα:Type u⊢ IsEmpty [] tactic 'assumption' failed
α : Type u
⊢ IsEmpty []trivialα:Type u⊢ IsEmpty []

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 (α := α) [] := byα:Type u_1⊢ IsEmpty [] simp [IsEmpty]All goals completed! 🐙

macro_rules | `(tactic|trivial) => `(tactic|exact emptyIsEmpty)

example (α : Type u) : IsEmpty (α := α) [] := byα:Type u⊢ IsEmpty []
  trivialAll 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 := by⊢ 2 = 2
  rflAll goals completed! 🐙 <|||> apply And.intro

example : 2 = 2 := by⊢ 2 = 2
  apply And.intro <|||> rflAll 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.FVarId → TacticM Unit)
    (atTarget : TacticM Unit)
    (failed : Lean.MVarId → TacticM 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)

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 goals collection.

def

Lean.Elab.Tactic.closeMainGoalUsing
  (tacName : Lean.Name)
  (x : Lean.Expr → TacticM Lean.Expr)
  (checkUnassigned : Bool := true) :
  TacticM Unit

Try to close main goal using x target, where target is the type of the main goal.

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) :
  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 main goal's tag. If multiple unnamed goals are encountered, tagSuffix is appended to the main goal's 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.Exception → TacticM α) : TacticM α

def

Lean.Elab.Tactic.liftMetaMAtMain {α : Type}
    (x : Lean.MVarId → Lean.MetaM α) : TacticM α

def

Lean.Elab.Tactic.getMainModule
    : TacticM Lean.Name

def

Lean.Elab.Tactic.orElse {α : Type}
    (x : TacticM α) (y : Unit → TacticM α)
    : TacticM α

7.7.2.6.2. Macro Expansion

def

Lean.Elab.Tactic.getCurrMacroScope
    : TacticM Lean.MacroScope

def

Lean.Elab.Tactic.adaptExpander
    (exp : Lean.Syntax → TacticM 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.Syntax →
      Lean.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.Syntax →
      Lean.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)