11_Tactic-Style_Proofs.org

Theorem Proving in Lean

Tactic-Style Proofs

In this chapter, we describe an alternative approach to constructing proofs, using tactics. A proof term is a representation of a mathematical proof; tactics are commands, or instructions, that describe how to build such a proof. Informally, we might begin a mathematical proof by saying “to prove the forward direction, unfold the definition, apply the previous lemma, and simplify.” Just as these are instructions that tell the reader how to find the relevant proof, tactics are instructions that tell Lean how to construct a proof term. They naturally support an incremental style of writing proofs, in which users decompose a proof and work on goals one step at a time.

We will describe proofs that consist of sequences of tactics as “tactic-style” proofs, to contrast with the ways of writing proof terms we have seen so far, which we will call “term-style” proofs. Each style has its own advantages and disadvantages. One important difference is that term-style proofs are elaborated globally, and information gathered from one part of a term can be used to fill in implicit information in another part of the term. In contrast, tactics apply locally, and are narrowly focused on a single subgoal in the proof.

Entering the Tactic Mode

Conceptually, stating a theorem or introducing a have statement creates a goal, namely, the goal of constructing a term with the expected type. For example, the following creates the goal of constructing a term of type p ∧ q ∧ p, in a context with constants p q : Prop, Hp : p and Hq : q:

theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
sorry

We can write this goal as follows:

p : Prop, q : Prop, Hp : p, Hq : q ⊢ p ∧ q ∧ p

Indeed, if you replace the “sorry” by an underscore in the example above, Lean will report that it is exactly this goal that has been left unsolved.

Ordinarily, we meet such a goal by writing an explicit term. But wherever a term is expected, Lean allows us to insert instead a begin ... end block, followed by a sequence of commands, separated by commas. We can prove the theorem above in that way:

-- BEGIN
theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
begin
  apply and.intro,
  exact Hp,
  apply and.intro,
  exact Hq,
  exact Hp
end
-- END

The apply tactic applies an expression, viewed as denoting a function with zero or more arguments. It unifies the conclusion with the expression in the current goal, and creates new goals for the remaining arguments, provided that no later arguments depend on them. In the example above, the command apply and.intro yields two subgoals:

p : Prop,
q : Prop,
Hp : p,
Hq : q
⊢ p

⊢ q ∧ p

For brevity, Lean only displays the context for the first goal, which is the one addressed by the next tactic command. The first goal is met with the command exact Hp. The exact command is just a variant of apply which signals that the expression given should fill the goal exactly. It is good form to use it in a tactic proof, since its failure signals that something has gone wrong; but otherwise apply would work just as well.

You can see the resulting proof term with print:

theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
begin
  apply and.intro,
  exact Hp,
  apply and.intro,
  exact Hq,
  exact Hp
end

-- BEGIN
reveal test
print test
-- END

You can write a tactic script incrementally. If you run Lean on an incomplete tactic proof bracketed by begin and end, the system reports all the unsolved goals that remain. If you are running Lean with its Emacs interface, you can see this information by putting your cursor on the end symbol, which should be underlined. In the Emacs interface, there is another extremely useful trick: if you put your cursor on a line of a tactic proof and press “C-c C-g”, Lean will show you the goal that remains at the end of the line.

Tactic commands can take compound expressions, not just single identifiers. The following is a shorter version of the preceding proof:

-- BEGIN
theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
begin
  apply (and.intro Hp),
  exact (and.intro Hq Hp)
end
-- END

Unsurprisingly, it produces exactly the same proof term.

theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
begin
  apply (and.intro Hp),
  exact (and.intro Hq Hp)
end

-- BEGIN
reveal test
print test
-- END

Tactic applications can also be concatenated with a semicolon. Formally speaking, there is only one (compound) step in the following proof:

theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
begin
  apply (and.intro Hp); exact (and.intro Hq Hp)
end

Whenever a proof term is expected, instead of using a begin...end block, you can write the by keyword followed by a single tactic:

theorem test (p q : Prop) (Hp : p) (Hq : q) : p ∧ q ∧ p :=
by apply (and.intro Hp); exact (and.intro Hq Hp)

In the Lean Emacs mode, if you put your cursor on the “b” in “by” and press “C-c C-g”, Lean shows you the goal that the tactic is supposed to meet.

