Theorem Proving in Lean 4

5. Tactics

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, you 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 you 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. For example, tactic-style proofs can be harder to read, because they require the reader to predict or guess the results of each instruction. But they can also be shorter and easier to write. Moreover, tactics offer a gateway to using Lean's automation, since automated procedures are themselves tactics.

5.1. Entering 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 declaration uses 'sorry'test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p All goals completed! 🐙

You can write this goal as follows:

p:Propq:Prophp:phq: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, you meet such a goal by writing an explicit term. But wherever a term is expected, Lean allows us to insert instead a by <tactics> block, where <tactics> is a sequence of commands, separated by semicolons or line breaks. You can prove the theorem above in that way:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

We often put the by keyword on the preceding line, and write the example above as:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

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:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p

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. It is also more robust than apply, since the elaborator takes the expected type, given by the target of the goal, into account when processing the expression that is being applied. In this case, however, apply would work just as well.

You can see the resulting proof term with the #print command:

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

You can write a tactic script incrementally. In VS Code, you can open a window to display messages by pressing CtrlShiftEnter, and that window will then show you the current goal whenever the cursor is in a tactic block. If the proof is incomplete, the token by is decorated with a red squiggly line, and the error message contains the remaining goals.

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

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p All goals completed! 🐙

Unsurprisingly, it produces exactly the same proof term:

theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p := fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩#print test
theorem test : ∀ (p q : Prop), p → q → p ∧ q ∧ p :=
fun p q hp hq => ⟨hp, ⟨hq, hp⟩⟩

Multiple tactic applications can be written in a single line by concatenating with a semicolon.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ q ∧ p; All goals completed! 🐙

Tactics that may produce multiple subgoals often tag them. For example, the tactic apply And.intro tagged the first subgoal as leftp:Propq:Prophp:phq:q⊢ p, and the second as rightp:Propq:Prophp:phq:q⊢ q ∧ p. In the case of the apply tactic, the tags are inferred from the parameters' names used in the And.intro declaration. You can structure your tactics using the notation case <tag> => <tactics>. The following is a structured version of our first tactic proof in this chapter.

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

You can solve the subgoal rightp:Propq:Prophp:phq:q⊢ q ∧ p before leftp:Propq:Prophp:phq:q⊢ p using the case notation:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p case right p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p case left p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 case right p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 case left p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

Note that Lean hides the other goals inside the case block. After case left =>, the proof state is:

p:Propq:Prophp:phq:q⊢ q

We say that case is “focusing” on the selected goal. Moreover, Lean flags an error if the selected goal is not fully solved at the end of the case block.

For simple subgoals, it may not be worth selecting a subgoal using its tag, but you may still want to structure the proof. Lean also provides the “bullet” notation . <tactics> (or · <tactics>) for structuring proofs:

theorem test (p q : Prop) (hp : p) (hq : q) : p ∧ q ∧ p := p:Propq:Prophp:phq:q⊢ p ∧ q ∧ p p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙 p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙

5.2. 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 a previous chapter, now proved using tactics.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ q → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ r → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r)p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ q → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpq:p ∧ q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ p All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ q ∨ r p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhpr:p ∧ r⊢ r All goals completed! 🐙

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

example (α : Type) : α → α := α:Type⊢ α → α α:Typea:α⊢ α All goals completed! 🐙 example (α : Type) : ∀ x : α, x = x := α:Type⊢ ∀ (x : α), x = x α:Typex:α⊢ x = x All goals completed! 🐙

You can use it to introduce several variables:

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a:Natb:Natc:Nath₁:a = bh₂:a = c⊢ c = b All goals completed! 🐙

As the apply tactic is a command for constructing function applications interactively, the intro tactic is a command for constructing function abstractions interactively (i.e., terms of the form fun x => e). As with lambda abstraction notation, the intro tactic allows us to use an implicit match.

