13_More_Tactics.org

Theorem Proving in Lean

More Tactics

We have seen that tactics provide a powerful language for describing and constructing proofs. Care is required: a proof that is a long string of tactic applications can be very hard to read and maintain. But when combined with the various structuring mechanisms that Lean’s proof language has to offer, they provide efficient means for filling in the details of a proof. The goal of this chapter is to add some additional tactics to your repertoire.

[This chapter is still under construction.]

Induction

Just as the cases tactic performs proof by cases on an element of an inductively defined type, the induction tactic performs a proof by induction. As with the cases tactic, the with clause allows you to name the variables and hypotheses that are introduced. Also as with the cases tactic, the induction tactic will revert any hypotheses that depend on the induction variable and then reintroduce them for you automatically. The following examples prove the commutativity of addition on the natural numbers, using only the defining equations for addition (in particular, the property add_succ, which asserts that x + succ y = succ (x + y) for every x and y).

import data.nat
namespace hide
-- BEGIN
open nat

theorem zero_add (x : ℕ) : 0 + x = x :=
begin
  induction x with x ih,
    {exact rfl},
  rewrite [add_succ, ih]
end

theorem succ_add (x y : ℕ) : succ x + y = succ (x + y) :=
begin
  induction y with y ih,
    {exact rfl},
  rewrite [add_succ, ih]
end

theorem add.comm (x y : ℕ) : x + y = y + x :=
begin
  induction x with x ih,
    {show 0 + y = y + 0, by rewrite zero_add},
  show succ x + y = y + succ x,
    begin
      induction y with y ihy,
        {krewrite zero_add},
      rewrite [succ_add, ih]
    end
end
-- END
end hide

(For the use of krewrite here, see the end of Chapter Tactic-Style Proofs.)

The induction tactic can be used not only with the induction principles that are created automatically when an inductive type is defined, but also induction principles that prove on their own. For example, recall that the standard library defines the type finset A of finite sets of elements of any type A. Typically, we assume A has decidable equality, which means in particular that we can decide whether an element a : A is a member of a finite set s. Clearly, a property P holds for an arbitrary finite set when it holds for the empty set and when it is maintained for a finite set s after a new element a, that was not previosly in s, is added to s. This is encapsulated by the following principle of induction:

open finset
namespace hide
-- BEGIN
theorem finset.induction {A : Type} [h : decidable_eq A] {P : finset A → Prop}
  (H₁ : P finset.empty)
  (H₂ : ∀ ⦃a : A⦄ {s : finset A}, a ∉ s → P s → P (insert a s))
  : (∀ s, P s)
-- END
  := sorry
end hide

To use this as an induction principle, one has to mark it with the attribute [recursor 6], which tells the induction tactic that this is a user defined induction principle in which induction is carried out on the sixth argument. This is done in the standard library. Then, when induction is carried out on an element of finset, the induction tactic finds the relevant principle.

import data.finset data.nat
open finset nat

variables (A : Type) [deceqA : decidable_eq A]
include deceqA

theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
begin
  induction s₂ with a s₂ hs₂ ih,
    show card s₁ + card (∅:finset A) = card (s₁ ∪ ∅) + card (s₁ ∩ ∅),
      by rewrite [union_empty, card_empty, inter_empty],
    show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a s₂)),
      from sorry
end

The proof is carried out by induction on s₂. According to the with clause, the inductive step concerns the set insert a s₂ in place of s₂, hs₂ denotes the assuption a ∉ s₂, and ih denotes the inductive hypothesis. (The full proof can be found in the library.) If necessary, we can specify the induction principle manually:

import data.finset data.nat
open finset nat

variables (A : Type) [deceqA : decidable_eq A]
include deceqA

-- BEGIN
theorem card_add_card (s₁ s₂ : finset A) : card s₁ + card s₂ = card (s₁ ∪ s₂) + card (s₁ ∩ s₂) :=
begin
  induction s₂ using finset.induction with a s₂ hs₂ ih,
    show card s₁ + card (∅:finset A) = card (s₁ ∪ ∅) + card (s₁ ∩ ∅),
      by rewrite [union_empty, card_empty, inter_empty],
    show card s₁ + card (insert a s₂) = card (s₁ ∪ (insert a s₂)) + card (s₁ ∩ (insert a s₂)),
      from sorry
end
-- END

Other Tactics

The tactic subst substitutes a variable defined in the context, and clears both the variable and the hypothesis. The tactic substvars substitutes all the variables in the context.

import data.nat
open nat

variables a b c d : ℕ

