Logical Foundations

4. UsingLean: Using the Full Power of a Proof Assistant🔗

In this chapter, we will learn to write more idiomatic Lean using its more powerful tools.

4.1. More Powerful Natural Numbers🔗

Whereas we performed manual rewrite steps on our custom Nats ...

section OldNats open NatPlayground.Nat example : (two * two : NatPlayground.Nat) = four := n:Nat⊢ two * two = four n:Nat⊢ succ (succ zero) * succ (succ zero) = four n:Nat⊢ zero + succ (succ zero) + succ (succ zero) = four n:Nat⊢ succ (succ (zero + succ (succ zero))) = four n:Nat⊢ succ (succ (succ (succ zero))) = four All goals completed! 🐙

... we can simplify Lean's built-in Nats automatically.

end OldNats -- Now, we are using Lean's built-in natural numbers. example : (2 * 2 : Nat) = 4 := n:Nat⊢ 2 * 2 = 4 All goals completed! 🐙

Doing so is very helpful for large numbers — we would not want to write out the hundreds or thousands of rewrite steps needed for proving examples like the following!

example : (2 * 3 + 4 * 5 : Nat) * 6 = 156 := n:Nat⊢ (2 * 3 + 4 * 5) * 6 = 156 All goals completed! 🐙

Of course, rfl still can't close goals where the values of the terms are unknown.

example (n m : Nat) (h : n = m) : n = m := n✝:Natn:Natm:Nath:n = m⊢ n = m -- `rfl` will not work here! -- First rewrite the goal with `h`; then the two sides are identical. All goals completed! 🐙

From now on we will use the built-in Nat type.

4.2. Searching for Standard Library Theorems🔗

Use the exact? tactic to search for relevant theorems in the standard library.

example (n m : Nat) : n + m = m + n := n✝:Natn:Natm:Nat⊢ n + m = m + n Try this: [apply] exact Nat.add_comm n mAll goals completed! 🐙

You can also use rw? to look for theorems to rewrite by.

example (n m : Nat) : n + m = m + n := n✝:Natn:Natm:Nat⊢ n + m = m + n Try this: [apply] rw [Nat.add_comm] -- no goalsAll goals completed! 🐙

Just because rw? suggests a theorem does not mean that it will be useful; choose carefully from its suggestions (if at all).

example (n m k : Nat) : (n + m) + k = m + (n + k) := unsolved goals n✝ n m k:Nat⊢ n + k + m = m + (n + k)n✝:Natn:Natm:Natk:Nat⊢ n + m + k = m + (n + k) -- lots of suggestions to look through here! Try this: [apply] rw [Nat.add_right_comm] -- n + k + m = m + (n + k)Try this: [apply] rw [Nat.add_assoc] -- n + (m + k) = m + (n + k)Try this: [apply] rw [Nat.add_left_comm] -- n + m + k = n + (m + k)Try this: [apply] rw [Nat.add_comm] -- k + (n + m) = m + (n + k)Try this: [apply] rw [← Nat.add_assoc] -- n + m + k = m + n + kTry this: [apply] rw [Nat.eq_iff_testBit_eq] -- ∀ (i : Nat), (n + m + k).testBit i = (m + (n + k)).testBit ifound an applicable rewrite lemma, but the corresponding tactic failed: (expose_names; rw [propext (Nat.ext_div_mod_iff n_1 (n + m + k) (m + (n + k)))]) -- (n + m + k) / n_1 = (m + (n + k)) / n_1 ∧ (n + m + k) % n_1 = (m + (n + k)) % n_1 It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.Try this: [apply] rw [Nat.le_antisymm_iff] -- n + m + k ≤ m + (n + k) ∧ m + (n + k) ≤ n + m + kTry this: [apply] rw [← Std.PRange.Nat.succMany_eq] -- Std.PRange.succMany k (n + m) = m + (n + k)found an applicable rewrite lemma, but the corresponding tactic failed: (expose_names; rw [← BitVec.cpopNatRec_allOnes Nat.le.refl]) -- (BitVec.allOnes k).cpopNatRec k (n + m) = m + (n + k) It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.found an applicable rewrite lemma, but the corresponding tactic failed: (expose_names; rw [← Nat.add_sub_sub_cancel Nat.le.refl]) -- k + (n + m) - (k - k) = m + (n + k) It may be possible to correct this proof by adding type annotations, explicitly specifying implicit arguments, or eliminating unnecessary function abstractions.Try this: [apply] rw [← Nat.add_left_max_self] -- max (n + m + k) k = m + (n + k)Try this: [apply] rw [← Nat.add_right_max_self] -- max (n + m + k) (n + m) = m + (n + k)Try this: [apply] rw [← Nat.succ_add_sub_one] -- (n + m).succ + k - 1 = m + (n + k)Try this: [apply] rw [← Nat.max_add_left_self] -- max k (n + m + k) = m + (n + k)Try this: [apply] rw [← Nat.max_add_right_self] -- max (n + m) (n + m + k) = m + (n + k)Try this: [apply] rw [← Nat.add_succ_sub_one] -- n + m + k.succ - 1 = m + (n + k)Try this: [apply] rw [← Nat.add_eq] -- (n + m).add k = m + (n + k)Try this: [apply] rw [← Rat.ofNat_eq_ofNat] -- OfNat.ofNat (n + m + k) = OfNat.ofNat (m + (n + k))Try this: [apply] rw [← Nat.compare_eq_eq] -- compare (n + m + k) (m + (n + k)) = Ordering.eqn✝:Natn:Natm:Natk:Nat⊢ n + k + m = m + (n + k)