example (p q : α → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x α:Sort u_1p:α → Propq:α → Propw:αhpw:p whqw:q w⊢ ∃ x, q x ∧ p x All goals completed! 🐙

You can also provide multiple alternatives like in the match expression.

example (p q : α → Prop) : (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x := α:Sort u_1p:α → Propq:α → Prop⊢ (∃ x, p x ∨ q x) → ∃ x, q x ∨ p x intro α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:p w⊢ ∃ x, q x ∨ p x All goals completed! 🐙 α:Sort u_1p:α → Propq:α → Propx✝:∃ x, p x ∨ q xw:αh:q w⊢ ∃ x, q x ∨ p x All goals completed! 🐙

The intros tactic can be used without any arguments, in which case, it chooses names and introduces as many variables as it can. You 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.

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ z = w All goals completed! 🐙 -- applied h₃

It will unify metavariables in the conclusion if necessary:

variable (x y z w : Nat) example (h₁ : x = y) (h₂ : y = z) (h₃ : z = w) : x = w := x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = w x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ x = ?bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = w -- solves x = ?b with h₁ x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ y = ?h₂.bx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ ?h₂.b = wx:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ Nat x:Naty:Natz:Natw:Nath₁:x = yh₂:y = zh₃:z = w⊢ z = w -- solves y = ?h₂.b with h₂ All goals completed! 🐙 -- solves z = w with h₃

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 := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ a✝² = b✝ All goals completed! 🐙

Note that names automatically generated by Lean are inaccessible by default. The motivation is to ensure your tactic proofs do not rely on automatically generated names, and are consequently more robust. However, you can use the combinator unhygienic to disable this restriction.

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b unhygienic a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = b a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ c = ?ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ca:Natb:Natc:Nata_1:a = ba_2:a = c⊢ ?b = ba:Natb:Natc:Nata_1:a = ba_2:a = c⊢ Nat a:Natb:Natc:Nata_1:a = ba_2:a = c⊢ a = b All goals completed! 🐙

You can also use the rename_i tactic to rename the most recent inaccessible names in your context. In the following example, the tactic rename_i h1 _ h2 renames two of the last three hypotheses in your context.

example : ∀ a b c d : Nat, a = b → a = d → a = c → c = b := ⊢ ∀ (a b c d : Nat), a = b → a = d → a = c → c = b a✝³:Natb✝:Natc✝:Natd✝:Nata✝²:a✝³ = b✝a✝¹:a✝³ = d✝a✝:a✝³ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ c✝ = b✝ a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ c✝ = ?ba✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ ?b = c✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ ?b = b✝a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ Nat a✝¹:Natb✝:Natc✝:Natd✝:Nath1:a✝¹ = b✝a✝:a✝¹ = d✝h2:a✝¹ = c✝⊢ a✝¹ = b✝ All goals completed! 🐙

The rfl tactic solves goals that are reflexive relations applied to definitionally equal arguments. Equality is reflexive:

example (y : Nat) : (fun unused variable `x` note: this linter can be disabled with `set_option linter.unusedVariables false`x : Nat => 0) y = 0 := y:Nat⊢ (fun x => 0) y = 0 All goals completed! 🐙

The repeat combinator can be used to apply a tactic several times:

example : ∀ a b c : Nat, a = b → a = c → c = b := ⊢ ∀ (a b c : Nat), a = b → a = c → c = b a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = b✝ a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ c✝ = ?ba✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = c✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ ?b = b✝a✝²:Natb✝:Natc✝:Nata✝¹:a✝² = b✝a✝:a✝² = c✝⊢ Nat repeat All goals completed! 🐙

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

example (x : Nat) : x = x := x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

After revert x, the proof state is:

⊢ ∀ (x : Nat), x = x

After intro y, it is:

y:Nat⊢ y = y

Moving a hypothesis into the goal yields an implication:

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x x:Naty:Nat⊢ x = y → y = x x:Naty:Nath₁:x = y⊢ y = x -- goal is x y : Nat, h₁ : x = y ⊢ y = x x:Naty:Nath₁:x = y⊢ x = y All goals completed! 🐙

After revert h, the proof state is:

x:Naty:Nat⊢ x = y → y = x

After intro h₁, it is:

x:Naty:Nath₁:x = y⊢ y = x

But revert is even more clever, in that it will revert not only an element of the context but also all the subsequent elements of the context that depend on it. For example, reverting x in the example above brings h along with it:

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x y:Nat⊢ ∀ (x : Nat), x = y → y = x y:Natx✝:Nath✝:x✝ = y⊢ y = x✝ y:Natx✝:Nath✝:x✝ = y⊢ x✝ = y All goals completed! 🐙

After revert x, the goal is:

y:Nat⊢ ∀ (x : Nat), x = y → y = x

You can also revert multiple elements of the context at once:

example (x y : Nat) (h : x = y) : y = x := x:Naty:Nath:x = y⊢ y = x ⊢ ∀ (x y : Nat), x = y → y = x x✝:Naty✝:Nath✝:x✝ = y✝⊢ y✝ = x✝ x✝:Naty✝:Nath✝:x✝ = y✝⊢ x✝ = y✝ All goals completed! 🐙

After revert x y, the goal is:

⊢ ∀ (x y : Nat), x = y → y = x

You can only revert an element of the local context, that is, a local variable or hypothesis. But you can replace an arbitrary expression in the goal by a fresh variable using the generalize tactic:

example : 3 = 3 := ⊢ 3 = 3 x:Nat⊢ x = x ⊢ ∀ (x : Nat), x = x y:Nat⊢ y = y All goals completed! 🐙

In particular, after generalize, the goal is

x:Nat⊢ x = x

The mnemonic in the notation above is that you are generalizing the goal by setting 3 to an arbitrary variable x. Be careful: not every generalization preserves the validity of the goal. Here, generalize replaces a goal that could be proved using rfl with one that is not provable:

declaration uses 'sorry'example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nat⊢ 2 + x = 5 All goals completed! 🐙

In this example, the sorry tactic is the analogue of the sorry proof term. It closes the current goal, producing the usual warning that sorry has been used. To preserve the validity of the previous goal, the generalize tactic allows us to record the fact that 3 has been replaced by x. All you need to do is to provide a label, and generalize uses it to store the assignment in the local context:

example : 2 + 3 = 5 := ⊢ 2 + 3 = 5 x:Nath:3 = x⊢ 2 + x = 5 All goals completed! 🐙

Following generalize h : 3 = x, h is a proof that 3 = x:

x:Nath:3 = x⊢ 2 + x = 5

Here the rewriting tactic rw uses h to replace x by 3 again. The rw tactic will be discussed below.

5.3. More Tactics🔗

Some additional tactics are useful for constructing and destructing propositions and data. For example, when applied to a goal of the form p ∨ q, you use tactics such as apply Or.inl and apply Or.inr. Conversely, the cases tactic can be used to decompose a disjunction:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙 p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙

Note that the syntax is similar to the one used in match expressions. The new subgoals can be solved in any order:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p cases h with p:Propq:Prophq:q⊢ q ∨ p p:Propq:Prophq:q⊢ q; All goals completed! 🐙 p:Propq:Prophp:p⊢ q ∨ p p:Propq:Prophp:p⊢ p; All goals completed! 🐙

You can also use a (unstructured) cases without the with and a tactic for each alternative:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙

The (unstructured) cases is particularly useful when you can close several subgoals using the same tactic:

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p repeat All goals completed! 🐙

You can also use the combinator tac1 <;> tac2 to apply tac2 to each subgoal produced by tactic tac1:

example (p : Prop) : p ∨ p → p := p:Prop⊢ p ∨ p → p p:Proph:p ∨ p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p p:Proph✝:p⊢ pp:Proph✝:p⊢ p All goals completed! 🐙

You can combine the unstructured cases tactic with the case and . notation:

example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙 p:Propq:Proph✝:q⊢ q ∨ p p:Propq:Proph✝:q⊢ q All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 case inl h p:Propq:Proph:p⊢ q ∨ p p:Propq:Proph:p⊢ p All goals completed! 🐙 example (p q : Prop) : p ∨ q → q ∨ p := p:Propq:Prop⊢ p ∨ q → q ∨ p p:Propq:Proph:p ∨ q⊢ q ∨ p p:Propq:Proph✝:p⊢ q ∨ pp:Propq:Proph✝:q⊢ q ∨ p case inr h p:Propq:Proph:q⊢ q ∨ p p:Propq:Proph:q⊢ q All goals completed! 🐙 p:Propq:Proph✝:p⊢ q ∨ p p:Propq:Proph✝:p⊢ p All goals completed! 🐙

The cases tactic can also be used to decompose a conjunction:

example (p q : Prop) : p ∧ q → q ∧ p := p:Propq:Prop⊢ p ∧ q → q ∧ p p:Propq:Proph:p ∧ q⊢ q ∧ p cases h with p:Propq:Prophp:phq:q⊢ q ∧ p p:Propq:Prophp:phq:q⊢ qp:Propq:Prophp:phq:q⊢ p; p:Propq:Prophp:phq:q⊢ p; All goals completed! 🐙

In this example, there is only one goal after the cases tactic is applied, with h : p ∧ q replaced by a pair of assumptions, hp : p and hq : q:

p:Propq:Prophp:phq:q⊢ q ∧ p

The constructor tactic applies the unique constructor for conjunction, And.intro.

With these tactics, an example from the previous section can be rewritten as follows:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h with p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:q⊢ p ∧ q; p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q p:Propq:Propr:Prophp:ph✝:q⊢ pp:Propq:Propr:Prophp:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:ph✝:r⊢ p ∧ r; p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r p:Propq:Propr:Prophp:ph✝:r⊢ pp:Propq:Propr:Prophp:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) cases hpq with p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phq:q⊢ pp:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q ∨ r; p:Propq:Propr:Prophp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) cases hpr with p:Propq:Propr:Prophp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophp:phr:r⊢ pp:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ q ∨ r; p:Propq:Propr:Prophp:phr:r⊢ r; All goals completed! 🐙

