Lean theorem prover/System/The tactic framework

Plain-language version: Tactics· Holes and goals

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

A tactic is a program that constructs part of a proof term. The tactic framework is what such programs act on: a list of goals, each one a metavariable, inside a monad that gives access to everything the elaborator can do. This page describes the framework in Lean 4.34.1: how a by block enters elaboration, what a goal is, the monad TacticM, the combinators that join tactics, a new tactic defined in three lines, and the library-search tactics exact? and apply?. The idea of a tactic goes back to the LCF system; LCF and the tactic idea tells that history.

A by block is a hole

The reference manual states that by tac constructs a term of the expected type by running the tactics tac, and that tactics construct proof terms behind the scenes. When the elaborator meets by, it does not run the tactics at once. It creates a metavariable of the expected type, of the synthetic opaque kind, and registers the tactic code to be run later. Tactic blocks are run in the last round of pending work, after the rest of the surrounding term has been elaborated as far as it can be, so that the goal's type is as complete as possible. The trace option trace.Elab.step shows both moments. These lines are an excerpt from the trace of example (p : Prop) (hp : p) : p ∧ p := by exact ⟨hp, hp⟩:

[Elab.step] ✅️ expected type: p ∧ p, term
    by exact ⟨hp, hp⟩
  [Elab.step.result] ?m.1
[Elab.step] ✅️ exact ⟨hp, hp⟩

The by term elaborates to the metavariable ?m.1. Only afterwards does the tactic exact run, and it is the tactic that assigns ?m.1.

Goals are metavariables

The state of the tactic framework is a structure with one field, goals : List MVarId. Each goal is a metavariable, with its own local context of hypotheses and its type, the statement still to be proved; the first is the main goal. A tactic usually acts on the main goal: it assigns that metavariable a term, which may contain new metavariables, and puts the new metavariables in the goal's place. The goal of a by block, and the goals made by tactics such as intro, are synthetic opaque, the kind that unification never assigns, because a goal counts as solved exactly when its metavariable is assigned. Metavariables and unification treats these kinds.

A short tactic that reads the list makes the point concrete:

import Lean
open Lean Elab Tactic in
elab "show_goals" : tactic => do
  let gs ← getGoals
  logInfo m!"goals: {gs.map Expr.mvar}"

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  show_goals
  all_goals assumption

It prints goals: [?left, ?right]. The tactic constructor assigned the original goal the term And.intro ?left ?right and left the two new metavariables as goals, named after the arguments of And.intro. The built-in trace_state prints the same goals in the familiar form:

theorem and_swap (p q : Prop) (h : p ∧ q) : q ∧ p := by
  constructor
  trace_state
  · exact h.2
  · exact h.1

#print and_swap

case left
p q : Prop
h : p ∧ q
⊢ q

case right
p q : Prop
h : p ∧ q
⊢ p
theorem and_swap : ∀ (p q : Prop), p ∧ q → q ∧ p :=
fun p q h => ⟨h.right, h.left⟩

The last lines are the point of the whole framework. Once every goal is assigned, the by block's metavariable stands for an ordinary term, and that term, not the script, is what the Lean kernel checks and what Lean's environment, its table of definitions and theorems, records. If a goal is left open, the block fails:

example (p q : Prop) (hp : p) : p ∧ q := by
  constructor
  exact hp

error: unsolved goals
case right
p q : Prop
hp : p
⊢ q

The monad TacticM

In Lean 4.34.1 the tactic monad is defined as

abbrev TacticM := ReaderT Context $ StateRefT State TermElabM

Its documentation describes it as the term elaboration monad TermElabM extended with the current goals and some local information, and defines a tactic as a function from syntax to an action in TacticM. Several tactics may be attached to one kind of syntax; they are attempted until one succeeds. Because TacticM sits on top of the elaborator, a tactic can do anything the elaborator does: elaborate a term against a goal, call the unifier, search for instances, inspect and extend Lean's environment. Monads and do-notation explains the monad stack, and metaprogramming in Lean shows how to write tactics against it. The paper that introduced Lean 4 stresses that tactics are implemented in Lean itself and can be added by users.

None of this is trusted. A tactic may be wrong in any way: it may assign a goal an ill-typed term, or a term of the wrong type. The error surfaces when the term is checked, at the latest by the Lean kernel (the Lean kernel).

Combinators

Tactics are joined by combinators, themselves tactics. Their documentation strings in Lean's source give their meaning:

• t₁ <;> t₂ runs t₁ on the main goal and t₂ on each goal it produces, collecting all the goals that result.
• all_goals t runs t on every goal and fails if it fails on any. focus t runs t on the main goal with the other goals hidden; the bullet · t, used in and_swap above and preferred by the documentation, also requires that t close the goal. In 4.34.1 t₁ <;> t₂ is itself a macro built from focus and all_goals.
• first | t₁ | t₂ | … runs each alternative until one succeeds, and fails if none does.
• try t runs t and succeeds even if t fails. In 4.34.1 it is not a primitive but a macro: first | t | skip.
• repeat t applies t for as long as it succeeds, undoing any partial changes of the attempt that fails. If t never fails, repeat t does not stop. repeat' t applies t recursively to every goal produced.

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := by
  constructor <;> (try constructor) <;> assumption

example (n : Nat) : n = n ∨ n = 0 := by
  first
  | exact Or.inr rfl
  | exact Or.inl rfl

In the second example the first alternative fails, since n = 0 does not hold for every n, and first backtracks to the second. Before the second alternative runs, the state saved before the first is restored, metavariable assignments included: in TacticM the standard way of catching a failure rolls the state back.

A new tactic in three lines

Since try is a macro, so can a user's tactic be. A macro tactic rewrites its own syntax into existing tactics, and needs no access to TacticM at all:

macro "conj_close" : tactic =>
  `(tactic| (repeat' constructor) <;> assumption)

theorem three (p q r : Prop) (hp : p) (hq : q) (hr : r) : (p ∧ q) ∧ r := by
  conj_close

#print three

theorem three : ∀ (p q r : Prop), p → q → r → (p ∧ q) ∧ r :=
fun p q r hp hq hr => ⟨⟨hp, hq⟩, hr⟩

The new tactic conj_close splits nested conjunctions as far as they go and closes every resulting goal with a hypothesis. The proof term shows nothing of it. Syntax extension and hygienic macros covers the macro system, and metaprogramming in Lean the tactics that need elab and TacticM, as show_goals above did.

Library search

Lean 4.34.1 includes two search tactics in its core. exact? searches Lean's environment for a definition or theorem that closes the goal with exact, discharging side conditions with solve_by_elim; apply? searches for one that refines the goal with apply. Both report what they found as a suggestion to paste in place of the search:

example (a b : Nat) : a + b = b + a := by
  exact?

Try this:
  [apply] exact Nat.add_comm a b

The suggestion is meant to replace the call. A proof that keeps exact? repeats the search every time the file is checked, and may find a different lemma once the library changes.

Next

Decision procedures describes the tactics that settle whole classes of goals: decide, omega, simp, grind and bv_decide.