4.3. Structuring Proofs with calc🔗

In Lean proofs, long rw chains are useful, but they are sometimes hard to read because the intermediate goals are invisible.

The calc tactic writes down the intermediate goals of a proof, and allows us to specify exactly which rewrite rules to apply at each step. It is designed to mimic the style of proofs in mathematics textbooks, which will often look something like this:

n + (m + k)
= (n + m) + k        ...   [by associativity of addition]
= (m + n) + k        ...   [by commutativity of addition]
= m + (n + k)        ...   [by associativity of addition]
example (n m k : Nat) : n + (m + k) = m + (n + k) := n✝:Natn:Natm:Natk:Nat⊢ n + (m + k) = m + (n + k) All goals completed! 🐙

Now, the same theorem written with calc. Note how each intermediate goal is visible in the source.

example (n m k : Nat) : n + (m + k) = m + (n + k) := n✝:Natn:Natm:Natk:Nat⊢ n + (m + k) = m + (n + k) calc n + (m + k) /- one side of the goal is the argument to `calc`... ... and each subsequent line is a transformation, with a tactic. -/ n + (m + k) = (n + m) + k := n✝:Natn:Natm:Natk:Nat⊢ n + (m + k) = n + m + k All goals completed! 🐙 (n + m) + k = (m + n) + k := n✝:Natn:Natm:Natk:Nat⊢ n + m + k = m + n + k All goals completed! 🐙 /- once a line matches the other side of the equality in the main goal (in this case `m + (n + k)`), the calc tactic succeeds. -/ (m + n) + k = m + (n + k) := n✝:Natn:Natm:Natk:Nat⊢ m + n + k = m + (n + k) All goals completed! 🐙

We can also write the proof like this to be a bit more concise:

example (n m k : Nat) : n + (m + k) = m + (n + k) := n✝:Natn:Natm:Natk:Nat⊢ n + (m + k) = m + (n + k) calc n + (m + k) _ = (n + m) + k := n✝:Natn:Natm:Natk:Nat⊢ n + (m + k) = n + m + k All goals completed! 🐙 _ = (m + n) + k := n✝:Natn:Natm:Natk:Nat⊢ n + m + k = m + n + k All goals completed! 🐙 _ = m + (n + k) := n✝:Natn:Natm:Natk:Nat⊢ m + n + k = m + (n + k) All goals completed! 🐙
Note to developers (Niklas Halonen @xhalo32)

How to grade that succ_mul_succ' uses calc without cheating?

4.4. Unfolding definitions using rw🔗

Here are some definitions about Nats:

def addTwice (n : Nat) : Nat := n + n def addThrice (n : Nat) : Nat := n + n + n

Suppose we wish to prove that addThrice n is equal to adding n to addTwice n. We might hope to proceed by rfl, but this doesn't work:

example (n : Nat) : (addThrice n) = n + (addTwice n) := n✝:Natn:Nat⊢ addThrice n = n + addTwice n Tactic `rfl` failed: The left-hand side addThrice n is not definitionally equal to the right-hand side n + addTwice n n✝ n:Nat⊢ addThrice n = n + addTwice nn✝:Natn:Nat⊢ addThrice n = n + addTwice n

Consulting our definitions, what we are trying to prove amounts to the following equation:

(n + n) + n = n + (n + n)

These two things are not definitionally equal, so we cannot use rfl alone.

example (n : Nat) : addThrice n = n + addTwice n := n✝:Natn:Nat⊢ addThrice n = n + addTwice n n✝:Natn:Nat⊢ addThrice n = n + addTwice n

We need to unfold the underlying definitions of addThrice and addTwice so that rw, which only operates on syntax, can see the addition. We can do this using the rw tactic.