You will see in Inductive Types that these tactics are quite general. The cases tactic can be used to decompose any element of an inductively defined type; constructor always applies the first applicable constructor of an inductively defined type. For example, you can use cases and constructor with an existential quantifier:

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.w ∨ q ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p ?intro.wp:Nat → Propq:Nat → Propx:Natpx:p x⊢ Nat; All goals completed! 🐙

Here, the constructor tactic leaves the first component of the existential assertion, the value of x, implicit. It is represented by a metavariable, which should be instantiated later on. In the previous example, the proper value of the metavariable is determined by the tactic exact px, since px has type p x. If you want to specify a witness to the existential quantifier explicitly, you can use the exists tactic instead:

example (p q : Nat → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x) → ∃ x, p x ∨ q x p:Nat → Propq:Nat → Proph:∃ x, p x⊢ ∃ x, p x ∨ q x cases h with p:Nat → Propq:Nat → Propx:Natpx:p x⊢ ∃ x, p x ∨ q x p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x ∨ q x; p:Nat → Propq:Nat → Propx:Natpx:p x⊢ p x; All goals completed! 🐙

Here is another example:

example (p q : Nat → Prop) : (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x := p:Nat → Propq:Nat → Prop⊢ (∃ x, p x ∧ q x) → ∃ x, q x ∧ p x p:Nat → Propq:Nat → Proph:∃ x, p x ∧ q x⊢ ∃ x, q x ∧ p x cases h with p:Nat → Propq:Nat → Propx:Nathpq:p x ∧ q x⊢ ∃ x, q x ∧ p x cases hpq with p:Nat → Propq:Nat → Propx:Nathp:p xhq:q x⊢ ∃ x, q x ∧ p x All goals completed! 🐙

These tactics can be used on data just as well as propositions. In the next example, they are used to define functions which swap the components of the product and sum types:

def swap_pair : α × β → β × α := α:Type ?u.18β:Type ?u.17⊢ α × β → β × α α:Type ?u.18β:Type ?u.17p:α × β⊢ β × α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ β × α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ βα:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ α α:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ βα:Type ?u.18β:Type ?u.17fst✝:αsnd✝:β⊢ α All goals completed! 🐙 def swap_sum : Sum α β → Sum β α := α:Type ?u.116β:Type ?u.115⊢ α ⊕ β → β ⊕ α α:Type ?u.116β:Type ?u.115p:α ⊕ β⊢ β ⊕ α α:Type ?u.116β:Type ?u.115val✝:α⊢ β ⊕ αα:Type ?u.116β:Type ?u.115val✝:β⊢ β ⊕ α α:Type ?u.116β:Type ?u.115val✝:α⊢ β ⊕ α α:Type ?u.116β:Type ?u.115val✝:α⊢ α; All goals completed! 🐙 α:Type ?u.116β:Type ?u.115val✝:β⊢ β ⊕ α α:Type ?u.116β:Type ?u.115val✝:β⊢ β; All goals completed! 🐙

Note that up to the names we have chosen for the variables, the definitions are identical to the proofs of the analogous propositions for conjunction and disjunction. The cases tactic will also do a case distinction on a natural number:

open Nat example (P : Nat → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : Nat) : P m := P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm:Nat⊢ P m cases m with P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succ⊢ P 0 All goals completed! 🐙 P:Nat → Proph₀:P 0h₁:∀ (n : Nat), P n.succm':Nat⊢ P (m' + 1) All goals completed! 🐙

