Tactics: what a tactic proof builds

Goals are metavariables

Part 2 showed that the elaborator works by creating metavariables and filling them in. Tactics work the same way. When the elaborator reaches by, it creates a metavariable whose type is the statement to prove. That metavariable is the goal. Each tactic assigns part of the goal and leaves new metavariables for the parts it didn't finish, and those become the new goals.

run_tac runs a piece of TacticM code in the middle of a proof, so you can watch this happen. The probe below saves the original goal, runs the two tactics one at a time, and prints the goal with every assigned metavariable replaced by its value:

start: ?m.1

after constructor: ⟨?left, ?right⟩

after assumption: ⟨hp, hq⟩

At the start, the goal is an unassigned metavariable. constructor assigned it to And.intro ?left ?right, a term with two new holes, named after the fields of And. Those two holes are the goals constructor leaves for you. Then assumption filled each hole with a hypothesis of the right type, and the term was complete.

So the "proof state" in the editor is a view of the metavariables still unassigned. A tactic proof is finished when none are left. At that point the elaborator has an ordinary term, and the kernel checks it the same way it checks a term you wrote by hand. The kernel never runs a tactic. A buggy tactic can build a wrong term, but the kernel rejects any term that doesn't type-check. A tactic can still close a goal with sorry or an axiom, which the kernel accepts. Part 4 covers how #print axioms exposes that.

Sequencing vs <;>

A new line (or ;) runs the next tactic on whatever the goal list is now, which means on the main goal. t <;> s instead runs s on every goal that t produced. The difference shows up as soon as a tactic makes more than one goal:

unsolved goals
rightp q:Prophp:phq:q⊢ q

assumption closed left and stopped. right was never touched, so the proof ends with a goal still open. (Lean also warns that hq is unused, which is the same mistake seen from the other side.) Written constructor <;> assumption, as in the first section, the same assumption runs once per new goal.

Picking a goal

The other combinators choose which goals a tactic sees:

• · focuses on the main goal and fails unless the tactic block under it closes that goal. That's why the first example above can't leave anything open by accident.

• case tag => tac focuses on the goal with that tag, in any order.

• all_goals tac runs tac on each goal and fails if it fails on any. any_goals tac succeeds if it worked on at least one.

• first | t₁ | t₂ tries t₁, and if it fails, rolls the state back and tries t₂.

Two of these together, solving the goals out of order:

and one tactic that works on both goals, whichever hypothesis each needs:

Try this:
  [apply] exact ⟨hp, hq⟩

For left, exact hq fails (hq proves q, not p), so first restores the goal and tries exact hp. The failed attempt leaves nothing behind, because first saves the whole tactic state, including the metavariable assignments, before each try. This backtracking is something terms can't express. It belongs to the program that builds the term, and none of it is left in the term itself.

decide: let the kernel compute

theorem small : 10 < 20 :=
of_decide_eq_true (id (Eq.refl true))

The term is short because the work is left to the kernel. 10 < 20 has a Decidable instance, and decide (10 < 20) is a Bool. The tactic claims Eq.refl true : decide (10 < 20) = true, and of_decide_eq_true turns that into a proof of 10 < 20. For the kernel to accept Eq.refl true at that type, it has to reduce decide (10 < 20) to true itself, by unfolding the instance. The proof is a certificate that says "run this and check you get true". The log entry on rfl vs decide looks at the same mechanism from the failing side.

That makes decide proofs cheap to store and potentially expensive to check: the kernel redoes the computation every time the theorem is checked, and the kernel is a slow evaluator. Part 4 covers native_decide, which hands the computation to compiled code instead and changes what you have to trust.

simp: a chain of rewrites

Try this:
  [apply] simp only [List.append_nil]

simp? reports which lemmas simp used, here only List.append_nil (xs ++ [] = xs). The term shows how one rewrite proves the goal:

theorem appNil : ∀ (xs : List Nat), (xs ++ []).length = xs.length :=
fun xs =>
  of_eq_true
    (Eq.trans (congrFun' (congrArg Eq (congrArg List.length (List.append_nil xs))) xs.length) (eq_self xs.length))

Read it from the inside out:

• List.append_nil xs proves xs ++ [] = xs.

• congrArg List.length applies List.length to both sides: (xs ++ []).length = xs.length.

• congrArg Eq and congrFun' lift that equation of numbers to an equation of propositions: the goal (xs ++ []).length = xs.length equals the proposition xs.length = xs.length.

• eq_self xs.length says (xs.length = xs.length) = True, and Eq.trans joins the two steps: the goal equals True.

• of_eq_true turns "this proposition equals True" into a proof of it.

This is how simp works in general. It rewrites the goal, as a proposition, step by step toward True, and records each step as an equation. The proof is the chain of those equations. simp never proves your goal directly; it proves that your goal is equal to something trivially true.

'appNil' depends on axioms: [propext]

Equations between propositions are where propext comes in: it is the axiom that says two propositions that imply each other are equal. A simp proof can depend on it even when, as here, nothing about the goal mentions it.

omega: a decision procedure with a certificate

omega decides linear arithmetic over Nat and Int. It looks for a contradiction between the hypotheses and the negated goal, and then has to justify what it found as a term:

theorem bump : ∀ (x y : Nat), x < y → x + 1 ≤ y :=
fun x y h => Decidable.byContradiction fun a => bump._proof_1 x y h a

The top level is a proof by contradiction: assume a : ¬x + 1 ≤ y and derive False. The derivation lives in an auxiliary theorem, bump._proof_1, which omega added to the environment. Printing it gives about 2 KB of term, so I'll describe it instead. It casts the hypotheses to Int, rewrites each one into a linear combination over the atoms x and y (with lemmas from Lean.Omega), combines them into a single constraint, and finishes with not_sat'_of_isImpossible (of_decide_eq_true (id (Eq.refl true))). The last step is the decide certificate from above: once the problem is a concrete constraint, "this has no solution" is a computation the kernel can run.

The axiom lists show a second difference:

'bump' depends on axioms: [propext, Quot.sound]

'small' does not depend on any axioms

The decide proof uses no axioms: it is computation that the kernel checks. The omega proof uses propext and Quot.sound (from which Lean derives function extensionality). Neither is a reason to distrust it; both are among Lean's three standard axioms. But "proved by a tactic" can mean quite different things to the kernel, and #print axioms is the quickest way to see which. Part 4 starts from here.

A tactic can be wrong

Nothing forces goal.assign to be given a term of the right type. This tactic fills every goal with True.intro:

(kernel) declaration type mismatch, 'oops' has type
  True
but it is expected to have type
  1 = 2

The tactic ran without complaint and the goal list ended empty, so as far as the tactic framework knew, the proof was finished. The error comes from the kernel, as the (kernel) prefix says: when oops was added to the environment, the kernel type-checked the finished term and found a proof of True where a proof of 1 = 2 was needed. This is the guarantee from the first section in action. A buggy tactic can fail to prove something, but it can't make the kernel accept a term of the wrong type. What it can do is close a goal with sorry or an axiom, which the kernel accepts, and which #print axioms shows.

Macros

Not every tactic needs TacticM. A macro tactic is a rewrite of syntax into other tactics, like the if macro in part 2:

Try this:
  [apply] exact ⟨hp, hq⟩

split_and expands to constructor <;> assumption before anything runs, so it builds the same term as the script it stands for. Macros are the right tool for naming a combination of existing tactics. elab is for tactics that need to inspect goals or build terms themselves.