3.1. Separate Compilation🔗

Before getting started on this chapter, we need to import all of our definitions from the previous chapter:

import LF.Basics

For this import to work, Lean needs to be able to find a compiled version of the previous chapter (Basics.lean). This compiled version, called Basics.olean, is analogous to the .class files compiled from .java source files and the .o files compiled from .c files.

When using Lake (Lean's build system), the file lakefile.toml specifies dependencies and build configuration. Running lake build will compile all necessary files in the correct order.

If you are using VS Code with the Lean 4 extension, compilation happens automatically in the background. When you open a file, the extension compiles its dependencies as needed.

Troubleshooting:

• If you get complaints about missing imports, make sure you have run lake build from the project root directory in a terminal, at least once.

• If you modify Basics.lean, VS Code will automatically recompile it when you save. You may need to reopen this file or wait for recompilation to finish.

• If you get errors that seem inconsistent with the source, try running lake clean followed by lake build to recompile everything from scratch.

  (If you are using the Lean 4 extension for VS Code, you can also restart the extension on the current file via the Restart File button in the InfoView. The extension should prompt you to do this if you change things upstream in the dependency tree.)

3.2. Review🔗

We reopen the namespace from the previous chapter to group this chapter's definitions and theorems with the custom natural-number development and keep their names distinct from the standard library.

Now let's review what we learned in Basics using some quiz questions and an exercise.

def or (b1 : Bool) (b2 : Bool) : Bool :=
  match b1 with
  | true => true
  | false => b2

theorem review₁ : (true || false) = true

theorem review₂ (b : Bool) : (true || b) = true

theorem review₃ (b : Bool) : (b || true) = true

theorem review₄ (n : Nat) : n + zero = n

theorem review₅ (n : Nat) : zero + n = n

3.3. Proof by Induction🔗

We will introduce proofs by induction on natural numbers, first motivating why induction is needed, and then explaining what it is and how you do it in Lean.

theorem add_zero : ∀ (n : Nat), n + zero = n := by
  intro n
  rfl

Tactic `rfl` failed: The left-hand side
  zero + n
is not definitionally equal to the right-hand side
  n

n:Nat⊢ zero + n = n

unsolved goals
succn':Nat⊢ zero + succ n' = succ n'

rewrite [double_zero]; rfl

rw [double_zero]

3.4. Proofs Within Proofs🔗

In Lean, as in informal mathematics, large proofs are often broken into sequences of theorems, with later proofs referring to earlier theorems. But sometimes a proof will involve some miscellaneous fact that is too trivial and of too little general interest to bother giving it its own top-level name. In such cases, it is convenient to simply state and prove the required fact "in place." The have tactic allows us to do this.

The have tactic introduces a local lemma into the proof. We prove it immediately, and it's available as a hypothesis for the rest of the proof.

As another example, suppose we want to prove that (n + m) + (p + q) = (m + n) + (p + q). The only difference between the two sides of the = is that the arguments m and n to the first inner + are swapped, so it seems we should be able to use the commutativity of addition (add_comm) to rewrite one into the other. However, the rw tactic is not very smart about where it applies the rewrite. There are three uses of + here, and rw [add_comm] may choose the wrong one...

unsolved goals
n m p q:Nat⊢ p + q + (n + m) = m + n + (p + q)

To use add_comm at the point where we need it, we can supply explicit arguments: rw [add_comm n m] tells Lean exactly which + to rewrite. (We can also use have to establish the specific equation we want, then rewrite with it.)

3.5. Formal vs. Informal Proof🔗

What constitutes a successful proof of a mathematical claim?

The question has challenged philosophers for millennia, but a rough and ready answer could be this: A proof of a mathematical proposition P is a text that instills in the reader the certainty that P is true. That is, a proof is an act of communication.

Acts of communication may involve different sorts of readers. On one hand, the reader can be a program like Lean, in which case the "belief" that is instilled is that P can be mechanically derived from a certain set of formal logical rules, and the proof is a recipe that guides the program in checking this fact. Such recipes are formal proofs.

Alternatively, the reader can be a human being, in which case the proof will probably be written in English or some other natural language and will thus necessarily be informal. Here, the criteria for success are less clearly specified. A "valid" proof is one that makes the reader believe P. But the same proof may be read by many different readers, some of whom may be convinced by a particular way of phrasing the argument, while others may not be. Some readers may be unfamiliar with the area and need the argument spelled out in detail. Other readers, more familiar with the area, may find that extra detail makes it harder to follow the argument; all they want is to be told the main ideas, since it is easier for them to fill in the details for themselves than to wade through a written presentation of them. Ultimately, there is no universal standard, because there is no single way of writing an informal proof that will convince every conceivable reader.

In practice, mathematicians have developed a rich set of conventions and idioms for writing about complex mathematical objects that — at least within a certain community — make communication pretty reliable. The conventions of this stylized form of communication give a reasonably clear standard for judging proofs good or bad.

Because we are using Lean in this course, we will be working heavily with formal proofs. But this doesn't mean we can completely forget about informal ones! Formal proofs are useful in many ways, but they are typically not the most efficient ways of communicating ideas between human beings.

For example, here is a proof that addition is associative (you might have written something like it yourself, recently...):

Lean is perfectly happy with this. For a human, however, it is difficult to make much sense of it. We can pass arguments to the add_succ theorem to show the structure more clearly...

... and if you're used to Lean you might be able to step through the tactics one after the other in your mind and imagine the state of the context and goal stack at each point, but, if the proof were even a little bit more complicated, this would be next to impossible.

On paper, a (somewhat pedantic) mathematician might write the proof like this:

• Theorem: For any n, m, and p,

  n + (m + p) = (n + m) + p.

Proof: By induction on p.

• First, suppose p = zero. We must show that

  n + (m + zero) = (n + m) + zero.

This follows directly from the definition of + (since x + zero = x for any x).

• Next, suppose p = p' + 1 (i.e., p = succ p'), where

  n + (m + p') = (n + m) + p'.

We must now show that

  n + (m + (p' + 1)) = (n + m) + (p' + 1).

By definition of +, both sides rewrite (via add_succ) to

  (n + (m + p')) + 1   and   ((n + m) + p') + 1

respectively, which are equal by the induction hypothesis. QED.

The overall form of the formal and informal proofs is basically similar, and of course this is no accident: Lean has been designed so that its induction tactic generates the same sub-goals, in the same order, as the bullet points that a mathematician would usually write. But there are significant differences of detail: the formal proof is much more explicit in some ways (e.g., the sequence of rewrites) and less explicit in others. In particular, the "proof state" at any given point in the Lean proof is completely implicit, whereas the informal proof reminds the reader several times where things stand.

3.6. Aside: Using Code Actions to Generate Match Skeletons🔗

Lean's language server can suggest code actions, which are small editor commands that modify the source code.

In VS Code, a lightbulb icon appears on the left when a code action is available at your cursor.

You can click the icon or open the code action menu with Ctrl + . on Windows/Linux or Command + . on macOS. For more information, see the Lean 4 VSCode extension manual.

For example, code actions can generate the explicit branches needed for pattern matching. This can be especially useful when working with match expressions or with tactics such as cases and induction, which we saw earlier in the book.

Let's look at a code action for induction. Suppose we start with the following incomplete proof:

Put your cursor on induction n and open the code action menu.

You should see "Generate an explicit pattern match for 'induction'." in the list. If you choose this action, Lean adds an explicit branch for each constructor:

This gives us the basic structure of the proof without requiring us to write each branch by hand. We can then focus on proving each case.

One possible proof is the following.

The same trick also works for match expressions. For example, suppose we start with

Lean can generate the missing branches:

Now you just have to replace the holes _ with your definition. You can use code actions freely to fill out induction, case, and match branches while working with this book.

One note: Sometimes the variables the code action chooses are not ideal, so you might want to change them.

For example, here is what we get from the code action for add_comm

Notice that the action chose n for the succ case, even though we are inducting on m. Manually updating this variable to either m or m' will make your proof easier to read.

3.7. More Exercises🔗

By default, rewrite and rw rewrite left to right, i.e., they transform the goal (or a hypothesis) from the form on the left side of the equality to the right side. To rewrite from right to left, use rewrite [← h] or rw [← h], where ← is entered as \l or \<-.