example (Ha : a = b + c) : c + a = c + (b + c) :=
by subst a

example (Ha : a = b + c) (Hd : d = b) : a + d = b + c + d :=
by subst [a, d]

example (Ha : a = b + c) (Hd : d = b) : a + d = b + c + d :=
by substvars

example (Ha : a = b + c) (Hd : b = d) : a + d = d + c + d :=
by substvars

example (Hd : b = d) (Ha : a = b + c) : a + d = d + c + d :=
by substvars

A number of tactics are designed to help construct elements of inductive types. For example constructor <i> constructs an element of an inductive type by applying the ith constructor; constructor alone applies the first constructor that succeeds. The tactic split can only be applied to inductive types with only one constructor, and is then equivalent to constructor 1. Similarly, left and right are designed for use with inductive types with two constructors, and are then equivalent to constructor 1 and constructor 2, respectively. Here are prototypical examples:

variables p q : Prop

example (Hp : p) (Hq : q) : p ∧ q :=
by split; exact Hp; exact Hq

example (Hp : p) (Hq : q) : p ∧ q :=
by split; repeat assumption

example (Hp : p) : p ∨ q :=
by constructor; assumption

example (Hq : q) : p ∨ q :=
by constructor; assumption

example (Hp : p) : p ∨ q :=
by constructor 1; assumption

example (Hq : q) : p ∨ q :=
by constructor 2; assumption

example (Hp : p) : p ∨ q :=
by left; assumption

example (Hq : q) : p ∨ q :=
by right; assumption

The tactic existsi is similar to constructor 1, but it allows us to provide an argument, as is commonly done with when introducing an element of an exists or sigma type.

import data.nat
open nat

example : ∃ x : ℕ, x > 2 :=
by existsi 3; exact dec_trivial

example (B : ℕ → Type) (b : B 2) : Σ x : ℕ, B x :=
by existsi 2; assumption

The injection tactic makes use of the fact that constructors to an inductive type are injective:

import data.nat
open nat

example (x y : ℕ) (H : succ x = succ y) : x = y :=
by injection H with H'; exact H'

example (x y : ℕ) (H : succ x = succ y) : x = y :=
by injection H; assumption

The first version gives the name the consequence of applying injectivity to the hypothesis H. The second version lets Lean choose the name.

The tactics reflexivity, symmetry, and transitivity work not just for equality, but also for any relation with a corresponding theorem marked with the attribute refl, symm, or trans, respectively. Here is an example of their use:

variables (A : Type) (a b c d : A)

example (H₁ : a = b) (H₂ : c = b) (H₃ : c = d) : a = d :=
by transitivity b; assumption; transitivity c; symmetry; assumption; assumption

The contradiction tactic closes a goal when contradictory hypotheses have been derived:

variables p q : Prop

example (Hp : p) (Hnp : ¬ p) : q :=
by contradiction

Similarly, exfalso and trivial implement “ex falso quodlibet” and the introduction rule for true, respectively.

Combinators

Combinators are used to combine tactics. The most basic one is the and_then combinator, written with a semicolon (;), which applies tactics successively.

The par combinator, written with a vertical bar (|), tries one tactic and then the other, using the first one that succeeds. The repeat tactic applies a tactic repeatedly. Here is an example of these in use:

example (a b c d : Prop) : a ∧ b ∧ c ∧ d ↔ d ∧ c ∧ b ∧ a :=
begin
  apply iff.intro,
  repeat (intro H; repeat (cases H with [H', H] | apply and.intro | assumption))
end

Here is another one:

import data.set
open set function eq.ops

variables {X Y Z : Type}

lemma image_comp (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
set.ext (take z,
  iff.intro
    (assume Hz,
      obtain x Hx₁ Hx₂, from Hz,
      by repeat (apply mem_image | assumption | reflexivity))
    (assume Hz,
      obtain y [x Hz₁ Hz₂] Hy₂, from Hz,
      by repeat (apply mem_image | assumption | esimp [comp] | rewrite Hz₂)))

Finally, some tactics can be used to “debug” a tactic proof by printing output to the screen when Lean is run from the command line. The command trace produces the given output, state shows the current goal, now fails if there are any current goals, and check_expr t displays the type of the expression in the context of the current goal.

open tactic

theorem tst {A B : Prop} (H1 : A) (H2 : B) : A :=
by (trace "first";  state; now  |
       trace "second"; state; fail |
       trace "third";  assumption)

Other tactics can be used to manipulate goals. For example, rotate_left or rotate_right followed by a number rotates through the goals. The tactic rotate is equivalent to rotate_left.