11_Using_Tactics.org

Theorem Proving in Lean

Using Tactics

In this chapter, we describe an alterantive 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.

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:

import logic

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:

import logic

-- 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 definition:

import logic

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
print definition test
-- END

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

import logic

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

Unsuprisingly, it produces exactly the same proof term.

import logic

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

-- BEGIN
print definition test2
-- 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 useful trick: if you open up the *lean-info* buffer in a separate window and put your cursor on the comma after a tactic command, Lean shows you the goals that remain open at that stage in the proof.

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 <a href=”Examples of Propositional Validities”>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.

import logic

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

A variant of apply called fapply 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 (typeof 0 : ℕ),
  apply rfl
end
-- END

One thing that is nice about Lean’s proof-writing syntax is that it is possible to mix “declarative” 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 aribtrary 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.

import logic

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

The Rewrite Tactic

The rewrite tactic provide a basic mechanism for applying substitutions to goals and hypotheses. It is a simple and efficient mechanism for working with Leibniz equality. This tactic is loosely based on the one available in SSReflect.

The rewrite tactic has many features. The most basic form 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 trivial goal of the form t = t.

Multiple rewrites can be combined using the notations rewrite [t_1, ..., t_n] or rewrite ⟨t_1, ..., t_n⟩. Both notations are just shorthands 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 rewrites from left to right. The notation -t can be used to instruct the tactic to rewrite from right to left.

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

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, and +t one or more. Note that, *t never fails.

import data.nat
open nat

example (x y : nat) : (x + y) * (x + y) = x * x + y * x + x * y + y * y :=
by rewrite ⟨*mul.left_distrib, *mul.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 whether 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
-- 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 into a + (b + c). Then, {b + _}add.comm applies commutativity to term b + c. Without the pattern {b + _}, the tactic would rewrite a + (b + c) into (b + c) + a. Finally, -add.assoc applies associativity in the “reverse direction” rewriting a + (c + b) into 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
-- 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 step add_zero at H rewrites the hypothesis (H : a + 0 = 0) into a = 0. Then, the “new” (H : a = 0) is used to rewrite the main goal into f 0 = f 0.

Multiple hypotheses can be specified in the same at clause.

import data.nat
open nat
-- 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

We 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. The character ⊢ is entered by typing \|-.

import data.nat
open nat
-- 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 into v : vector A 0.

import data.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), by default, the tactic rewrite t 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 existing theorems/lemmas and hypotheses as rewriting rules. In both cases, the term t is just an identifier. The notation rewrite (t) can be used to use an arbitrary term t as a rewriting rule.

import algebra.group
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⟩

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 following alternative ASCII notation is also supported ^f, >*, <D t, > t.

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. We discharge the inductive cases using the rewrite tactic. The base case is solved by simply 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) into a :: (s ++ t ++ u) = a :: s ++ (t ++ u) by applying the reduction step ▸ a :: (l ++ t ++ u) = _. The basic idea is to expose the term l ++ t ++ u that can be rewritten using the inductive hypothesis append_assoc (s t u : list A) : s ++ t ++ u = s ++ (t ++ u). Note that, we have 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. By using this placeholder, you do not have to “copy” the goal’s right-hand-side.

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

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