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 proof assistants are now commonly used for hardware and software verification. This chapter, we introduce the basics of using Lean as a proof assistant by focusing on the treatment of propositional logic. Chapter 13 will extend this to equational reasoning and proof by induction, but even that only scratches the surface. 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. 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