Lean theorem prover/Explainers/Tactics

Technical version: The tactic framework· Metaprogramming in Lean

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 proof in Lean can be written in two ways: as a term, an expression whose type is the statement, or as a sequence of tactics, commands that tell Lean how to construct that expression. This page explains what a tactic is, where the idea came from, which tactics are met most often, and why no tactic has to be trusted.

Two ways to write the same proof

In Lean a proof is a value, and the statement it proves is its type (see propositions as types). Here is a proof that "p and q" gives "q and p", written both ways:

theorem swap_term (p q : Prop) (h : p ∧ q) : q ∧ p :=
  ⟨h.2, h.1⟩

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

#print swap_term
#print swap_tactic

The first proof is a term. The brackets make a pair, and the pair is the second part of h followed by the first. The second proof begins with by, which switches to tactics. constructor splits the goal "q and p" into two goals, q and p, and each exact supplies one of them.

The two #print lines answer with the same proof, word for word: fun p q h => ⟨h.right, h.left⟩. The tactic script was a way of arriving at the term. The term is what Lean keeps. Theorem Proving in Lean 4 calls the two styles "term-style" and "tactic-style" proofs.

What a tactic is

A tactic is a small program that works on a proof state: the list of goals still to be proved, each with the facts available for it. A tactic either fails, or succeeds and leaves some number of new goals, possibly none. When no goals remain, the proof is complete. Behind the scenes, each step fills in part of the proof term, and each open goal stands for a part not yet filled. How goals are shown and filled is the subject of holes and goals.

Lean 4's tactics are themselves Lean programs. Lean 4 is a reimplementation of Lean written in Lean itself, and its users can extend it with tactics and decision procedures of their own; many write their proof automation in Lean. A new tactic can be an abbreviation that expands into existing tactics, or a program that acts on the proof state directly.

Where the idea came from

Tactics come from LCF, a proof-checking program begun by Robin Milner at Stanford in 1972 and developed further at Edinburgh. In Edinburgh LCF the logic was set up as a protected type in the programming language ML, so that theorems could be produced only by the rules of inference. Strategies for breaking a goal into subgoals were ordinary ML functions, which Milner called tactics, and functions that combine strategies were called tacticals. Lean keeps the first idea, that proof strategies are ordinary programs, and secures the second in its own way, by checking the finished term, as described below. The history is told in LCF and the tactic idea.

The tactics met most often

• intro: to prove "if A then B", assume A, give it a name, and prove B.
• apply: to prove a goal with a fact of the form "if A then the goal", switch to proving A.
• exact: finish the goal by giving a proof of exactly that statement.
• rw: rewrite the goal with an equation, replacing one side by the other.
• simp: simplify with a large stock of known equations.
• induction: split a goal about every value of a type into one goal for each way a value can be made, with induction hypotheses (see induction, as the machine sees it).
• cases: split by how a value was made, without induction hypotheses. A proof of "p or q", for instance, was made either from a proof of p or from a proof of q.
• omega: settle a problem of linear arithmetic over whole numbers.
• decide: settle a statement by computing whether it is true.

The last two, with simp, are automation, treated in automation and its limits and computation inside proofs. The first three are enough for a short chain of reasoning:

theorem chain (p q r : Prop) : (p → q) → (q → r) → p → r := by
  intro hpq hqr hp
  apply hqr
  exact hpq hp

#print chain

The statement says: if p gives q, and q gives r, then p gives r. intro names the three assumptions, and the goal becomes r. apply hqr uses the fact that q gives r, so it is enough to prove q. exact hpq hp finishes: applying "p gives q" to the proof of p yields a proof of q. Lean prints the term that the script produced: fun p q r hpq hqr hp => hqr (hpq hp). It is the same argument, read from the inside out.

Why a tactic need not be trusted

Whatever a tactic does, its product is a term, and the term goes to the Lean kernel to be checked like any other. A tactic with a bug can fail, or produce a term that the Lean kernel rejects. It cannot make Lean accept a false theorem. The Lean Language Reference puts it this way: the worst a bug in a tactic can cause is a confusing error message, not an incorrect proof.

That is why tactics may be large, clever and written by anyone, including programs that search for proofs on their own, while the part that must be trusted stays small (see the small trusted core). The exceptions are visible. A tactic that rests on an extra axiom, such as native_decide or the placeholder sorry, leaves that axiom's name in the list that #print axioms shows for the theorem.

Terms or tactics?

Neither style is more rigorous than the other; both end in the same kind of term. Tactic proofs are often shorter and easier to write, and they open the way to automation, since the automatic procedures are tactics too. They can be harder to read, because the reader has to picture the goal after every step. A term shows the whole argument at once but can be laborious to write by hand. In practice the two are mixed: a term may contain a by block, and a tactic such as exact takes a term.

Next

• Holes and goals: the proof state, and the parts of a proof still missing.
• The tactic framework: the technical treatment.