Writing Custom Lean 4 Tactics with TacticM and MetaM

Tactics in Lean 4 are first-class metaprograms. Every tactic — simp, ring, omega, exact — is written in ordinary Lean 4 using the TacticM monad. This page shows you how to write your own.

The `TacticM` Monad

TacticM is defined in Lean.Elab.Tactic.Basic as:

-- From Lean.Elab.Tactic.Basic
abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
abbrev Tactic  := Syntax → TacticM Unit

It extends TermElabM (and thus MetaM and CoreM) with two additional pieces:

Context — the name of the current elaborator and whether error recovery is enabled.
State — the current list of open goals (goals : List MVarId).

Because TacticM extends TermElabM, you have the full power of MetaM available — unification, type inference, expression building — directly inside any tactic.

Getting and Setting Goals

open Lean Elab Tactic in

-- Read the current goal list (may include already-assigned goals)
def readGoals : TacticM (List MVarId) :=
  getGoals

-- Replace the entire goal list
def clearAllGoals : TacticM Unit :=
  setGoals []

-- Get unassigned goals only (pruning solved ones)
def readOpen : TacticM (List MVarId) :=
  getUnsolvedGoals

-- Replace the main goal with a new list
-- e.g., split one goal into two
def splitInto (new1 new2 : MVarId) : TacticM Unit :=
  replaceMainGoal [new1, new2]

getMainGoal throws an error if there are no goals. Always guard with getUnsolvedGoals if you’re not sure goals remain.

The `MVarId` API

Each goal is an MVarId — a metavariable ID. The key operations are all dot-notation methods on MVarId, most living in MetaM:

open Lean Meta in

-- Get the type of a goal
example (g : MVarId) : MetaM Expr := g.getType

-- Enter the local context of a goal
example (g : MVarId) : MetaM Unit :=
  g.withContext do
    -- free variables from the goal's local context are in scope here
    let lctx ← getLCtx
    lctx.forM fun decl => logInfo m!"{decl.userName} : {decl.type}"

-- Assign a proof term to a goal (closes it)
example (g : MVarId) (proof : Expr) : MetaM Unit :=
  g.assign proof

-- Introduce one binder, returning the new FVarId and remaining goal
example (g : MVarId) : MetaM (FVarId × MVarId) :=
  g.intro `h

-- Apply a term to the goal, producing new subgoals
example (g : MVarId) (lemma : Expr) : MetaM (List MVarId) :=
  g.apply lemma

-- Revert a free variable back into the goal type
example (g : MVarId) (fvarId : FVarId) : MetaM (Array FVarId × MVarId) :=
  g.revert #[fvarId]

`liftMetaTactic` and `liftMetaFinishingTactic`

The bridge from MetaM to TacticM is liftMetaTactic:

open Lean Elab Tactic in

-- liftMetaTactic: run a MetaM action on the main goal,
-- replace the main goal with the returned list of new goals
def applyLemma (lem : Expr) : TacticM Unit :=
  liftMetaTactic fun goal => goal.apply lem

-- liftMetaFinishingTactic: like liftMetaTactic but expects no remaining goals
def closingTactic (pf : Expr) : TacticM Unit :=
  liftMetaFinishingTactic fun goal => goal.assign pf

liftMetaTacticAux is the general version that also returns a value:

open Lean Elab Tactic in
-- @[inline] def liftMetaTacticAux (tac : MVarId → MetaM (α × List MVarId)) : TacticM α

Registering a Tactic with `elab_rules`

The standard way to define a new tactic:

import Lean

open Lean Elab Tactic

-- Step 1: declare the syntax
syntax (name := myTac) "my_tac" : tactic

-- Step 2: attach the elaborator
@[tactic myTac]
def evalMyTac : Tactic
  | `(tactic| my_tac) => do
      logInfo m!"my_tac fired, {(← getGoals).length} goals remain"
  | _ => throwUnsupportedSyntax

Or equivalently with elab_rules:

elab_rules : tactic
  | `(tactic| my_tac) => do
      logInfo m!"my_tac fired"

Tactic Combinators

Lean 4’s tactic framework has built-in combinators you can call from TacticM:

open Lean Elab Tactic in

-- Evaluate a tactic syntax node
-- evalTactic : Syntax → TacticM Unit

-- Apply a tactic to all goals by iterating over the goal list manually,
-- or use the `all_goals` tactic syntax: evalTactic (← `(tactic| all_goals $stx))

-- Apply a tactic to any goal that accepts it using `any_goals` tactic syntax:
-- evalTactic (← `(tactic| any_goals $stx))
-- Returns true if at least one goal was closed

-- Run a tactic without error recovery (hard failure)
-- withoutRecover : TacticM α → TacticM α

-- Save/restore tactic state for backtracking
-- Tactic.saveState : TacticM SavedState
-- SavedState.restore : SavedState → TacticM Unit

You can also invoke user-facing tactic syntax programmatically:

open Lean Elab Tactic in
-- Run `rfl` on the current goal
def tryRfl : TacticM Unit := do
  let stx ← `(tactic| rfl)
  evalTactic stx

-- Run `simp` with a list of lemmas
def trySimpWith (lemmas : Array Name) : TacticM Unit := do
  let lemStx ← lemmas.mapM fun n => `(Lean.Parser.Tactic.simpLemma| $(mkIdent n):ident)
  evalTactic (← `(tactic| simp [$lemStx,*]))

Example 1: `swap_goals` Tactic