The cases tactic, and its companion, the induction tactic, are discussed in greater detail in the Tactics for Inductive Types section.

The contradiction tactic searches for a contradiction among the hypotheses of the current goal:

example (p q : Prop) : p ∧ ¬ p → q := p:Propq:Prop⊢ p ∧ ¬p → q p:Propq:Proph:p ∧ ¬p⊢ q p:Propq:Propleft✝:pright✝:¬p⊢ q All goals completed! 🐙

You can also use match in tactic blocks.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r match h with p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ p ∧ q; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:q⊢ q All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r p:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ pp:Propq:Propr:Proph:p ∧ (q ∨ r)left✝:ph✝:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) match h with p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Proph:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

You can “combine” intro with match and write the previous examples as follows:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r intro p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phq:q⊢ q All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ r; p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r p:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ (q ∨ r)hp:phr:r⊢ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) intro p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phq:q⊢ q; All goals completed! 🐙 p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ p ∧ (q ∨ r) p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ pp:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ q ∨ r; p:Propq:Propr:Propx✝:p ∧ q ∨ p ∧ rhp:phr:r⊢ r; All goals completed! 🐙

5.4. Structuring Tactic Proofs🔗

Tactics often provide an efficient way of building a proof, but long sequences of instructions can obscure the structure of the argument. In this section, we describe some means that help provide structure to a tactic-style proof, making such proofs more readable and robust.

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, and so on. Conversely, when writing an arbitrary Lean term, you can always invoke the tactic mode by inserting a by block. The following is a somewhat toy example:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r exact have hp : p := h.left have hqr : q ∨ r := h.right show (p ∧ q) ∨ (p ∧ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:phq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hp:phr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙

The following is a more natural example:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

In fact, there is a show tactic, which is similar to the show expression in a proof term. It simply declares the type of the goal that is about to be solved, while remaining in tactic mode.

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r cases h.right with p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hq:q⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)hr:r⊢ p ∧ q ∨ p ∧ r All goals completed! 🐙 p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r) cases h with p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r) All goals completed! 🐙 p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r) All goals completed! 🐙

The show tactic can actually be used to rewrite a goal to something definitionally equivalent:

example (n : Nat) : n + 1 = Nat.succ n := n:Nat⊢ n + 1 = n.succ n:Nat⊢ n.succ = n.succ All goals completed! 🐙

There is also a have tactic, which introduces a new subgoal, just as when writing proof terms:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qhpq:p ∧ q⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rhpr:p ∧ r⊢ p ∧ r All goals completed! 🐙

As with proof terms, you can omit the label in the have tactic, in which case, the default label this is used:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ r All goals completed! 🐙

The types in a have tactic can be omitted, so you can write have hp := h.left and have hqr := h.right. In fact, with this notation, you can even omit both the type and the label, in which case the new fact is introduced with the label this:

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phqr:q ∨ r⊢ p ∧ q ∨ p ∧ r cases hqr with p:Propq:Propr:Prophp:phq:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phq:qthis:p ∧ q⊢ p ∧ q; All goals completed! 🐙 p:Propq:Propr:Prophp:phr:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Prophp:phr:rthis:p ∧ r⊢ p ∧ r; All goals completed! 🐙

Lean also has a let tactic, which is similar to the have tactic, but is used to introduce local definitions instead of auxiliary facts. It is the tactic analogue of a let in a proof term:

example : ∃ x, x + 2 = 8 := ⊢ ∃ x, x + 2 = 8 a:Nat := 3 * 2⊢ ∃ x, x + 2 = 8 All goals completed! 🐙

As with have, you can leave the type implicit by writing let a := 3 * 2. The difference between let and have is that let introduces a local definition in the context, so that the definition of the local declaration can be unfolded in the proof.

We have used . to create nested tactic 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. The notation . is whitespace sensitive and relies on the indentation to detect whether the tactic block ends. Alternatively, you can define tactic blocks using curly braces and semicolons:

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) := p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ rp:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Prop⊢ p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ rp:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:q⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r p:Propq:Propr:Proph:p ∧ (q ∨ r)h✝:r⊢ p ∧ q ∨ p ∧ r; All goals completed! 🐙 } } p:Propq:Propr:Prop⊢ p ∧ q ∨ p ∧ r → p ∧ (q ∨ r) p:Propq:Propr:Proph:p ∧ q ∨ p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r)p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ q⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpq:p ∧ q⊢ p ∧ (q ∨ r); All goals completed! 🐙 } p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r) p:Propq:Propr:Proph✝:p ∧ r⊢ p ∧ (q ∨ r); p:Propq:Propr:Prophpr:p ∧ r⊢ p ∧ (q ∨ r); All goals completed! 🐙 } }

It is useful to use indentation to structure proof: every time a tactic leaves more than one subgoal, we separate the remaining subgoals by enclosing them in blocks and indenting. Thus if the application of theorem foo to a single goal produces four subgoals, one would expect the proof to look like this:

  apply foo
  . <proof of first goal>
  . <proof of second goal>
  . <proof of third goal>
  . <proof of final goal>

or

  apply foo
  case <tag of first goal>  => <proof of first goal>
  case <tag of second goal> => <proof of second goal>
  case <tag of third goal>  => <proof of third goal>
  case <tag of final goal>  => <proof of final goal>

or

  apply foo
  { <proof of first goal>  }
  { <proof of second goal> }
  { <proof of third goal>  }
  { <proof of final goal>  }

5.5. Tactic Combinators🔗

Tactic combinators are operations that form new tactics from old ones. A sequencing combinator is already implicit in the by block:

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q p:Propq:Prophp:p⊢ p; All goals completed! 🐙

