9. Using Lean as a Proof Assistant

This chapter marks three shifts in the way we are using Lean. First, up to this point we have been using Lean as a programming language, whereas here we will begin to use Lean as a proof assistant. In the theory-implementation-application trichotomy that we used to describe this course, this marks a shift from using Lean to implement logical tools to using Lean as an important application of logic, one that is used to verify hardware, software, and complex systems as well as mathematical theorems. Finally, whereas up to now our focus has been on representing logical languages in Lean, now we are using Lean as a logical language itself. This can be viewed as a shift from treating logic as an object language to treating logic as a metalanguage, a distinction we will now explain.

Imagine implementing one programming language, such as Lisp, in another programming language, like C++. In this scenario, we can characterize Lisp as being the object language, that is, the one that is being implemented, and C++ as the metalanguage, the one that is carrying out the implementation. What we did in Chapter 5 is similar: we are used one logical system, Lean, to implement another one, propositional logic. Whether we care about logical languages or programming languages (or a combination of both), it’s often the case that we use one language to implement or describe another. If we use Lean to implement a decision procedure for propositional logic, propositional logic is the object language, the target of our implementation. If we use propositional connectives (and more) to prove the correctness of that procedure in Lean, then in that case we are using propositional logic as part of the metalanguage, the thing we are using to achieve our goal.

One goal of this chapter is to clarify the sense in which Lean itself is a logical system, which is to say, its language can be used to state mathematical theorems and prove them. Using a logical foundation like Lean’s as both a programming language and a mathematical language brings a number of benefits:

• It allows us to specify the behavior of computer programs in the same language that we write them.

• It allows us to prove, rigorously, that our computer programs are correct, which is to say, that they meet their specifications.

• It allows us to enforce preconditions on our programs. For example, we can write functions whose input is required to be a positive integer, a requirement that is enforced statically, at compile time. Compiler optimizations can make use of this knowledge.

• It allows us to compute with objects in our mathematical libraries.

• It gives us ways of using computation reliably in mathematical proofs.

Although we will not discuss it in this course, Lean also serves as its own metaprogramming language, which means that we can use Lean to develop automation that can help us construct programs and proofs. In that way, Lean becomes a self-extending system, meaning that we can improve its support for programming and theorem proving using the system itself.

Lean’s logical foundation is powerful and expressive enough to carry out any mathematical argument, and the use of proof assistants in hardware and software verification is an import subject to study. In this chapter, we will present only the most basic aspects of using Lean as a proof assistant, to convey a flavor of what is possible. You can learn more about the use of Lean as a proof assistant in either Mathematics in Lean or Theorem Proving in Lean 4. You may also enjoy interactive tutorials, like the Natural Number Game, found on the Lean Game Server.

For the examples in this chapter, we use the following imports:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

Since importing a file also imports everything it depends on, these serve to make available to us a modest portion of Lean’s mathematical library, Mathlib.

9.1. Propositional logic

In Lean, we can declare variables that range over propositions and then use them to build more complicated propositions.

variable (P Q R S : Prop)

#check True
#check False
#check P ∧ Q
#check P ∨ Q
#check P → Q
#check P ↔ Q
#check ¬ P

Hovering over the symbols will give you options for typing them. Using \and, \or, \to, \iff, and \not will work. In Lean, you state a theorem with the keyword theorem.

theorem easy : P → P := by
  intro h
  apply h

What follows the keyword by is what is known as a tactic proof, that is, a list of commands that tells Lean how to construct a proof of the theorem. In the next section, we will say more about how proofs are represented in Lean and what tactics do underneath the hood. Here, instead, we will focus on how to use them. Stating a theorem creates a goal, namely, the theorem to be proved. If you put your cursor at the beginning of the line intro h, the infoview window shows the following goal:

P Q R S: Prop
⊢ P → P

If you put your cursor at the end of the line, you will see that the goal has changed to:

P Q R S: Prop
h : P
⊢ P

When the cursor is at the beginning of the line intro h, the highlighting in the infoview window helpfully shows what is about to change, and when you move the cursor to the end of the line, the highlighting shows what has just changed. The notation should remind you of a sequent in natural deduction: the second goal says that we are given propositions P, Q, R, and S together with the assumption that P holds, labelled as h, and we are to prove P. The command apply P finishes it off, leaving you with the happy message, “no goals.” The label h is arbitrary, and you can use any valid identifier instead. It’s conventional to use the letter h for hypotheses. The information before the turnstile is called the context. The right side of the sequent is also sometimes confusingly called the goal, but we will call it the conclusion of the sequent and reserve the term “goal” for the entire sequent.

