Tactics¶

Every tactic used in these notes, including the how-to guides, with what it does, where it first appears and which library provides it. Each example is taken from a file that compiles. The table gives the overview; the sections below give the detail in the same order.

norm_num¶

Proves goals that are arithmetic once definitions are unfolded, such as inequalities between numerals. Definitions it may unfold are passed in brackets; without them it treats payoff as opaque and makes no progress. It builds a proof from Mathlib lemmas and never computes with real numbers, which is why it works where decide does not.

example : payoff defect cooperate = 5 := by
  norm_num [payoff]

rfl¶

Proves a = b when the two sides are equal by definition, by computing both. It proves equalities only; on an inequality it fails with a type mismatch. In these notes it is used as a term after := rather than inside by.

example : payoff defect cooperate = 5 := rfl

decide¶

Proves a goal by finding a decision procedure for it and running it. It works for concrete statements about natural numbers, integers and finite types, and fails on real numbers, whose comparisons have no procedure. See Computation and the real numbers.

theorem zero_lt_one_nat : (0 : ℕ) < 1 := by
  decide

intro¶

Proves a goal of the form ∀ x, P x or P → Q by naming the variable or the hypothesis and moving it into the context. Several names may be given at once, and a goal ¬ P is treated as P → False.

  intro opponent
  cases opponent

Before and after intro opponent:

⊢ StrictlyDominates payoff defect cooperate

opponent : Action
⊢ payoff cooperate opponent < payoff defect opponent

cases¶

Splits a variable of an inductive type into one goal per constructor, substituting the constructor for the variable in the goal and in every hypothesis. On Action it produces the goals case cooperate and case defect.

The focusing dot¶

·, typed \., focuses on the first remaining goal. The tactics indented beneath it must close that goal, and Lean reports an error if they do not.

  cases mutant
  · left
    norm_num [payoff]
  · contradiction

The combinator <;>¶

t <;> s runs t, then runs s on every goal that t produced.

  cases opponent <;> norm_num [payoff]

left¶

Proves P ∨ Q by committing to P, leaving P as the goal. The tactic right commits to Q.

have¶

Adds a named fact to the context. The fact is often a hypothesis applied to particular arguments, since a proof of a ∀ statement is a function.

  intro claim
  have tempted := claim defect
  norm_num [payoff] at tempted

at¶

Many tactics act on the goal by default; at h makes them act on the hypothesis h instead. In the example above, norm_num [payoff] at tempted reduces the hypothesis to False, which closes the goal.

contradiction¶

Closes the goal when the context contains something impossible, such as a hypothesis h : a ≠ a or h : False. The goal itself need not be true.

by_cases¶

by_cases h : P splits into two goals, case pos with h : P and case neg with h : ¬P. It works for any statement, whether or not a type has constructors to split on.

  by_cases same : deviation = resident
  · rw [same]

rw¶

rw [h], where h : a = b, replaces every a in the goal by b. After rewriting it tries to close the goal by reflexivity, which is why rw [same] above finishes its case. Adding at h' rewrites a hypothesis instead.

rcases¶

Takes a hypothesis apart according to a pattern. a | b splits a disjunction into two goals; ⟨a, b⟩ splits a conjunction into two hypotheses; _ discards a part, which then appears in the context with a dagger, as in right✝.

  · rcases stable deviation same with worse | ⟨tie, _⟩
    · exact le_of_lt worse
    · exact le_of_eq tie

exact¶

exact e closes the goal when e is a proof of exactly that goal. The two uses above apply the Mathlib lemmas le_of_lt : a < b → a ≤ b and le_of_eq : a = b → a ≤ b to hypotheses from the context.

exact?¶

Searches the imported libraries for a lemma that closes the goal and reports it as a suggestion, in the form Try this: exact .... It is for exploring; the suggestion is then written into the proof in its place.

trace_state¶

Prints the current goals as an informational message without changing them, so that they appear in the output of lake build. See Read a goal without an infoview.

  trace_state
  intro opponent

constructor¶

Splits a goal built from a structure into one goal per part. On P ↔ Q it produces the two directions, P → Q and Q → P.

  constructor
  · intro stable
    refine ⟨stable.isSymmetricNash, ?_⟩

simp only¶

simp only [f, g] unfolds the definitions f and g, and simplifies with the given lemmas only. Plain simp would also use every lemma Mathlib marks for simplification, which is more powerful and less predictable.

linarith¶

Proves a goal that follows from the hypotheses by adding them and multiplying them by constants. It works by assuming the goal is false and deriving a contradiction. It does not unfold definitions, so simp only usually comes first. See Prove an inequality.

  · simp only [symbolicPayoff]
    linarith

nlinarith¶

As linarith, but it also multiplies pairs of hypotheses together, which handles products such as a probability times a payoff. It accepts extra facts as hints in brackets.

positivity¶

Proves goals of the form 0 < e or 0 ≤ e by the structure of e: squares, sums of non-negative terms, products of positive terms and so on.

apply¶

apply f closes the goal with the lemma f when its conclusion matches, leaving each of its assumptions as a new goal. See Use a hypothesis.

obtain¶

obtain ⟨x, h⟩ := e takes apart a proof e of ∃ x, P x or of P ∧ Q, naming the pieces.

apply? and rw?¶

Like exact?, these search the imported libraries: apply? for a lemma that applies to the goal, possibly leaving further goals, and rw? for an equation to rewrite with. See Find a lemma.

ring¶

Proves an equation between expressions in a commutative ring, such as the real numbers, when it follows from the laws of algebra alone: expanding, collecting terms and cancelling. It uses no hypotheses.

  simp only [expectedPayoff, sum_posture, payoff, mineDove, theirsDove]
  ring

ext¶

Reduces an equality between functions, or between structures built from functions such as mixed strategies, to an equality at each argument. After ext posture the goal is about the value at an arbitrary posture.

show¶

show P replaces the goal with P, provided the two are the same statement once definitions are unfolded. It is used to make a goal readable, or to put it in the form a following tactic expects.

refine¶

refine e closes the goal with a term e that may contain holes written ?_. Each hole becomes a new goal. Above, the first half of a conjunction is supplied at once and the second is left to prove.