Here, apply Or.inl; assumption is functionally equivalent to a single tactic which first applies apply Or.inl and then applies assumption.

In t₁ <;> t₂, the <;> operator provides a parallel version of the sequencing operation: t₁ is applied to the current goal, and then t₂ is applied to all the resulting subgoals:

example (p q : Prop) (hp : p) (hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q All goals completed! 🐙

This is especially useful when the resulting goals can be finished off in a uniform way, or, at least, when it is possible to make progress on all of them uniformly.

The first | t₁ | t₂ | ... | tₙ applies each tᵢ until one succeeds, or else fails:

example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q first | p:Propq:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr; assumption example (p q : Prop) (hq : q) : p ∨ q := p:Propq:Prophq:q⊢ p ∨ q first | p:Propq:Prophq:q⊢ p; p:Propq:Prophq:q⊢ p | p:Propq:Prophq:q⊢ q; All goals completed! 🐙

In the first example, the left branch succeeds, whereas in the second one, it is the right one that succeeds. In the next three examples, the same compound tactic succeeds in each case:

example (p q r : Prop) (hp : p) : p ∨ q ∨ r := p:Propq:Propr:Prophp:p⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophp:p⊢ p; All goals completed! 🐙 | apply Or.inr | assumption) example (p q r : Prop) (hq : q) : p ∨ q ∨ r := p:Propq:Propr:Prophq:q⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophq:q⊢ q; All goals completed! 🐙 | p:Propq:Propr:Prophq:q⊢ q ∨ r | assumption) example (p q r : Prop) (hr : r) : p ∨ q ∨ r := p:Propq:Propr:Prophr:r⊢ p ∨ q ∨ r repeat (first | p:Propq:Propr:Prophr:r⊢ r; p:Propq:Propr:Prophr:r⊢ q | p:Propq:Propr:Prophr:r⊢ r | All goals completed! 🐙)

The tactic tries to solve the left disjunct immediately by assumption; if that fails, it tries to focus on the right disjunct; and if that doesn't work, it invokes the assumption tactic.

You will have no doubt noticed by now that tactics can fail. Indeed, it is the “failure” state that causes the first combinator to backtrack and try the next tactic. The try combinator builds a tactic that always succeeds, though possibly in a trivial way: try t executes t and reports success, even if t fails. It is equivalent to first| t |skip, where skip is a tactic that does nothing (and succeeds in doing so). In the next example, the second constructor succeeds on the right conjunct q ∧ r (remember that disjunction and conjunction associate to the right) but fails on the first. The try tactic ensures that the sequential composition succeeds:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r All goals completed! 🐙

Be careful: repeat (try t) will loop forever, because the inner tactic never fails.

In a proof, there are often multiple goals outstanding. Parallel sequencing is one way to arrange it so that a single tactic is applied to multiple goals, but there are other ways to do this. For example, all_goals t applies t to all open goals:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r all_goals (try p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r) all_goals All goals completed! 🐙

In this case, the any_goals tactic provides a more robust solution. It is similar to all_goals, except it succeeds if its argument succeeds on at least one goal:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ q ∧ r := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ q ∧ r p:Propq:Propr:Prophp:phq:qhr:r⊢ pp:Propq:Propr:Prophp:phq:qhr:r⊢ q ∧ r any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ qp:Propq:Propr:Prophp:phq:qhr:r⊢ r any_goals All goals completed! 🐙

The first tactic in the by block below repeatedly splits conjunctions:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals p:Propq:Propr:Prophp:phq:qhr:r⊢ p) all_goals All goals completed! 🐙

In fact, we can compress the full tactic down to one line:

example (p q r : Prop) (hp : p) (hq : q) (hr : r) : p ∧ ((p ∧ q) ∧ r) ∧ (q ∧ r ∧ p) := p:Propq:Propr:Prophp:phq:qhr:r⊢ p ∧ ((p ∧ q) ∧ r) ∧ q ∧ r ∧ p repeat (any_goals (first | p:Propq:Propr:Prophp:phq:qhr:r⊢ p | All goals completed! 🐙))

The combinator focus t ensures that t only effects the current goal, temporarily hiding the others from the scope. So, if t ordinarily only effects the current goal, focus (all_goals t) has the same effect as t.

5.6. Rewriting🔗

The rw tactic and the simp tactic were introduced briefly in Calculational Proofs. In this section and the next, we discuss them in greater detail.

The rw tactic provides a basic mechanism for applying substitutions to goals and hypotheses, providing a convenient and efficient way of working with equality. The most basic form of the tactic is rw [t], where t is a term whose type asserts an equality. For example, t can be a hypothesis h : x = y in the context; it can be a general lemma, like add_comm : ∀ x y, x + y = y + x, in which the rewrite tactic tries to find suitable instantiations of x and y; or it can be any compound term asserting a concrete or general equation. In the following example, we use this basic form to rewrite the goal using a hypothesis.

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f 0 = 0 -- replace k with 0 All goals completed! 🐙 -- replace f 0 with 0

In the example above, the first use of rw replaces k with 0 in the goal f k = 0. Then, the second one replaces f 0 with 0. The tactic automatically closes any goal of the form t = t. Here is an example of rewriting using a compound expression:

example (x y : Nat) (p : Nat → Prop) (q : Prop) (h : q → x = y) (h' : p y) (hq : q) : p x := x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p x x:Naty:Natp:Nat → Propq:Proph:q → x = yh':p yhq:q⊢ p y; All goals completed! 🐙

Here, h hq establishes the equation x = y.

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

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

By default, rw 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.

variable (a b : Nat) (f : Nat → Nat) example (h₁ : a = b) (h₂ : f a = 0) : f b = 0 := a:Natb:Natf:Nat → Nath₁:a = bh₂:f a = 0⊢ f b = 0 All goals completed! 🐙

In this example, the term ←h₁ instructs the rewriter to replace b with a. In the editors, you can type the backwards arrow as \l. You can also use the ASCII equivalent, <-.

Sometimes the left-hand side of an identity can match more than one subterm in the pattern, in which case the rw tactic chooses the first match it finds when traversing the term. If that is not the one you want, you can use additional arguments to specify the appropriate subterm.

example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙 example (a b c : Nat) : a + b + c = a + c + b := a:Natb:Natc:Nat⊢ a + b + c = a + c + b All goals completed! 🐙
example (f : Nat → Nat) (a : Nat) (h : a + 0 = 0) : f a = f 0 := f:Nat → Nata:Nath:a + 0 = 0⊢ f a = f 0 f:Nat → Nata:Nath:a = 0⊢ f a = f 0 All goals completed! 🐙

The first step, rw [Nat.add_zero] at h, rewrites the hypothesis a + 0 = 0 to a = 0. Then the new hypothesis a = 0 is used to rewrite the goal to f 0 = f 0.

The rw tactic is not restricted to propositions. In the following example, we use rw [h] at t to rewrite the hypothesis t : Tuple α n to t : Tuple α 0.

def Tuple (α : Type) (n : Nat) := { as : List α // as.length = n } example (n : Nat) (h : n = 0) (t : Tuple α n) : Tuple α 0 := α:Typen:Nath:n = 0t:Tuple α n⊢ Tuple α 0 α:Typen:Nath:n = 0t:Tuple α 0⊢ Tuple α 0 All goals completed! 🐙

5.7. Using the Simplifier🔗

Whereas rw is designed as a surgical tool for manipulating a goal, the simplifier offers a more powerful form of automation. A number of identities in Lean's library have been tagged with the [simp] attribute, and the simp tactic uses them to iteratively rewrite subterms in an expression.

example (x y z : Nat) : (x + 0) * (0 + y * 1 + z * 0) = x * y := x:Naty:Natz:Nat⊢ (x + 0) * (0 + y * 1 + z * 0) = x * y All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h : p (x * y)) : p ((x + 0) * (0 + y * 1 + z * 0)) := x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p ((x + 0) * (0 + y * 1 + z * 0)) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

In the first example, the left-hand side of the equality in the goal is simplified using the usual identities involving 0 and 1, reducing the goal to x * y = x * y. At that point, simp applies reflexivity to finish it off. In the second example, simp reduces the goal to p (x * y), at which point the assumption h finishes it off. Here are some more examples with lists:

open List example (xs : List Nat) : reverse (xs ++ [1, 2, 3]) = [3, 2, 1] ++ reverse xs := xs:List Nat⊢ (xs ++ [1, 2, 3]).reverse = [3, 2, 1] ++ xs.reverse All goals completed! 🐙 example (xs ys : List α) : length (reverse (xs ++ ys)) = length xs + length ys := α:Type u_1xs:List αys:List α⊢ (xs ++ ys).reverse.length = xs.length + ys.length All goals completed! 🐙

As with rw, you can use the keyword at to simplify a hypothesis:

example (x y z : Nat) (p : Nat → Prop) (h : p ((x + 0) * (0 + y * 1 + z * 0))) : p (x * y) := x:Naty:Natz:Natp:Nat → Proph:p ((x + 0) * (0 + y * 1 + z * 0))⊢ p (x * y) x:Naty:Natz:Natp:Nat → Proph:p (x * y)⊢ p (x * y); All goals completed! 🐙

Moreover, you can use a “wildcard” asterisk to simplify all the hypotheses and the goal:

attribute [local simp] Nat.mul_comm Nat.mul_assoc Nat.mul_left_comm attribute [local simp] Nat.add_assoc Nat.add_comm Nat.add_left_comm example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙 example (x y z : Nat) (p : Nat → Prop) (h₁ : p (1 * x + y)) (h₂ : p (x * z * 1)) : p (y + 0 + x) ∧ p (z * x) := x:Naty:Natz:Natp:Nat → Proph₁:p (1 * x + y)h₂:p (x * z * 1)⊢ p (y + 0 + x) ∧ p (z * x) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y) ∧ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x + y)x:Naty:Natz:Natp:Nat → Proph₁:p (x + y)h₂:p (x * z)⊢ p (x * z) All goals completed! 🐙

For operations that are commutative and associative, like multiplication on the natural numbers, the simplifier uses these two facts to rewrite an expression, as well as left commutativity. In the case of multiplication the latter is expressed as follows: x * (y * z) = y * (x * z). The local modifier tells the simplifier to use these rules in the current file (or section or namespace, as the case may be). It may seem that commutativity and left-commutativity are problematic, in that repeated application of either causes looping. But the simplifier detects identities that permute their arguments, and uses a technique known as ordered rewriting. This means that the system maintains an internal ordering of terms, and only applies the identity if doing so decreases the order. With the three identities mentioned above, this has the effect that all the parentheses in an expression are associated to the right, and the expressions are ordered in a canonical (though somewhat arbitrary) way. Two expressions that are equivalent up to associativity and commutativity are then rewritten to the same canonical form.

example (w x y z : Nat) (unused variable `p` note: this linter can be disabled with `set_option linter.unusedVariables false`p : Nat → Prop) : x * y + z * w * x = x * w * z + y * x := w:Natx:Naty:Natz:Natp:Nat → Prop⊢ x * y + z * w * x = x * w * z + y * x All goals completed! 🐙 example (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)) : p (x * w * z + y * x) := w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * w * z + y * x) w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + z * w * x)⊢ p (x * y + w * (x * z)); w:Natx:Naty:Natz:Natp:Nat → Proph:p (x * y + w * (x * z))⊢ p (x * y + w * (x * z)); All goals completed! 🐙