You can use the example keyword to prove a theorem without naming it:

example : P → P := by
  intro h
  apply h

When an apply command finishes off the goal exactly, it is conventional to use the exact tactic instead:

example : P → P := by
  intro h
  exact h

You can also end a proof with the done tactic, which does nothing but declare that there are no more goals.

example : P → P := by
  intro h
  exact h
  done

It is often useful to put a done at the end of a proof while you are still writing it. Lean gives you an error message if the proof isn’t over, and the error message tells you the goals that remain to be proved. It can be convenient to force Lean to put the error message on the done command rather than somewhere lower down in the file. You can then delete the done when you are finished with the proof. Notice, by the way, that you can learn more about a tactic by hovering over it in VS Code.

The apply tactic can also be used to apply an implication.

example (h1 : P → Q) (h2 : P) : Q := by
  apply h1
  exact h2

In this example, applying the assumption P → Q to the goal reduces the task of proving Q to the task of proving P. To prove a conjunction, we can use the constructor tactic:

example : P → Q → P ∧ Q := by
  intro hP hQ
  constructor
  . exact hP
  . exact hQ

The command intro hP hQ is shorthand for writing intro hP followed by intro hQ. The constructor tactic tells Lean we intend to prove P ∧ Q by proving each conjunct in turn. As a result, after that line, there are two goals to prove, one for each conjunct. The first period focuses on the first goal, which is solved using hP, and the second period focuses on the second goal, which is using hQ. Lean is whitespace sensitive, and once you focus on a goal, Lean expects you to maintain the indentation until the goal is solved. You can check that the proof still works if you delete the periods. Structuring a proof in this way, however, tends to make it more readable and robust.

At this point, there is a trick that is worth mentioning. At any point in a proof, you can solve the current goal with the sorry tactic. You can prove any theorem at all using sorry. It’s cheating, and the squiggly line the editor puts underneath the name of the theorem tells you as much. But it is often a useful device when writing proofs, because it means you can temporarily close a goal to work on others, and then come back to it.

The natural way to use a conjunction h : P ∧ Q in a hypothesis is to split it to the hypotheses hP : P and hQ : Q.

example : P ∧ Q → Q ∧ P := by
  intro h
  rcases h with ⟨hP, hQ⟩
  constructor
  . exact hQ
  . exact hP

Here the angle brackets denote a conjunctive pattern for Lean to match h against, and the rcases tactic does the matching, removing h : P ∧ Q and replacing it with hP : P and hQ : Q.

The corresponding proof for disjunction is dual:

example : P ∨ Q → Q ∨ P := by
  intro h
  rcases h with hP | hQ
  . right
    exact hP
  . left
    exact hQ

Here we use a vertical bar with rcases h because the split is disjunctive, resulting in two goals: one in which we have hP : P in the context and one in which we have hQ : Q. The right tactic tells Lean that we want to prove Q ∨ P by proving P, and the left tactic tells Lean that we want to prove Q ∨ P by proving Q. Notice that in contrast to casing on a conjunction, which results in one new goal and two new hypotheses, casing on a disjunction results in two new goals, each with one new hypothesis.

Recall from Section 8.6 that in the natural deduction proof system, rules for the connectives can be categorized as either introduction rules or elimination rules. Even though we have not yet clarified the relationship between natural deduction and Lean’s internal logic, you should notice that the tactics we have given so far follow a similar pattern:

• Given a goal of the form P → Q, we can use the intro tactic to prove it.

• Given a hypothesis of the form h : P → Q, we can use the apply tactic to use it.

• Given a goal of the form P ∧ Q, we can use the constructor tactic to prove it.

• Given a hypothesis of the form h : P ∧ Q, we can use the rcases tactic to use it.

• Given a goal of the form P ∨ Q, we can use the left and right tactics to prove it.

• Given a hypothesis of the form h : P ∨ Q, we can use the rcases tactic to use it.

In Lean, negation ¬ P is defined to be P → False. For most purposes, the two expressions are interchangeable. This means that you can prove ¬ P by assuming P and deriving False, and if you have hnp : ¬ P, you an reduce the task of proving False to the task of proving P. In the next example, the intro tactic implements the first strategy, and the apply tactic implements the second.

example (h : P → Q) : ¬ Q → ¬ P := by
  intro hnQ
  intro hP
  apply hnQ
  apply h
  exact hP

After the second intro, we have h : P → Q, hnQ : ¬ Q, and hP : P in the context and False as the desired conclusion. Applying hnQ leaves us the goal of proving Q, which we do using h and hP.