A tactic that reverses the order of the goal list:

import Lean
open Lean Elab Tactic

syntax (name := swapGoals) "swap_goals" : tactic

@[tactic swapGoals]
def evalSwapGoals : Tactic
  | `(tactic| swap_goals) => do
      let goals ← getUnsolvedGoals
      setGoals goals.reverse
  | _ => throwUnsupportedSyntax

-- Usage
example : True ∧ False ∨ True := by
  apply Or.inl        -- goal: True ∧ False  (boring)
  swap_goals          -- won't help here, but demonstrates the combinator
  trivial

Example 2: Close `a = a` Goals with `rfl`

A tactic that scans all goals and closes any that are definitionally a = a:

import Lean
open Lean Elab Tactic Meta

syntax (name := closeRefl) "close_refl_goals" : tactic

@[tactic closeRefl]
def evalCloseRefl : Tactic
  | `(tactic| close_refl_goals) => do
      let goals ← getUnsolvedGoals
      let remaining ← goals.filterM fun g => do
        -- Enter the local context of this goal
        g.withContext do
          let ty ← g.getType
          -- Try to close it with `Eq.refl`
          try
            liftMetaTactic1 fun goal => do
              goal.refl  -- MVarId.refl tries to close the goal with rfl
              return none  -- goal closed
            return false   -- goal was closed, don't keep it
          catch _ =>
            return true    -- goal remains
      setGoals remaining
  | _ => throwUnsupportedSyntax

-- Usage
example (n : Nat) : n = n ∧ 1 + 1 = 2 := by
  constructor
  · close_refl_goals   -- closes n = n
  · norm_num

Using `Lean.Meta.Simp` from a Tactic

You can call simp programmatically via Meta.simp:

import Lean
open Lean Meta Elab Tactic Simp

def simpGoal (g : MVarId) (lemmas : Array Name) : MetaM (Option MVarId) := do
  let ctx ← mkSimpContext (← lemmas.foldlM (fun s n => do
    let e ← mkConstWithFreshMVarLevels n
    return s.addConst n) {}) false
  let (result, _) ← Lean.Meta.Simp.simp (← g.getType) ctx
  match result.expr with
  | .const ``True _ => do
      g.assign (← mkEqMPR result.proof? (mkConst ``True.intro))
      return none
  | newTy => do
      let newGoal ← mkFreshExprSyntheticOpaqueMVar newTy
      return some newGoal.mvarId!

For simpler use, call Lean.Elab.Tactic.simpTarget:

open Lean Elab Tactic in
def runSimp : TacticM Unit := do
  let goal ← getMainGoal
  let (_, newGoals) ← simpTarget goal {}
  setGoals newGoals

Accessing the Local Context

Inside g.withContext, you can iterate over hypotheses:

open Lean Meta in
def listHyps (g : MVarId) : MetaM Unit :=
  g.withContext do
    let lctx ← getLCtx
    for decl in lctx do
      if !decl.isAuxDecl then
        logInfo m!"{decl.userName} : {decl.type}"

Complete: A `trivial_eq` Tactic

Putting it all together — a tactic that closes goals of the form a = a (including under function application) using Eq.refl:

import Lean
open Lean Elab Tactic Meta

elab_rules : tactic
  | `(tactic| trivial_eq) => do
      liftMetaFinishingTactic fun goal => do
        goal.withContext do
          let ty ← goal.getType
          -- Check the goal is of the form t = t
          match ty with
          | .app (.app (.app (.const ``Eq _) _) lhs) rhs => do
              if ← isDefEq lhs rhs then
                goal.assign (← mkEqRefl lhs)
              else
                throwError "trivial_eq: {lhs} ≠ {rhs}"
          | _ =>
              throwError "trivial_eq: goal is not an equality"

-- Test
example (n : Nat) : n + 0 = n + 0 := by trivial_eq
example : [1, 2, 3] = [1, 2, 3] := by trivial_eq

Concepts

Elaboration

Interoperability

Writing Custom Lean 4 Tactics with TacticM and MetaM

The `TacticM` Monad

Getting and Setting Goals

The `MVarId` API

`liftMetaTactic` and `liftMetaFinishingTactic`

Registering a Tactic with `elab_rules`

Tactic Combinators

Example 1: `swap_goals` Tactic

Example 2: Close `a = a` Goals with `rfl`

Using `Lean.Meta.Simp` from a Tactic

Accessing the Local Context

Complete: A `trivial_eq` Tactic

Build docs developers (and LLMs) love

Concepts

Elaboration

Interoperability

Documentation Index

​The TacticM Monad

​Getting and Setting Goals

​The MVarId API

​liftMetaTactic and liftMetaFinishingTactic

​Registering a Tactic with elab_rules

​Tactic Combinators

​Example 1: swap_goals Tactic

​Example 2: Close a = a Goals with rfl

​Using Lean.Meta.Simp from a Tactic

​Accessing the Local Context

​Complete: A trivial_eq Tactic

Build docs developers (and LLMs) love

The `TacticM` Monad

Getting and Setting Goals

The `MVarId` API

`liftMetaTactic` and `liftMetaFinishingTactic`

Registering a Tactic with `elab_rules`

Tactic Combinators

Example 1: `swap_goals` Tactic

Example 2: Close `a = a` Goals with `rfl`

Using `Lean.Meta.Simp` from a Tactic

Accessing the Local Context

Complete: A `trivial_eq` Tactic