4.1. More Powerful Natural Numbers🔗

Until now, we have been working with our own custom natural numbers, using the Nat type that we defined in Basics.

As you might have guessed, Lean has a built-in type of natural numbers, also called Nat, which is automatically imported into .lean files by default. Its definition is essentially the same as our custom Nat, but it comes with a large library of useful theorems. Programmers and mathematicians usually apply these automatically rather than by writing out rewrite steps by hand. For example, here is a simple proof of equality using our custom Nats.

We made Lean enforce this pedagogical style using attribute [irreducible] on definitions like mul and add. This forced us to write proofs using tactics like rw rather than simplifying definitions.

This approach is useful in a textbook for understanding the structure of natural numbers and for providing early practice with writing proofs. But it is also tedious in the long term.

Instead of doing this, programmers and mathematicians use the built-in Nat and the powerful features of Lean to automatically prove properties about natural numbers and to compute with them.

The annotation : Nat tells Lean that we are using its built-in Nat type. Definitions in the built-in Nat library are not marked @[irreducible], so we can perform automatic simplification of functions on natural numbers, which is appropriate when their low-level behaviors are not the primary focus of proofs.

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!

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

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

We will write Nat.<theorem> to reference Lean's version of <theorem>; by convention, theorems about a type live in the namespace of that type.

4.2. Searching for Standard Library Theorems🔗

Because we did not write or prove theorems for built-in Nats ourselves, we may not know (or remember) all the available theorems.

Lean provides a few ways to search through the standard library to find theorems that may be useful during a particular proof. The first way is the exact? tactic. This tactic searches the standard library for a theorem that can be applied, along with the hypotheses in the context, to exactly close the current goal.

Try this:
  [apply] exact Nat.add_comm n m

If you are using the Lean extension in VS Code, the InfoView will have a blue [apply] button that shows the suggested theorem to close the goal. Alternatively, VS Code may show an inline suggestion (lightbulb) button above the exact?. You can click either of these buttons to replace the occurrence of exact? with the tactic it found to complete the proof; idiomatic Lean should not contain exact? tactics (or any other ? tactics) in the finished versions of proofs.

The exact? tactic is useful when we just need a single library theorem to get us over the finish line, but it is not so helpful when we are deep in the middle of a proof or wondering how to get started on one. Fortunately, there are other tactics that can help.

The rw? tactic searches for any theorems that you could use to rewrite (rather than complete) the current goal.

Try this:
  [apply] rw [Nat.add_comm]
  -- no goals

However, unlike exact?, just because rw? suggests a theorem to you does not automatically imply that it will be useful. In the example below, many of the theorems rw? suggests will not progress towards completing the proof; you will need to carefully look through its suggestions to see which ones seem useful.

We strongly recommend against blindly using rw? and accepting its suggestions without due consideration! You will find this to be a slow and frustrating way to write proofs. Instead, we suggest figuring out what you would like your next step to be, conceptually, and then using rw? to search for a theorem that implements it. If no such theorem exists, you may need to prove it yourself.

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.

Furthermore, sometimes we know exactly how we want to manipulate the terms of a proof, but don't want to have the tactics like Nat.add_comm and Nat.add_assoc "guess" which subterms to rewrite.

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]

Note how we can see each intermediate step of this proof when we look at it this way. Let's look at how we might prove this theorem (i.e., that n + (m + k) = m + (n + k)) in Lean.

First, a proof in the style we already know.

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

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

Whereas before, the left-hand side of each equality in the calc tactic was repeated from the right-hand side of the previous one, we can replace the left-hand side entirely with an _. Now our Lean proof looks quite a bit like the textbook one we saw earlier!

If you prefer rw to calc, that's fine! Each has particular uses, and both will be tools in your ever-growing toolbox of tactics.

4.4. Unfolding definitions using rw🔗

Here are some definitions about Nats:

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:

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 n

What happened?

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.

A natural next step is to rewrite by Nat.add_assoc so that rfl should work on the result.

This doesn't work either.

Tactic `rewrite` failed: Did not find an occurrence of the pattern
  ?n + ?m + ?k
in the target expression
  addThrice n = n + addTwice n

n✝ n:Nat⊢ addThrice n = n + addTwice n

The reason is that the expression in which we are trying to rewrite Nat.add_assoc isn't of the form n + m + k precisely; it is addThrice 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.

Since Lean does not unfold most definitions automatically, we use tactics like rw to do so selectively, in goals and hypotheses, in order to guide how a proof is carried out.

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

Aside: rw? at h also works on hypotheses:

With the ability to unfold definitions via rewriting, one may wonder why we need simplification rules like add_zero and add_succ. As mentioned when motivating these rules, they provide some engineering benefits: The rules tend to stay the same even as definitions change, which helps avoid proof breakages. Avoiding such breakages is particularly important with proofs using parts of Lean's standard library, which are often implemented in ways that are very efficient but less friendly to proofs.

4.5. Definitional Simplification with dsimp🔗

Sometimes when you unfold a definition your hypothesis or goal may become hard to understand. When that happens, it can be useful to simplify it. To apply simplifications similar to those that rfl does, but without also trying to close an equality goal, you can use the tactic dsimp only or dsimp only at h.

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

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.