There is no introduction rule for falsity; there is no canonical way to prove False! If we assume h : False, we can reach any conclusion we want, using either contradiction or rcases h. Intuitively, there is no proof of False, so if we have h : False, there are no cases to consider.

example (h : False) : P := by
  contradiction

example (h : False) : P := by
  rcases h

As a convenience, if you have h : P and hnP : ¬ P in the context, the contradiction tactic solves the goal automatically.

The principles we have used before all fall within what is known as intuitionistic logic. Many mathematical arguments require classical logic, which is embodied in the law of the excluded middle, P ∨ ¬ P. This is embodied in the by_cases tactic, which lets us split on cases. In the proof below, we have hP : P in the first case and hnP : ¬ P in the second.

example (h1 : P → Q) : ¬ P ∨ Q := by
  by_cases hP : P
  . right
    apply h1
    exact hP
  . left
    exact hP

example : ¬ ¬ P → P := by
  intro hnnP
  by_cases hP : P
  . exact hP
  . contradiction

Classical reasoning is also embodied in the by_contra tactic, which allows us to do proof by contradiction.

example : ¬ ¬ P → P := by
  intro hnnP
  by_contra hnP
  apply hnnP
  exact hnP

Applying by_contra hnP to a goal with conclusion P adds hnP : ¬ P to the context and asks us to prove False.

You can think of P ↔ Q as an abbreviation for (P → Q) ∧ (Q → P). It is not implemented exactly that way in Lean, but like a conjunction, the task of proving such a statement can be split into the forward and backward directions.

example (h1 : P ↔ Q) (h2 : P) : Q := by
  rcases h1 with ⟨hpq, _⟩
  apply hpq
  exact h2

example (h1 : P ↔ Q) : Q ↔ P := by
  rcases h1 with ⟨h2, h3⟩
  constructor
  . exact h3
  . exact h2

In the first example, the underscore omits a label for the hypothesis, since we don’t needed it. If you use a label, Lean’s built in linter will warn you that the label is unused. The hypothesis still appears in the context with an inaccessible name, and can be used by automation. If you replace the underscore with a dash (-), the rcases tactic clears it entirely from the context.

The methods in this section are complete for classical propositional logic, which is to say, any proof in classical propositional logic can be carried out using these methods. That is not to say that these methods are the most efficient; Lean offers both automation and syntax for writing proofs more compactly. As far as automation is concerned, all the proofs in this section can be carried out using the tauto tactic, which stands for “tautology.”

example (h1 : P → Q) : ¬ P ∨ Q := by
  tauto

But writing propositional proofs by hand is a good way to learn how propositional logic works in Lean, and in more complicated proofs we often need to carry out simple logical manipulations by hand.

9.2. Proof terms

Remember that, in Lean’s foundation, everything is expression. In particular, if an expression P has type Prop, then a term p of type P is interpreted as a proof of P. Lean’s proof language is therefore essentially the same as its programming language, which means that we can write proofs the same way we write programs.

def prod_swap (α β : Type) : α × β → β × α :=
  fun p => Prod.mk (Prod.snd p) (Prod.fst p)

theorem and_swap (P Q : Prop) : P ∧ Q → Q ∧ P :=
  fun h => And.intro (And.right h) (And.left h)

def sum_swap (α β : Type) : Sum α β → Sum β α :=
  fun s => match s with
    | Sum.inl a => Sum.inr a
    | Sum.inr b => Sum.inl b

theorem or_swap (P Q : Prop) : P ∨ Q → Q ∨ P :=
  fun h => match h with
    | Or.inl hp => Or.inr hp
    | Or.inr hq => Or.inl hq

Instead of using the identifier def, it is conventional to use the word theorem to name the proof of a proposition. Each keyword serves to assign an expression to an identifier; the main difference is that theorems are marked opaque, which means that they are generally not unfolded. A proof written this way is called a proof term. The tactic proofs described in the previous section are nothing more than instructions that tell the system how to construct such an expression.

The syntax for proof terms, in turn, is closely related to natural deduction. The #explode command prints proof terms in a format that is closer to the presentation of natural deduction in Section 8.6.

#explode and_swap
#explode or_swap

Don’t look too hard for an exact correspondence, because the details differ. But Lean’s foundation can be seen as a vast generalization of natural deduction, giving rise to its uniform treatment of proofs and programs. The analogy between the two is known as the Curry-Howard correspondence, and it explains the fact that the introduction and elimination rules for the connectives look a lot like the constructors and destructors for the corresponding data types. The examples above show that the introduction and elimination rules for conjunction parallel the constructors and destructors for the pair data type, and the introduction and elimination rules for disjunction parallel the constructors and destructors for the sum data type. In Lean’s foundation, the introduction and elimination rules for implication are exactly lambda abstraction and function application, respectively.

