Module 4 · Lesson 4

Custom Tactics

Build your own tactics to automate repetitive proof patterns. Lean's metaprogramming system lets you extend the tactic language.

Why Custom Tactics?

When you find yourself writing the same proof patterns repeatedly, you can create a custom tactic that encapsulates that pattern.

lean

1-- Instead of writing this pattern repeatedly:
2example (a b c : Nat) (h1 : a = b) (h2 : b = c) : a = c := by
3  rw [h1, h2]
4
5-- Create a tactic that handles it automatically

Simple Tactic Macros

lean

1-- The simplest way: macro syntax
2macro "my_trivial" : tactic => `(tactic| trivial)
3
4example : True := by my_trivial
5
6-- With parameters
7macro "my_simp" n:term : tactic => `(tactic| simp [$n])
8
9example (h : a = b) : a = b := by my_simp h

Key Takeaway

macro creates simple tactic abbreviations. For complex logic, use elab or theTactic monad.

Combining Tactics

lean

1-- Macro for a common pattern
2macro "finish" : tactic => `(tactic| 
3  first
4  | rfl
5  | simp
6  | trivial
7  | assumption
8)
9
10example : 1 + 1 = 2 := by finish
11example (h : P) : P := by finish

The TacticM Monad

lean

1import Lean
2open Lean Elab Tactic
3
4-- For complex tactics, use TacticM
5elab "my_intro" : tactic => do
6  let goal ← getMainGoal
7  let (_, newGoal) ← goal.intro `h
8  replaceMainGoal [newGoal]
9
10-- Now my_intro works like intro
11example : P → P := by
12  my_intro
13  assumption

ℹ

Custom tactics using TacticM have full access to the proof state and can perform complex manipulations.

Reading the Goal

lean

1import Lean
2open Lean Elab Tactic Meta
3
4-- A tactic that prints goal information
5elab "show_goal" : tactic => do
6  let goal ← getMainGoal
7  let goalType ← goal.getType
8  logInfo m!"Goal: {goalType}"
9
10example : 1 + 1 = 2 := by
11  show_goal  -- Prints: Goal: 1 + 1 = 2
12  rfl

Working with Hypotheses

lean

1import Lean
2open Lean Elab Tactic Meta
3
4-- Find and use a hypothesis of the right type
5elab "exact_hyp" : tactic => do
6  let goal ← getMainGoal
7  let goalType ← goal.getType
8  let lctx ← getLCtx
9  for ldecl in lctx do
10    if ldecl.isImplementationDetail then continue
11    let declType := ldecl.type
12    if ← isDefEq declType goalType then
13      goal.assign ldecl.toExpr
14      return
15  throwError "No hypothesis matches the goal"

Deep Dive: Metaprogramming Architecture

Lean's metaprogramming is based on several monads:

CoreM — Basic environment access
MetaM — Type checking, unification
TermElabM — Term elaboration
TacticM — Tactic execution

Each builds on the previous, adding capabilities. Tactics typically run in TacticM.

Practical Example: repeat_on

lean

1import Lean
2open Lean Elab Tactic
3
4-- Apply a tactic to all goals
5syntax "all_goals" tactic : tactic
6
7macro_rules
8  | `(tactic| all_goals $t) => `(tactic| focus (repeat ($t)))
9
10-- Example usage
11example : True ∧ True ∧ True := by
12  constructor
13  constructor
14  all_goals trivial

Error Handling

lean

1import Lean
2open Lean Elab Tactic
3
4-- Tactics can fail gracefully
5elab "try_rfl" : tactic => do
6  try
7    evalTactic (← `(tactic| rfl))
8  catch _ =>
9    logInfo "rfl failed, trying simp"
10    evalTactic (← `(tactic| simp))
11
12example : 1 + 1 = 2 := by try_rfl
13example (h : a = b) : a = b := by try_rfl

Best Practices

lean

1-- 1. Start with macros for simple patterns
2macro "intro_and_split" : tactic => 
3  `(tactic| intro h; constructor)
4
5-- 2. Use elab for logic that needs goal inspection
6elab "smart_close" : tactic => do
7  first
8  | evalTactic (← `(tactic| rfl))
9  | evalTactic (← `(tactic| assumption))
10  | throwError "smart_close failed"
11
12-- 3. Document your tactics
13/-- Applies either rfl or assumption to close the goal. -/
14elab "close" : tactic => ...

Tactic Combinators Next: Mathlib Introduction