Basic Tactics

In addition to apply and exact, another useful tactic is intro, which introduces a hypothesis. What follows is an example of an identity from propositional logic that we proved in Section Examples of Propositional Validities, but now prove using tactics. We adopt the following convention regarding indentation: whenever a tactic introduces one or more additional subgoals, we indent another two spaces, until the additional subgoals are deleted.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
begin
  apply iff.intro,
    intro H,
    apply (or.elim (and.elim_right H)),
      intro Hq,
      apply or.intro_left,
      apply and.intro,
        exact (and.elim_left H),
      exact Hq,
    intro Hr,
    apply or.intro_right,
    apply and.intro,
    exact (and.elim_left H),
    exact Hr,
  intro H,
  apply (or.elim H),
    intro Hpq,
    apply and.intro,
      exact (and.elim_left Hpq),
    apply or.intro_left,
    exact (and.elim_right Hpq),
  intro Hpr,
  apply and.intro,
    exact (and.elim_left Hpr),
  apply or.intro_right,
  exact (and.elim_right Hpr)
end

The intro command can more generally be used to introduce a variable of any type:

example (A : Type) : A → A :=
begin
  intro a,
  exact a
end

example (A : Type) : ∀ x : A, x = x :=
begin
  intro x,
  exact eq.refl x
end

It has a plural form, intros, which takes a list of names.

example : ∀ a b c : nat, a = b → a = c → c = b :=
begin
  intros [a, b, c, H1, H2],
  exact eq.trans (eq.symm H2) H1
end

The intros command can also be used without any arguments, in which case, it chooses names and introduces as many variables as it can. We will see an example of this in a moment.

The assumption tactic looks through the assumptions in context of the current goal, and if there is one matching the conclusion, it applies it.

import data.nat
open nat

variables x y z w : ℕ

-- BEGIN
example (H1 : x = y) (H2 : y = z) (H3 : z = w) : x = w :=
begin
  apply (eq.trans H1),
  apply (eq.trans H2),
  assumption   -- applied H3
end
-- END

It will unify metavariables in the conclusion if necessary:

import data.nat
open nat

variables x y z w : ℕ

-- BEGIN
example (H1 : x = y) (H2 : y = z) (H3 : z = w) : x = w :=
begin
  apply eq.trans,
  assumption,     -- solves x = ?b with H1
  apply eq.trans,
  assumption,     -- solves ?b = w with H2
  assumption      -- solves z = w with H3
end
-- END

The following example uses the intros command to introduce the three variables and two hypotheses automatically:

example : ∀ a b c : nat, a = b → a = c → c = b :=
begin
  intros,
  apply eq.trans,
  apply eq.symm,
  assumption,
  assumption
end

The repeat combinator can be used to simplify the last two lines:

example : ∀ a b c : nat, a = b → a = c → c = b :=
begin
  intros,
  apply eq.trans,
  apply eq.symm,
  repeat assumption
end

There is variant of apply called fapply that is more aggressive in creating new subgoals for arguments. Here is an example of how it is used:

import data.nat
open nat

example : ∃ a : ℕ, a = a :=
begin
  fapply exists.intro,
  exact nat.zero,
  apply rfl
end

The command fapply exists.intro creates two goals. The first is to provide a natural number, a, and the second is to prove that a = a. Notice that the second goal depends on the first; solving the first goal instantiates a metavariable in the second.

Notice also that we could not write exact 0 in the proof above, because 0 is a numeral that is coerced to a natural number. In the context of a tactic proof, expressions are elaborated “locally,” before being sent to the tactic command. When the tactic command is being processed, Lean does not have enough information to determine that 0 needs to be coerced. We can get around that by stating the type explicitly:

import data.nat
open nat

-- BEGIN
example : ∃ a : ℕ, a = a :=
begin
  fapply exists.intro,
  exact (0 : ℕ),
  apply rfl
end
-- END

Another tactic that is sometimes useful is the generalize tactic, which is, in a sense, an inverse to intro.

import data.nat
open nat

variables x y z : ℕ

example : x = x :=
begin
  generalize x, -- goal is x : ℕ ⊢ ∀ (x : ℕ), x = x
  intro y,      -- goal is x y : ℕ ⊢ y = y
  apply rfl
end