example : P → P ∧ P := fun h => And.intro h h

example (h1 : P → Q) (h2 : P) : Q := h1 h2

In Lean, ¬ P is defined to be P → False. The following proof assumes P and ¬ P, concludes ⊥, and then uses the ex falso principle to conclude Q.

example : P → ¬ P → Q := fun h1 h2 => False.elim (h2 h1)

Lean allows the use of anonymous constructors and projections with proof terms just as with data:

example : P ∧ Q → Q ∧ P :=
  fun h => ⟨h.right, h.left⟩

You can use proof terms in a tactic proof:

example : P → Q → (P ∧ Q) ∨ R := by
  intro h1 h2
  exact Or.inl (And.intro h1 h2)

In fact, under the hood, a tactic proof is essentially a program that constructs the relevant proof. Here are some more examples:

theorem and_swap' : P ∧ Q → Q ∧ P := by
  intro h
  rcases h with ⟨h1, h2⟩
  constructor
  . exact h2
  . exact h1

theorem or_swap' : P ∨ Q → Q ∨ P := by
  intro h
  rcases h with h1 |  h2
  . right; exact h1
  . left; exact h2

#print and_swap'
#explode and_swap'
#print or_swap'
#explode or_swap'

Lean’s show_term tactic will show you the proof term that a tactic block produces, and it will even given you the option of clicking to replace the tactic block by an explicit use of that term.