As with rw, you can send simp a list of facts to use, including general lemmas, local hypotheses, definitions to unfold, and compound expressions. The simp tactic also recognizes the ←t syntax that rewrite does. In any case, the additional rules are added to the collection of identities that are used to simplify a term.

def f (m n : Nat) : Nat := m + n + m example {m n : Nat} (h : n = 1) (h' : 0 = m) : (f m n) = n := m:Natn:Nath:n = 1h':0 = m⊢ f m n = n All goals completed! 🐙

A common idiom is to simplify a goal using local hypotheses:

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

To use all the hypotheses present in the local context when simplifying, we can use the wildcard symbol, *:

variable (k : Nat) (f : Nat → Nat) example (h₁ : f 0 = 0) (h₂ : k = 0) : f k = 0 := k:Natf:Nat → Nath₁:f 0 = 0h₂:k = 0⊢ f k = 0 All goals completed! 🐙

Here is another example:

example (u w x y z : Nat) (h₁ : x = y + z) (h₂ : w = u + x) : w = z + y + u := u:Natw:Natx:Naty:Natz:Nath₁:x = y + zh₂:w = u + x⊢ w = z + y + u All goals completed! 🐙

The simplifier will also do propositional rewriting. For example, using the hypothesis p, it rewrites p ∧ q to q and p ∨ q to True, which it then proves trivially. Iterating such rewrites produces nontrivial propositional reasoning.

example (p q : Prop) (hp : p) : p ∧ q ↔ q := p:Propq:Prophp:p⊢ p ∧ q ↔ q All goals completed! 🐙 example (p q : Prop) (hp : p) : p ∨ q := p:Propq:Prophp:p⊢ p ∨ q All goals completed! 🐙 example (p q r : Prop) (hp : p) (hq : q) : p ∧ (q ∨ r) := p:Propq:Propr:Prophp:phq:q⊢ p ∧ (q ∨ r) All goals completed! 🐙

The next example simplifies all the hypotheses, and then uses them to prove the goal.

example (unused variable `u` note: this linter can be disabled with `set_option linter.unusedVariables false`u unused variable `w` note: this linter can be disabled with `set_option linter.unusedVariables false`w x x' y y' unused variable `z` note: this linter can be disabled with `set_option linter.unusedVariables false`z : Nat) (unused variable `p` note: this linter can be disabled with `set_option linter.unusedVariables false`p : Nat → Prop) (h₁ : x + 0 = x') (h₂ : y + 0 = y') : x + y + 0 = x' + y' := u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x + 0 = x'h₂:y + 0 = y'⊢ x + y + 0 = x' + y' u:Natw:Natx:Natx':Naty:Naty':Natz:Natp:Nat → Proph₁:x = x'h₂:y = y'⊢ x + y = x' + y' All goals completed! 🐙

One thing that makes the simplifier especially useful is that its capabilities can grow as a library develops. For example, suppose we define a list operation that symmetrizes its input by appending its reversal:

def mk_symm (xs : List α) := xs ++ xs.reverse

Then for any list xs, (mk_symm xs).reverse is equal to mk_symm xs, which can easily be proved by unfolding the definition:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙

We can now use this theorem to prove new results:

example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

But using reverse_mk_symm is generally the right thing to do, and it would be nice if users did not have to invoke it explicitly. You can achieve that by marking it as a simplification rule when the theorem is defined:

@[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

The notation @[simp] declares reverse_mk_symm to have the [simp] attribute, and can be spelled out more explicitly:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

The attribute can also be applied any time after the theorem is declared:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 attribute [simp] reverse_mk_symm example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙

Once the attribute is applied, however, there is no way to permanently remove it; it persists in any file that imports the one where the attribute is assigned. As we will discuss further in Attributes, one can limit the scope of an attribute to the current file or section using the local modifier:

theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 section attribute [local simp] reverse_mk_symm example (xs ys : List Nat) : (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse := xs:List Natys:List Nat⊢ (xs ++ mk_symm ys).reverse = mk_symm ys ++ xs.reverse All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 end

Outside the section, the simplifier will no longer use reverse_mk_symm by default.

Note that the various simp options we have discussed—giving an explicit list of rules, and using at to specify the location—can be combined, but the order they are listed is rigid. You can see the correct order in an editor by placing the cursor on the simp identifier to see the documentation string that is associated with it.

There are two additional modifiers that are useful. By default, simp includes all theorems that have been marked with the attribute [simp]. Writing simp only excludes these defaults, allowing you to use a more explicitly crafted list of rules. In the examples below, the minus sign and only are used to block the application of reverse_mk_symm.

def mk_symm (xs : List α) := xs ++ xs.reverse @[simp] theorem reverse_mk_symm (xs : List α) : (mk_symm xs).reverse = mk_symm xs := α:Type u_1xs:List α⊢ (mk_symm xs).reverse = mk_symm xs All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p (mk_symm ys ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p (mk_symm ys ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p (mk_symm ys ++ xs.reverse)⊢ p (mk_symm ys ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙 example (xs ys : List Nat) (p : List Nat → Prop) (h : p (xs ++ mk_symm ys).reverse) : p ((mk_symm ys).reverse ++ xs.reverse) := xs:List Natys:List Natp:List Nat → Proph:p (xs ++ mk_symm ys).reverse⊢ p ((mk_symm ys).reverse ++ xs.reverse) xs:List Natys:List Natp:List Nat → Proph:p ((mk_symm ys).reverse ++ xs.reverse)⊢ p ((mk_symm ys).reverse ++ xs.reverse); All goals completed! 🐙

The simp tactic has many configuration options. For example, we can enable contextual simplifications as follows:

example : if x = 0 then y + x = y else x ≠ 0 := x:Naty:Nat⊢ if x = 0 then y + x = y else x ≠ 0 All goals completed! 🐙

With +contextual, the simp tactic uses the fact that x = 0 when simplifying y + x = y, and x ≠ 0 when simplifying the other branch. Here is another example:

example : ∀ (x : Nat) (unused variable `h` note: this linter can be disabled with `set_option linter.unusedVariables false`h : x = 0), y + x = y := y:Nat⊢ ∀ (x : Nat), x = 0 → y + x = y All goals completed! 🐙

Another useful configuration option is +arith which enables arithmetical simplifications.

example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := x:Naty:Nat⊢ 0 < 1 + x ∧ x + y + 2 ≥ y + 1 All goals completed! 🐙

5.8. Split Tactic🔗

The split tactic is useful for breaking nested if-then-else and match expressions in cases. For a match expression with n cases, the split tactic generates at most n subgoals. Here is an example:

def f (x y z : Nat) : Nat := match x, y, z with | 5, _, _ => y | _, 5, _ => y | _, _, 5 => y | _, _, _ => 1 example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1 All goals completed! 🐙 w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1 All goals completed! 🐙 x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1 All goals completed! 🐙 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 All goals completed! 🐙

We can compress the tactic proof above as follows.

example (x y z : Nat) : x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 := w:Natx:Naty:Natz:Nat⊢ x ≠ 5 → y ≠ 5 → z ≠ 5 → z = w → f x y w = 1 w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ f x y w = 1; w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = w⊢ (match x, y, w with | 5, x, x_1 => y | x, 5, x_1 => y | x, x_1, 5 => y | x, x_1, x_2 => 1) = 1; w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 w:Naty:Natz:Nata✝³:y ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝:Naty✝:Natz✝:Nata✝:5 ≠ 5⊢ y = 1w:Natx:Natz:Nata✝³:x ≠ 5a✝²:z ≠ 5a✝¹:z = wx✝¹:Naty✝:Natz✝:Natx✝:x = 5 → Falsea✝:5 ≠ 5⊢ 5 = 1x:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5x✝²:Naty✝:Natz✝:Natx✝¹:x = 5 → Falsex✝:y = 5 → Falsea✝:z = 5⊢ y = 1w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 first | w:Natx:Naty:Natz:Nata✝³:x ≠ 5a✝²:y ≠ 5a✝¹:z ≠ 5a✝:z = wx✝³:Naty✝:Natz✝:Natx✝²:x = 5 → Falsex✝¹:y = 5 → Falsex✝:w = 5 → False⊢ 1 = 1 | All goals completed! 🐙

The tactic split <;> first | contradiction | rfl first applies the split tactic, and then for each generated goal it tries contradiction, and then rfl if contradiction fails. Like simp, we can apply split to a particular hypothesis:

def g (xs ys : List Nat) : Nat := match xs, ys with | [a, b], _ => a+b+1 | _, [b, unused variable `c` note: this linter can be disabled with `set_option linter.unusedVariables false`c] => b+1 | _, _ => 1 example (xs ys : List Nat) (h : g xs ys = 0) : False := xs:List Natys:List Nath:g xs ys = 0⊢ False xs:List Natys:List Nath:(match xs, ys with | [a, b], x => a + b + 1 | x, [b, c] => b + 1 | x, x_1 => 1) = 0⊢ False; ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Natc✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b c : Nat), ys = [b, c] → Falseh:1 = 0⊢ False ys:List Natxs✝:List Natys✝:List Nata✝:Natb✝:Nath:a✝ + b✝ + 1 = 0⊢ Falsexs:List Natxs✝:List Natys✝:List Natb✝:Natc✝:Natx✝:∀ (a b : Nat), xs = [a, b] → Falseh:b✝ + 1 = 0⊢ Falsexs:List Natys:List Natxs✝:List Natys✝:List Natx✝¹:∀ (a b : Nat), xs = [a, b] → Falsex✝:∀ (b c : Nat), ys = [b, c] → Falseh:1 = 0⊢ False All goals completed! 🐙

5.9. Extensible Tactics🔗

In the following example, we define the notation triv using the command syntax. Then, we use the command macro_rules to specify what should be done when triv is used. You can provide different expansions, and the tactic interpreter will try all of them until one succeeds:

-- Define a new tactic notation syntax "triv" : tactic macro_rules | `(tactic| triv) => `(tactic| assumption) example (h : p) : p := p:Sort ?u.598h:p⊢ p All goals completed! 🐙 -- You cannot prove the following theorem using `triv` -- example (x : α) : x = x := by -- triv -- Let's extend `triv`. The tactic interpreter -- tries all possible macro extensions for `triv` until one succeeds macro_rules | `(tactic| triv) => `(tactic| rfl) example (x : α) : x = x := α:Sort u_1x:α⊢ x = x All goals completed! 🐙 example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p α:Sort u_1p:Propx:αh:p⊢ x = xα:Sort u_1p:Propx:αh:p⊢ p All goals completed! 🐙 -- We now add a (recursive) extension macro_rules | `(tactic| triv) => `(tactic| apply And.intro <;> triv) example (x : α) (h : p) : x = x ∧ p := α:Sort u_1p:Propx:αh:p⊢ x = x ∧ p All goals completed! 🐙

5.10. Exercises

  1. Go back to the exercises in Propositions and Proofs and Quantifiers and Equality and redo as many as you can now with tactic proofs, using also rw and simp as appropriate.

  2. Use tactic combinators to obtain a one-line proof of the following:

declaration uses 'sorry'example (p q r : Prop) (hp : p) : (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) := p:Propq:Propr:Prophp:p⊢ (p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) All goals completed! 🐙