example (H : x = y) : y = x :=
begin
  generalize H, -- goal is x y : ℕ, H : x = y ⊢ y = x
  intro H1,     -- goal is x y : ℕ, H H1 : x = y ⊢ y = x
  apply (eq.symm H1)
end

In the first example above, the generalize tactic generalizes the conclusion over the variable x, turning the goal into a ∀. In the second, it generalizes the goal over the hypothesis H, putting the antecedent explicitly into the goal. We generalize any term, not just variables:

import data.nat
open nat

variables x y z : ℕ

-- BEGIN
example : x + y + z = x + y + z :=
begin
  generalize (x + y + z), -- goal is x y z : ℕ ⊢ ∀ (x : ℕ), x = x
  intro w,                -- goal is x y z w : ℕ ⊢ w = w
  apply rfl
end
-- END

Notice that once we generalize over x + y + z, the variables x y z : ℕ in the context become irrelevant. (The same is true of the hypothesis H in the previous example.) The clear tactic throws away elements of the context, when it is safe to do so:

import data.nat
open nat

variables x y z : ℕ

-- BEGIN
example : x + y + z = x + y + z :=
begin
  generalize (x + y + z), -- goal is x y z : ℕ ⊢ ∀ (x : ℕ), x = x
  clear x, clear y, clear z,
  intro w,                -- goal is w : ℕ ⊢ w = w
  apply rfl
end
-- END

The revert tactic is a combination of generalize and clear:

import data.nat
open nat

variables x y z w : ℕ

-- BEGIN
example : x = x :=
begin
  revert x,     -- goal is ⊢ ∀ (x : ℕ), x = x
  intro y,      -- goal is y : ℕ ⊢ y = y
  apply rfl
end

example (H : x = y) : y = x :=
begin
  revert H,     -- goal is x y : ℕ ⊢ x = y → y = x
  intro H1,     -- goal is x y : ℕ, H1 : x = y ⊢ y = x
  apply (eq.symm H1)
end
-- END

Like intro, the tactics generalize, clear, and revert have plural forms. For example, we could have written above:

import data.nat
open nat

variables x y z : ℕ

-- BEGIN
example : x + y + z = x + y + z :=
begin
  generalize (x + y + z), -- goal is x y z : ℕ ⊢ ∀ (x : ℕ), x = x
  clears x y z,
  intro w,                -- goal is w : ℕ ⊢ w = w
  apply rfl
end
-- END

#

#

Structuring Tactic Proofs

One thing that is nice about Lean’s proof-writing syntax is that it is possible to mix term-style and tactic-style proofs, and pass between the two freely. For example, the tactics apply and exact expect arbitrary terms, which you can write using have, show, obtains, and so on. Conversely, when writing an arbitrary Lean term, you can always invoke the tactic mode by inserting a begin...end block. In the next example, we use show within a tactic block to fulfill a goal by providing an explicit term.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
begin
  apply iff.intro,
    intro H,
    apply (or.elim (and.elim_right H)),
      intro Hq,
      show (p ∧ q) ∨ (p ∧ r),
        from or.inl (and.intro (and.elim_left H) Hq),
    intro Hr,
    show (p ∧ q) ∨ (p ∧ r),
      from or.inr (and.intro (and.elim_left H) Hr),
  intro H,
  apply (or.elim H),
    intro Hpq,
    show p ∧ (q ∨ r), from
      and.intro
        (and.elim_left Hpq)
        (or.inl (and.elim_right Hpq)),
  intro Hpr,
  show p ∧ (q ∨ r), from
    and.intro
      (and.elim_left Hpr)
      (or.inr (and.elim_right Hpr))
end

You can also nest begin...end blocks within other begin...end blocks. In a nested block, Lean focuses on the first goal, and generates an error if it has not been fully solved at the end of the block. This can be helpful in indicating the separate proofs of multiple subgoals introduced by a tactic.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
begin
  apply iff.intro,
  begin
    intro H,
    apply (or.elim (and.elim_right H)),
      intro Hq,
      show (p ∧ q) ∨ (p ∧ r),
        from or.inl (and.intro (and.elim_left H) Hq),
    intro Hr,
    show (p ∧ q) ∨ (p ∧ r),
      from or.inr (and.intro (and.elim_left H) Hr),
  end,
  begin
    intro H,
    apply (or.elim H),
    begin
      intro Hpq,
      show p ∧ (q ∨ r), from
        and.intro
          (and.elim_left Hpq)
          (or.inl (and.elim_right Hpq)),
    end,
    begin
      intro Hpr,
      show p ∧ (q ∨ r), from
        and.intro
          (and.elim_left Hpr)
          (or.inr (and.elim_right Hpr))
    end
  end