example (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  show_term {
  rcases h with ⟨h1, h2⟩
  constructor
  . exact h2
  . exact h1}

You can read more about Lean expressions in Theorem Proving in Lean 4. For the most part, in this course, we will focus on tactic proofs, but you should feel free to use a proof term with apply or exact when you feel like it. More importantly, you should keep in mind that at the end of the day, what you are doing is constructing something like a natural deduction proof, represented as an expression in Lean’s foundation. You can therefore think of Lean as an engine for manipulating expressions that can represent data types, statements, programs, and proofs. Tactics are pieces of automation that are designed to help us construct these expressions.

9.3. Structured proofs

Tactics allow us to work backward to prove a goal by reducing it to simpler ones. Lean also provides a means of reasoning forward from hypotheses, using the have tactic:

example (h1 : P → Q) (h2 : Q → R) (h3 : P) : R := by
  have hQ : Q := by
    apply h1
    exact h3
  apply h2
  exact hQ

Here the first line of the proof states an intermediate goal of proving Q. The result is named hQ, which we are then free to use. Using have tends to make proofs more readable because the text displays the stepping stones to the main goal. It also tends to make proofs more robust, in that errors are localized to small, compartmentalized parts of the proof. If you omit the keyword by, you can use a proof term to fill an easy have:

example (h1 : P → Q) (h2 : Q → R) (h3 : P) : R := by
  have hQ : Q := h1 h3
  exact h2 hQ

You can even write have hQ := h1 h3 in the second line of the first proof, omitting the type ascription, because Lean can figure that out. Of course, this sacrifices readability somewhat. You can generallly eliminate a have statement by inlining the result. For example, replacing hQ by h1 h3 yields the first proof below:

example (h1 : P → Q) (h2 : Q → R) (h3 : P) : R := by
  exact h2 (h1 h3)

example (h1 : P → Q) (h2 : Q → R) (h3 : P) : R := h2 (h1 h3)

The proof by exact h2 (h1 h3) is equivalent to just presenting the proof term h2 (h1 h3), as we do in the second example.

Lean also has a show tactic, which declares the goal we are about to solve.

example (h1 : P → Q) (h2 : Q → R) (h3 : P) : R := by
  have hQ : Q := h1 h3
  show R
  exact h2 hQ

example (h1 : P ∧ Q) (h2 : Q → R) : P ∧ R := by
  rcases h1 with ⟨hP, hQ⟩
  have hR : R := h2 hQ
  show P ∧ R
  exact ⟨hP, hR⟩

The show tactic mainly serves to make a proof more readable, though it does a little more work than we are letting on here. For example, if there are multiple goals left to prove, show fill focus on the first one that matches the given statement.

9.4. Equational reasoning

We are still a long way from from full-blown mathematical reasoning. In the chapters to come, we will gradually expand the formal languages we consider, and we will explore ways to automate the associated patterns of reasoning. In particular, in the next chapter, we will see that it is important to be able to reason about terms and relationships between them. For example, if x and y are variables ranging over integers and xs and ys are variables ranging over lists of integers, the expression (x + y) + 3 is a term denoting an integer and the expression x :: xs ++ [3] ++ ys is a term denoting a list of integers. The expressions x < y + 3, x = y + 3, and x ∈ xs are formulas that say that x is less than y + 3, x is equal to y + 3, and x is an element of the list xs, respectively. The symbols <, =, and ∈ denote binary relations, since they express a relationship between the terms on either side.

Mathematically, the most fundamental relation is the equality relationship. Equality satisfies two axiomatic properties: first, everything is equal to itself, and second, equal terms can be substituted for one another. In Lean, these are implemented by the tactics rfl and rw, respectively. The first is short for reflexivity, and the second is short for rewrite.

example : f (a + b) = f (a + b) := by
  rfl

example (h : b = c) : f (a + b) = f (a + c) := by
  rw [h]

In the second example, the rewrite tactic replaces b by c in the goal and then automatically applies reflexivity to finish it off.

The rw tactic takes a list of identities and rewrites with them one at a time. You can use a left arrow to indicate that the tactic should use an equation in the reverse direction:

example (h1 : a = c) (h2 : b = d) : f (a + b) = f (c + d) := by
  rw [h1, h2]

example (h1 : a = c) (h2 : d = c + b) (h3 : d = e) :
    f (a + b) = f (e) := by
  rw [h1, ←h2, h3]

Notice that even common properties like the symmetry and transitivity of equality can be reduced to the substitution property and reflexivity.

example (h : a = b) : b = a := by
  rw [h]

example (h1 : a = b) (h2 : b = c) : a = c := by
  rw [h1, h2]

You can also rewrite with general identities. In Lean, when you write a * b * c, parentheses associate to the left, so the expression is interpreted as (a * b) * c. The identities mul_assoc, mul_comm, and mul_left_comm can be used to move the parentheses around.

#check (mul_assoc : ∀ a b c, (a * b) * c = a * (b * c))
#check (mul_comm : ∀ a b, a * b = b * a)
#check (mul_left_comm : ∀ a b c, a * (b * c) = b * (a * c))

example : (c * b) * a = b * (a * c) := by
  rw [mul_assoc, mul_comm, ←mul_assoc]

Notice that your cursor after the comma in the list of the identities shows that goal at the point, so you can step through a sequence of rewrites to see what is happening.

You can specialize identities at particular arguments. For example, mul_comm c a is the identity c * a = a * c, and mul_comm c is the identity ∀ x, c * x = x * c. Notice that Lean uses the same syntax for applying a theorem to arguments as it does for applying a function to arguments. In the underlying foundation, the two are instances of the same thing.

example : (a * b) * c = b * (a * c) := by
  rw [mul_comm a b, mul_assoc b a c]

example : (a * b) * c = b * (a * c) := by
  rw [mul_comm a, mul_assoc]

example (a b c d e : ℕ) (h1 : a = b + 1)
    (h2 : d = c + a) (h3 : e = b + c) :
  d = e + 1 := by
  rw [h2, h3, h1, add_comm b c, add_assoc]

You can also use rw with the at modifier to rewrite at a particular hypothesis.

example (a b c d e : ℕ) (h1 : a = b + 1) (h2 : d = c + a) (h3 : e = b + c) : d = e + 1 := by
  rw [h1] at h2
  rw [h2, h3, ←add_assoc, add_comm c]

Sometimes, you only want to replace a single occurrence of a term. You can use the nth_rw tactic for that.

example (h : a = a * a) : b * a = b * (a * a) := by
  nth_rw 1 [h]

In this example, nth_rw 1 [h] applies the rewrite h to the first occurrence of a in the conclusion.

Mathlib has specialized tactics for proving particular types of equations. For example, norm_num can be used for concrete calculations and ring can be used to prove identities involving addition, subtraction, multiplication, integer coefficients, and natural number exponents.

example : 123 * 345 = 42435 := by
  norm_num

example : (a + b)^2 = a^2 + 2*a*b + b^2 := by
  ring

example : a^2 - b^2 = (a + b) * (a - b) := by
  ring

Rewriting with the name of a function amounts to unfolding the definition, or, if it is defined by cases, its defining clauses.

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | (n + 2) => fib (n + 1) + fib n

example : fib (n + 3) = 2 * fib (n + 1) + fib n := by
  rw [fib, fib]
  ring

Finally, Lean will let you rewrite with propositional equivalences.

#check (not_and_or : ¬ (P ∧ Q) ↔ ¬ P ∨ ¬ Q)
#check (not_not : ¬ ¬ P ↔ P)

example : ¬ (P ∧ ¬ Q) ↔ ¬ P ∨ Q := by
  rw [not_and_or, not_not]

Sometimes Lean will surprise you by not making you prove something you think you should have to. When it needs to, Lean will unfold definitions and apply computational rules to simplify an expression, and so it can often treat syntactically different expressions as being the same. In the next example, Lean unfolds the definition of addition and determines n + 0 and n are definitionally equal.

example (n : Nat) : n + 0 = n := by
  rfl

Replacing n + 0 by 0 + n does not work, however. Definitional equality is subtle and we will discuss it in detail here, but it might be helpful to know that Lean can generally unfold a recursive definition or a definition on cases when it has to. This feature of Lean is probably at play when you find that rw declares a goal solved when you thought you had more work to do.

Lean has other automation that can handle equational reasoning, most notably, a tactic called simp that simplifies expressions using a database of identities that have been marked for its use.

example : fib 8 = 21 := by
  simp [fib]

example : a + b - b = a := by
  simp

example : P ↔ P ∧ P := by
  simp

As usual, hovering over simp provides more information about how it works. In the real world, you should feel free to use automation like simp with reckless abandon. The more automation the better! That’s what this course is all about. But for the exercises we will ask you to do proofs using more elementary tactics — for example, using only the rw tactic to prove identities — so that you acquire a solid understanding of the principles of reasoning that they implement.

9.5. Induction

With only equality and the propositional connectives, our vocabulary is limited. In Lean, it is possible to describe any precise mathematical property or relationship, and, indeed, a vast number of them are already defined in Mathlib. But even with just equality and the propositional connectives, we can prove some interesting theorems, and so we will make a small start on that here.

In Chapter 2 we reviewed the principle of induction, and we have seen throughout this book that Lean allows us to define inductive data types and to define functions on those types by structural recursion. We now introduce Lean’s induction tactic. In the next example, we define the function sum_up_to n that sums the numbers up to and including n, and we use induction to prove that it is equal to n * (n + 1) / 2 for every n. (We state this in a roundabout way to avoid having to deal with division.)

def sum_up_to : Nat → Nat
  | 0 => 0
  | (n + 1) => (n + 1) + sum_up_to n

example (n : Nat) : 2 * sum_up_to n = n * (n + 1) := by
  induction n with
  | zero =>
      rw [Nat.zero_eq, sum_up_to]
  | succ n ih =>
      rw [Nat.succ_eq_add_one, sum_up_to, mul_add, ih]
      ring

As usual, hovering over induction gives you more information about its syntax and usage, including variations. Here the two cases are named zero and succ, corresponding to the two canonical ways of constructing a natural number. In the succ case we name the variable n and the inductive hypothesis ih. It is unfortunate that the two cases of the induction use Nat.zero and Nat.succ n instead of the (definitionally equal) expressions 0 and n + 1, respectively, but the equations Nat.zero_eq and Nat.succ_eq_add_one fix that. Rewriting with sum_up_to unfolds the definition, and hovering over mul_add shows that it distributes the multiplication over addition so that we can apply the inductive hypothesis. Remember that you can step through the rewrites in the infoview window by moving your cursor down the list. Here is another example of a proof by induction:

def sum_odds : Nat → Nat
  | 0 => 0
  | (n + 1) => (2 * n + 1) + sum_odds n

theorem sum_odds_eq_square (n : Nat) : sum_odds n = n^2 := by
  induction n with
  | zero =>
      rw [sum_odds, Nat.zero_eq, pow_two, zero_mul]
  | succ n ih =>
      rw [sum_odds, ih, Nat.succ_eq_add_one]
      ring

In fact, in Lean’s library, addition and multiplication on the natural numbers are defined recursively and their properties are proved using induction. In the example below, we define addition with the name add' to avoid clashing with names in the library, and we open the Nat namespace to shorten names like succ and zero_eq.

open Nat

def add' : Nat → Nat → Nat
  | m, 0 => m
  | m, (n + 1) => (add' m n) + 1

theorem zero_add' (n : Nat) : add' 0 n = n := by
  induction n with
  | zero => rw [add']
  | succ n ih => rw [add', ih]

theorem succ_add' (m n : Nat) : add' (succ m) n = succ (add' m n) := by
  induction n with
  | zero => rw [add', add']
  | succ n ih => rw [add', ih, add']

theorem add'_comm (m n : Nat) : add' m n = add' n m := by
  induction m with
  | zero =>
    rw [zero_eq, zero_add', add']
  | succ m ih =>
    rw [add', succ_add', ih]

Lean supports induction on any inductive type, not just the natural numbers. Remember that Lean’s core library defines the List data type and notation for it. In the example below, we open the namespace, declare some variables, and confirm the recursive definition of the append function. The proofs by reflexivity show that nil_append and cons_append are definitionally true, which is to say, they following by unfolding the definition of append.

open List

variable {α : Type}
variable (as bs cs : List α)
variable (a b c : α)

example : [] ++ as = as := nil_append as
example : (a :: as) ++ bs = a :: (as ++ bs) := cons_append a as bs

example : [] ++ as = as := rfl
example : (a :: as) ++ bs = a :: (as ++ bs) := rfl

The variable command does not do anything substantial. It tells Lean that when the corresponding identifiers are used in definitions and theorems that follow, they should be interpreted as arguments to those theorems and proofs, with the indicated types. The curly brackets around the declaration α : Type indicate that that argument is meant to be implicit, which is to say, users do not have to write it explicitly. Rather, Lean is expected to infer it from the context.

The library stores the theorems [] ++ as and (a :: as) ++ bs = a :: (as ++ bs) under the names nil_append and cons_append, respectively. You can see the statements by writing #check nil_append and #check cons_append. Remember that we took these to be the defining equations for the append function in Section 2.3.

Lean’s library also proves as ++ [] under the name append_nil, but to illustrate how proofs like this go, we will prove it again under the name append_nil'.

theorem append_nil' : as ++ [] = as := by
  induction as with
  | nil => rw [nil_append]
  | cons a as ih => rw [cons_append, ih]

Even though the proof is straightforward, some cleverness is needed to decide which variable to induct on. The fact that append is defined by recursion on the first argument makes as the natural choice. Similarly, we can prove the associativity of the append function.

theorem append_assoc' : as ++ bs ++ cs = as ++ (bs ++ cs) := by
  induction as with
  | nil => rw [nil_append, nil_append]
  | cons a as ih => rw [cons_append, cons_append, ih, cons_append]

Sometimes proving even simple identities can be challenging. Lean defines the list reverse function using a tail recursive auxiliary function reverseAux as bs, which in turn uses an accumulator to append the reverse of as to bs

example : reverse as = reverseAux as [] := rfl
example : reverseAux [] bs = bs := rfl
example : reverseAux (a :: as) bs = reverseAux as (a :: bs) := rfl

If you try proving reverse (as ++ bs) = reverse bs ++ reverse as, you’ll find that it isn’t easy. It turns out to be best to prove the following two identities first:

theorem reverseAux_append : reverseAux (as ++ bs) cs = reverseAux bs (reverseAux as cs) := by
  induction as generalizing cs with
  | nil => rw [nil_append, reverseAux]
  | cons a as ih => rw [cons_append, reverseAux, reverseAux, ih]

theorem reverseAux_append' : reverseAux as (bs ++ cs) = reverseAux as bs ++ cs := by
  induction as generalizing bs with
  | nil => rw [reverseAux, reverseAux]
  | cons a as ih => rw [reverseAux, reverseAux, ←cons_append, ih]

The generalizing clause in the two induction tells Lean that the inductive hypothesis should be applied to any choice of second parameter, not just the one from the previous step. Mathematically, what is going on is that we are proving by induction on as that the identity holds for every choice of the second parameter. This is needed because the recursive step of reverseAux uses a different parameter in the recursive call. You should try deleting the generalizing clause to see what goes wrong when we omit it.

With those facts in hand, we have the identity we are after:

theorem reverse_append : reverse (as ++ bs) = reverse bs ++ reverse as := by
  rw [reverse, reverseAux_append, reverse, ←reverseAux_append', nil_append,
      reverse]

As a similar exercise, we encourage you to prove that for any list as, reverse (reverse as) = as. You can do this by proving suitable lemmas about reverseAux.

Let’s consider one last example, which brings us closer to the kinds of logical operations that we have been implementing in Lean. We have often relied on the fact that when we evaluate a propositional formula relative to a truth assignment, the resulting truth value only depends on the variables that occur in the formula. We can formalize in Lean what it means to say that a variable v occurs in A in Lean as follows:

namespace PropForm

def Occurs (v : String) : PropForm → Prop
  | tr => False
  | fls => False
  | var w => v = w
  | neg A => Occurs v A
  | conj A B => Occurs v A ∨ Occurs v B
  | disj A B => Occurs v A ∨ Occurs v B
  | impl A B => Occurs v A ∨ Occurs v B
  | biImpl A B => Occurs v A ∨ Occurs v B

Here we follow Lean’s convention of using capital letters for propositions, properties, and predicates. We could just as well have defined a function vars : PropForm → Finset String that returns the finite set of variables contained in a propositional formula, in which case Occurs v A would be equivalent to v ∈ vars A.

In the past, we have also defined an evaluation function for propositional formulas relative to a partial truth assignment, an element of type PropAssignment. Here, to simplify the discussion, we will use total assignments to propositional variables, represented as functions of type String → Bool. The evaluation function for propositional formulas is then defined straightforwardly as follows.

def eval (v : String → Bool) : PropForm → Bool
  | var s => v s
  | tr => true
  | fls => false
  | neg A => !(eval v A)
  | conj A B => (eval v A) && (eval v B)
  | disj A B => (eval v A) || (eval v B)
  | impl A B => !(eval v A) || (eval v B)
  | biImpl A B => (!(eval v A) || (eval v B)) && (!(eval v B) || (eval v A))

The following theorem formalizes the statement that changing the value of a truth assignment at a variable that does not occur in a formula does not change the value of the formula. The proof is mainly a matter of unfolding definitions and checking all the cases.

variable (A B : PropForm) (τ : String → Bool) (v : String)

theorem eval_of_not_occurs (h : ¬ Occurs v A) (b : Bool) :
    A.eval (fun w => if v = w then b else τ w) = A.eval τ := by
  induction A with
  | var s =>
    rw [eval]
    rw [Occurs] at h
    rw [if_neg h, eval]
  | tr =>
    rw [eval, eval]
  | fls =>
    rw [eval, eval]
  | neg A ihA =>
    rw [eval, eval]
    rw [Occurs] at h
    rw [ihA h]
  | conj A B ihA ihB =>
    rw [Occurs, not_or] at h
    rcases h with ⟨hA, hB⟩
    rw [eval, eval, ihA hA, ihB hB]
  | disj A B ihA ihB =>
    rw [Occurs, not_or] at h
    rcases h with ⟨hA, hB⟩
    rw [eval, eval, ihA hA, ihB hB]
  | impl A B ihA ihB =>
    rw [Occurs, not_or] at h
    rcases h with ⟨hA, hB⟩
    rw [eval, eval, ihA hA, ihB hB]
  | biImpl A B ihA ihB =>
    rw [Occurs, not_or] at h
    rcases h with ⟨hA, hB⟩
    rw [eval, eval, ihA hA, ihB hB]

The theorems if_pos h and if_neg h are used to rewrite an if-then-else expression given the knowledge h that the condition is true or false, respectively. You should step through the proof and make sure you understand how it works.

Verifying proofs involving logical operations or programming constructs often looks like this, with lots of straightforwrd cases to check. Because such checking is tedious, the general practice is to verify only one or two representative cases in a pen-and-paper proof and claim that the others are “similar.” This is often a source of bugs, however, since a corner case or subtle difference in one of the cases and render the claim false. When formalizing such a theorem, it would be nice if the cases can be checked automatically. Indeed, in this case Lean’s simplifier reduces the proof to a one-liner:

example (h : ¬ Occurs v A) (b : Bool) :
    A.eval (fun w => if v = w then b else τ w) = A.eval τ := by
  induction A <;> simp [*, Occurs, eval, not_or] at * <;> simp [*] at *

Lean has even more powerful automation, like Aesop, that is designed for such purposes. Working through proofs like the one above by hand is a good way to come to terms with what we want such automation to do, and the techniques that we are describing in this course form the basis for writing such automation.

9.6. Exercises

Complete the following proofs in Lean.

import Mathlib.Data.Real.Basic

variable (P Q R S : Prop)

example : P ∧ Q ∧ (P → R) → R := by
sorry

example : (P → Q) ∧ (Q → R) → P → r := by
sorry

example (h : P → Q) (h1 : P ∧ R) : Q ∧ r := by
sorry

example (h : ¬ (P ∧ Q)) : P → ¬ Q := by
sorry

example (h : ¬ (P → Q)) : ¬ Q := by
sorry

example (h : P ∧ ¬ Q) : ¬ (P → Q) := by
sorry

example (h1 : P ∨ Q) (h2 : P → R) : r ∨ Q := by
sorry

example (h1 : P ∨ Q → R) : (P → R) ∧ (Q → R) := by
sorry

example (h1 : P → R) (h2 : Q → R) : P ∨ Q → R := by
sorry

example (h : ¬ (P ∨ Q)) : ¬ P ∧ ¬ Q := by
sorry

example (h : ¬ P ∧ ¬ Q) : ¬ (P ∨ Q) := by
sorry

-- this one requires classical logic!
example (h : ¬ (P ∧ Q)) : ¬ P ∨ ¬ Q := by
sorry

-- this one too
example (h : P → Q) : ¬ P ∨ Q := by
sorry