example (n : Nat) : addThrice n = n + addTwice n := n✝:Natn:Nat⊢ addThrice n = n + addTwice n -- `rw [addThrice]` unfolds `addThrice`, replacing it with its definition n✝:Natn:Nat⊢ n + n + n = n + addTwice n -- this likewise unfolds `addTwice` n✝:Natn:Nat⊢ n + n + n = n + (n + n) -- Now, proving our goal only requires associativity of additions All goals completed! 🐙

Rewriting can also be used in places where rfl can't, like hypotheses.

def square (n : Nat) : Nat := n * n example (n : Nat) (h : square n = 16) : n * n = 16 := n✝:Natn:Nath:square n = 16⊢ n * n = 16 n✝:Natn:Nath:n * n = 16⊢ n * n = 16 All goals completed! 🐙

Aside: rw? at h also works on hypotheses:

declaration uses `sorry`example (n m : Nat) (h : 2 * n = m * 2) : n + n = m + m := n✝:Natn:Natm:Nath:2 * n = m * 2⊢ n + n = m + m -- use rw? to construct the proof All goals completed! 🐙

Unfolding should not be overused; simplification rules are (still) useful proof engineering.

4.5. Definitional Simplification with dsimp🔗

dsimp only can perform basic simplification:

example : (fun x => x + 0) n = n := n:Nat⊢ (fun x => x + 0) n = n n:Nat⊢ n + 0 = n -- applies the function to its argument All goals completed! 🐙

If we did not simplify here before attempting to rewrite, we would get an error:

example : (fun x => x + 0) n = n := n:Nat⊢ (fun x => x + 0) n = n n:Nat⊢ (fun x => x + 0) n = n 
Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?n + 0
in the target expression
  (fun x => x + 0) n = n

n:Nat⊢ (fun x => x + 0) n = n

4.6. A First Automation Tactic: repeat🔗

When rw unfolds a definition, it does so one instance at time. Thus each occurrence of a definition needs its own rewrite.

example (n m k : Nat) (h : square n + square m + square k = 0) : n * n + m * m + k * k = 0 := n✝:Natn:Natm:Natk:Nath:square n + square m + square k = 0⊢ n * n + m * m + k * k = 0 n✝:Natn:Natm:Natk:Nath:n * n + m * m + k * k = 0⊢ n * n + m * m + k * k = 0 All goals completed! 🐙

Use repeat to repeat a tactic multiple times.

example (n m k : Nat) (h : square n + square m + square k = 0) : n * n + m * m + k * k = 0 := n✝:Natn:Natm:Natk:Nath:square n + square m + square k = 0⊢ n * n + m * m + k * k = 0 repeat n✝:Natn:Natm:Natk:Nath:n * n + m * m + k * k = 0⊢ n * n + m * m + k * k = 0 All goals completed! 🐙

There is much more to say about automation, covered in the Automation chapter.

4.7. Redefining Functions and Lemmas over Nats🔗

Let's redefine some functions on Lean's Nats and prove some theorems about them.

def Nat.even (n : Nat) := match n with | 0 => true | 1 => false | n + 2 => even n def Nat.odd (n : Nat) := !(even n) theorem Nat.odd_def (n : Nat) : n.odd = !(n.even) := rfl def Nat.minusTwo (n : Nat) : Nat := match n with | 0 => 0 | 1 => 0 | n' + 2 => n' def Nat.double (n : Nat) : Nat := match n with | 0 => 0 | n' + 1 => double n' + 2

Defining functions in the Nat namespace changes how they print:

theorem Nat.even_add_three (n : Nat) : even (n + 3) = even (n + 1) := n:Nat⊢ (n + 3).even = (n + 1).even All goals completed! 🐙

This printing style is called field notation and can be enabled or disabled with the pp.fieldNotation option.

set_option pp.fieldNotation false example (n : Nat) : Nat.double (n + 0) = Nat.double n := n✝:Natn:Nat⊢ Nat.double (n + 0) = Nat.double n All goals completed! 🐙 set_option pp.fieldNotation true example (n : Nat) : Nat.double (n + 0) = Nat.double n := n✝:Natn:Nat⊢ (n + 0).double = n.double All goals completed! 🐙

We reprove here for Lean's Nat some theorems about Nat.even and Nat.double, which we had previously proven for our custom NatPlayground.Nat.

theorem Nat.even_zero : even 0 = true := ⊢ even 0 = true All goals completed! 🐙 theorem Nat.double_zero : double 0 = 0 := ⊢ double 0 = 0 All goals completed! 🐙 theorem Nat.double_succ (n : Nat) : (n + 1).double = n.double + 2 := n:Nat⊢ (n + 1).double = n.double + 2 All goals completed! 🐙
Source revision: 9e5dba0, committed 2026-09-25 03:12 UTC