end

Notice that you still need to use a comma after a begin...end block when there are remaining goals to be discharged. Within a begin...end block, you can abbreviate nested occurrences of begin and end with curly braces:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
begin
  apply iff.intro,
  { intro H,
    apply (or.elim (and.elim_right H)),
    { intro Hq,
      apply or.intro_left,
      apply and.intro,
      { exact (and.elim_left H) },
      { exact Hq }},
    { intro Hr,
      apply or.intro_right,
      apply and.intro,
      { exact (and.elim_left H)},
      { exact Hr }}},
  { intro H,
    apply (or.elim H),
    { intro Hpq,
      apply and.intro,
      { exact (and.elim_left Hpq) },
      { apply or.intro_left,
        exact (and.elim_right Hpq) }},
    { intro Hpr,
      apply and.intro,
      { exact (and.elim_left Hpr)},
      { apply or.intro_right,
          exact (and.elim_right Hpr) }}}
end

Here we have adopted the convention that whenever a tactic increases the number of goals to be solved, the tactics that solve each subsequent goal are enclosed in braces. This may not increase readability much, but it does help clarify the structure of the proof.

There is a have construct for tactic-style proofs that is similar to the one for term-style proofs. In the proof below, the first have creates the subgoal Hp : p. The from clause solves it, and after that Hp is available to subsequent tactics. The example illustrates that you can also use another begin...end block, or a by clause, to prove a subgoal introduced by have.

-- BEGIN
variables p q : Prop

example : p ∧ q ↔ q ∧ p :=
begin
  apply iff.intro,
  begin
    intro H,
    have Hp : p, from and.left H,
    have Hq : q, from and.right H,
    apply and.intro,
    repeat assumption
  end,
  begin
    intro H,
    have Hp : p,
      begin
        apply and.right,
        apply H
      end,
    have Hq : q, by apply and.left; exact H,
    apply (and.intro Hp Hq)
  end
end
-- END

Cases and Pattern Matching

The cases tactic works on elements of an inductively defined type. It does what the name suggests: it decomposes an element of an inductive type according to each of the possible constructors, and leaves a goal for each case. Note that the following example also uses the revert tactic to move the hypothesis into the conclusion of the goal.

import data.nat
open nat

example (x : ℕ) (H : x ≠ 0) : succ (pred x) = x :=
begin
  revert H,
  cases x,
  -- first goal: ⊢ 0 ≠ 0 → succ (pred 0) = 0
  { intro H1,
    apply (absurd rfl H1)},
  -- second goal: ⊢ succ a ≠ 0 → succ (pred (succ a)) = succ a
  { intro H1,
    apply rfl}
end

The name of the cases tactic is particularly well suited to use with disjunctions:

example (a b : Prop) : a ∨ b → b ∨ a :=
begin
  intro H,
  cases H with [Ha, Hb],
  { exact or.inr Ha },
  { exact or.inl Hb }
end

In the next example, we rely on the decidability of equality for the natural numbers to carry out another proof by cases:

import data.nat
open nat

check nat.sub_self

example (m n : nat) : m - n = 0 ∨ m ≠ n :=
begin
  cases (decidable.em (m = n)) with [Heq, Hne],
  { apply eq.subst Heq,
    exact or.inl (nat.sub_self m)},
  { apply or.inr Hne }
end

The cases tactic can also be used to extract the arguments of a constructor, even for an inductive type like and, for which there is only one constructor.

example (p q : Prop) : p ∧ q → q ∧ p :=
begin
  intro H,
  cases H with [H1, H2],
  apply and.intro,
  exact H2,
  exact H1
end

Here the with clause names the two arguments to the constructor. If you omit it, Lean will choose a name for you. If there are multiple constructors with arguments, you can provide cases with a list of all the names, arranged sequentially:

import data.nat
open nat

inductive foo : Type :=
| bar1 : ℕ → ℕ → foo
| bar2 : ℕ → ℕ → ℕ → foo

definition silly (x : foo) : ℕ :=
begin
  cases x with [a, b, c, d, e],
  exact b,    -- a, b, c are in the context
  exact e     -- d, e    are in the context
end

You can also use pattern matching in a tactic block. With

example (p q r : Prop) : p ∧ q ↔ q ∧ p :=
begin
  apply iff.intro,
  { intro H,
    match H with
    |  and.intro H₁ H₂ := by apply and.intro; repeat assumption
    end },
  { intro H,
    match H with
    | and.intro H₁ H₂ := by apply and.intro; repeat assumption
    end },
end

With pattern matching, the first and third examples in this section could be written as follows:

import data.nat
open nat

inductive foo : Type :=
| bar1 : ℕ → ℕ → foo
| bar2 : ℕ → ℕ → ℕ → foo

-- BEGIN
example (x : ℕ) (H : x ≠ 0) : succ (pred x) = x :=
begin
  revert H,
  match x with
  | 0      := by intro H1; exact (absurd rfl H1)
  | succ y := by intro H1; apply rfl
  end
end

definition silly (x : foo) : ℕ :=
begin
  match x with
  | foo.bar1 a b   := b
  | foo.bar2 c d e := e
  end
end
-- END

The Rewrite Tactic

The rewrite tactic provide a basic mechanism for applying substitutions to goals and hypotheses, providing a convenient and efficient way of working with equality. This tactic is loosely based on the rewrite tactic available in the proof language SSReflect.

The rewrite tactic has many features. The most basic form of the tactic is rewrite t, where t is a term which conclusion is an equality. In the following example, we use this basic form to rewrite the goal using a hypothesis.

open nat
variables (f : nat → nat) (k : nat)

example (H₁ : f 0 = 0) (H₂ : k = 0) : f k = 0 :=
begin
  rewrite H₂, -- replace k with 0
  rewrite H₁  -- replace f 0 with 0
end

In the example above, the first rewrite tactic replaces k with 0 in the goal f k = 0. Then, the second rewrite replace f 0 with 0. The rewrite tactic automatically closes any goal of the form t = t.

Multiple rewrites can be combined using the notation rewrite [t_1, ..., t_n], which is just shorthand for rewrite t_1, ..., rewrite t_n. The previous example can be written as:

open nat
variables (f : nat → nat) (k : nat)

example (H₁ : f 0 = 0) (H₂ : k = 0) : f k = 0 :=
begin
  rewrite [H₂, H₁]
end

By default, the rewrite tactic uses an equation in the forward direction, matching the left-hand side with an expression, and replacing it with the right-hand side. The notation -t can be used to instruct the tactic to use the equality t in the reverse direction.

open nat
variables (f : nat → nat) (a b : nat)

example (H₁ : a = b) (H₂ : f a = 0) : f b = 0 :=
begin
  rewrite [-H₁, H₂]
end

In this example, the term -H₁ instructs the rewriter to replace b with a.

The notation *t instructs the rewriter to apply the rewrite t zero or more times, while the notation +t instructs the rewriter to use it at least once. Note that rewriting with *t never fails.

import data.nat
open nat algebra

example (x y : nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
by rewrite [*left_distrib, *right_distrib, -add.assoc]

To avoid non-termination, the rewriter tactic has a limit on the maximum number of iterations performed by rewriting steps of the form *t and +t. For example, without this limit, the tactic rewrite *add.comm would make Lean diverge on any goal that contains a sub-term of the form t + s since commutativity would be always applicable. The limit can be modified by setting the option rewriter.max_iter.

The notation rewrite n t, where n, is a positive number indicates that t must be applied exactly n times. Similarly, rewrite n>t is notation for at most n times.

A pattern p can be optionally provided to a rewriting step t using the notation {p}t . It allows us to specify where the rewrite should be applied. This feature is particularly useful for rewrite rules such as commutativity a + b = b + a which may be applied to many different sub-terms. A pattern may contain placeholders. In the following example, the pattern b + _ instructs the rewrite tactic to apply commutativity to the first term that matches b + _, where _ can be matched with an arbitrary term.

import data.nat
open nat algebra
-- BEGIN
example (a b c : nat) : a + b + c = a + c + b :=
begin
  rewrite [add.assoc, {b + _}add.comm, -add.assoc]
end
-- END

In the example above, the first step rewrites a + b + c to a + (b + c). Then, {b + _}add.comm applies commutativity to the term b + c. Without the pattern {b + _}, the tactic would instead rewrite a + (b + c) to (b + c) + a. Finally, -add.assoc applies associativity in the “reverse direction” rewriting a + (c + b) to a + c + b.

By default, the tactic affects only the goal. The notation t at H applies the rewrite t at hypothesis H.

import data.nat
open nat algebra
-- BEGIN
variables (f : nat → nat) (a : nat)

example (H : a + 0 = 0) : f a = f 0 :=
begin
  rewrite [add_zero at H, H]
end
-- END

The first step, add_zero at H, rewrites the hypothesis (H : a + 0 = 0) to a = 0. Then the new hypothesis (H : a = 0) is used to rewrite the goal to f 0 = f 0.

Multiple hypotheses can be specified in the same at clause.

import data.nat
open nat algebra
-- BEGIN
variables (a b : nat)

example (H₁ : a + 0 = 0) (H₂ : b + 0 = 0) : a + b = 0 :=
begin
  rewrite add_zero at (H₁, H₂),
  rewrite [H₁, H₂]
end
-- END

You may also use t at * to indicate that all hypotheses and the goal should be rewritten using t. The tactic step fails if none of them can be rewritten. The notation t at * ⊢ applies t to all hypotheses. You can enter the symbol ⊢ by typing \|-.

import data.nat
open nat algebra
-- BEGIN
variables (a b : nat)

example (H₁ : a + 0 = 0) (H₂ : b + 0 = 0) : a + b + 0 = 0 :=
begin
  rewrite add_zero at *,
  rewrite [H₁, H₂]
end
-- END

The step add_zero at * rewrites the hypotheses H₁, H₂ and the main goal using the add_zero (x : nat) : x + 0 = x, producing a = 0, b = 0 and a + b = 0 respectively.

The rewrite tactic is not restricted to propositions. In the following example, we use rewrite H at v to rewrite the hypothesis v : vector A n to v : vector A 0.

import data.examples.vector
open nat

variables {A : Type} {n : nat}
example (H : n = 0) (v : vector A n) : vector A 0 :=
begin
  rewrite H at v,
  exact v
end

Given a rewrite (t : l = r), the tactic rewrite t by default locates a sub-term s which matches the left-hand-side l, and then replaces all occurrences of s with the corresponding right-hand-side. The notation at {i_1, ..., i_k} can be used to restrict which occurrences of the sub-term s are replaced. For example, rewrite t at {1, 3} specifies that only the first and third occurrences should be replaced.

import data.nat
open nat
-- BEGIN
variables (f : nat → nat → nat → nat) (a b : nat)

example (H₁ : a = b) (H₂ : f b a b = 0) : f a a a = 0 :=
by rewrite [H₁ at {1, 3}, H₂]
-- END

Similarly, rewrite t at H {1, 3} specifies that t must be applied to hypothesis H and only the first and third occurrences must be replaced. You can also specify which occurrences should not be replaced using the notation rewrite t at -{i_1, ..., i_k}. Here is the previous example using this feature.

import data.nat
open nat

variables (f : nat → nat → nat → nat) (a b : nat)
-- BEGIN
example (H₁ : a = b) (H₂ : f b a b = 0) : f a a a = 0 :=
by rewrite [H₁ at -{2}, H₂]
-- END

So far, we have used theorems and hypotheses as rewriting rules. In these cases, the term t is just an identifier. The notation rewrite (t) can be used to provide an arbitrary term t as a rewriting rule.

import algebra.group
namespace hide
-- BEGIN
open algebra

variables {A : Type} [s : group A]
include s

theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
by rewrite [-(mul_one a⁻¹), -H, inv_mul_cancel_left]
-- END
end hide

In the example above, the term mul_one a⁻¹ has type a⁻¹ * 1 = a⁻¹. Thus, the rewrite step -(mul_one a⁻¹) replaces a⁻¹ with a⁻¹ * 1.

Calculational proofs and the rewrite tactic can be used together.

import data.nat
open nat
-- BEGIN
example (a b c : nat) (H1 : a = b) (H2 : b = c + 1) : a ≠ 0 :=
calc
  a     = succ c : by rewrite [H1, H2, add_one]
    ... ≠ 0      : succ_ne_zero c
-- END

The rewrite tactic also supports reduction steps: ↑f, ▸*, ↓t, and ▸t. The step ↑f unfolds f and performs beta/iota reduction and simplify projections. This step fails if there is no f to be unfolded. The step ▸* is similar to ↑f, but does not take a constant to unfold as argument, therefore it never fails. The fold step ↓t unfolds the head symbol of t, then search for the result in the goal (or a given hypothesis), and replaces any match with t. Finally, ▸t tries to reduce the goal (or a given hypothesis) to t, and fails if it is not convertible to t. (The up arrow is entered with \u, the down arrow is entered with \d, and the right triangle is entered with \t. You can also use the ASCII alternatives ^f, >*, <d t, and > t for ↑f, ▸*, ↓t, and ▸t, respectively.)

import data.nat
open nat
-- BEGIN
definition double (x : nat) := x + x

variable f : nat → nat

example (x y : nat) (H1 : double x = 0) (H3 : f 0 = 0) : f (x + x) = 0 :=
by rewrite [↑double at H1, H1, H3]
-- END

The step ↑double at H1 unfolds double in the hypothesis H1. The notation rewrite ↑[f_1, ..., f_n] is shorthand for rewrite [↑f_1, ..., ↑f_n]

The tactic esimp is a shorthand for rewrite ▸*. Here are two simple examples:

open sigma nat

example (x y : nat) (H : (fun (a : nat), pr1 ⟨a, y⟩) x = 0) : x = 0 :=
begin
  esimp at H,
  exact H
end

example (x y : nat) (H : x = 0) : (fun (a : nat), pr1 ⟨a, y⟩) x = 0 :=
begin
  esimp,
  exact H
end

Here is an example where the fold step is used to replace a + 1 with f a in the main goal.

open nat

definition foo [irreducible] (x : nat) := x + 1

example (a b : nat) (H : foo a = b) : a + 1 = b :=
begin
  rewrite ↓foo a,
  exact H
end

Here is another example: given any type A, we show that the list A append operation s ++ t is associative.

import data.list
open list
variable {A : Type}

theorem append_assoc : ∀ (s t u : list A), s ++ t ++ u = s ++ (t ++ u)
| append_assoc nil t u      := by apply rfl
| append_assoc (a :: l) t u :=
  begin
    rewrite ▸ a :: (l ++ t ++ u) = _,
    rewrite append_assoc
  end

We discharge the inductive cases using the rewrite tactic. The base case is solved by applying reflexivity, because nil ++ t ++ u and nil ++ (t ++ u) are definitionally equal. In the inductive step, we first reduce the goal a :: s ++ t ++ u = a :: s ++ (t ++ u) to a :: (s ++ t ++ u) = a :: s ++ (t ++ u) by applying the reduction step ▸ a :: (l ++ t ++ u) = _. The idea is to expose the term l ++ t ++ u, which can be rewritten using the inductive hypothesis append_assoc (s t u : list A) : s ++ t ++ u = s ++ (t ++ u). Notice that we used a placeholder _ in the right-hand-side of this reduction step; this placeholder is unified with the right-hand-side of the main goal. As a result, we do not have the copy the right-hand side of the goal.

The rewrite tactic supports type classes. In the following example we use theorems from the mul_zero_class and add_monoid classes in an example for the comm_ring class. The rewrite is acceptable because every comm_ring (commutative ring) is an instance of the classes mul_zero_class and add_monoid.

import algebra.ring
open algebra

example {A : Type} [s : comm_ring A] (a b c : A) : a * 0 + 0 * b + c * 0 + 0 * a = 0 :=
begin
  rewrite [+mul_zero, +zero_mul, +add_zero]
end

There are two variants of rewrite, namely krewrite and xrewrite, that are more aggressive about matching patterns. krewrite will unfold definitions as long as the head symbol matches, for example, when trying to match a pattern f p with an expression f t. In contrast, xrewrite will unfold all definitions that are not marked irreducible. Both are computationally expensive and should be used sparingly. krewrite is often useful when matching patterns requires unfolding projections in an algebraic structure.