Proof Structure
Proofs in Lean have the same logical structure as paper proofs! In paper proofs, this logical structure is largely implicit: certain words on the page indicate the logical manipulations that are occurring, but it is rare to see the underlying logical structure of the proof explicitly depicted. In Lean, however, this logical structure is directly displayed in the Lean Infoview; this allows you to see the precise form of what you're attempting to prove, what you already know to be true, and what types of reasoning steps you're able to take next.
Hypotheses and Goals
All proofs in Lean (and in mathematics) occur in the context of certain assumptions (which we'll call hypotheses) and attempt to show certain goals. Hypotheses are propositions that are either known to be true or taken to be true for the purposes of the proof (for instance, I might want to prove that some proposition holds provided some hypothesis also does). Goals are the propositions we are trying to prove: they are the things that we want to show to be true provided that all of our hypotheses are.
In other words, hypotheses are things we know, and goals are things we want.
Let's consider a proposition about integers:
Proposition. Let n be an integer. If n is divisible by 6, then n is divisible by 2 and n is divisible by 3.
Here, we fix an integer n in advance: in other words, we are assuming that n is an integer. Our goal is the proposition "If n is divisible by 6, then n is divisible by 2 and n is divisible by 3.". We can represent this diagrammatically as follows:
n is an integer
⊢ If n is divisible by 6, then n is divisible by 2 and n is divisible by 3
We write our hypotheses in a list above the turnstile (⊢), then write our goal on the final line next to the turnstile. We refer to the collection of our hypotheses as our context, and the collection of our hypotheses and goals together as our proof state.
In the Lean Infoview, your proof state is depicted similarly, with hypotheses displayed in a list above the turnstile and the goal displayed to the right of the turnstile. There are a few key differences to be aware of, however:
- In Lean, hypotheses have names. For instance, the hypothesis a = b might be called hab.
- Hypotheses of the form "X is a Y" aren't treated as hypotheses; instead, X is treated in your context as a piece of data (specifically, one that is a Y) that you can refer to . For instance, rather than have a hypothesis hn that says "n is an integer," you'll just see "n : ℤ" in your context, indicating that n is an integer variable that you can refer to.
- Since, as we noted on the main page, Lean uses a formal language to represent mathematics rather than English, your hypotheses and goals will be displayed using symbols of that language rather than (as we have used here) English prose.
Over the course of a proof, we apply reasoning steps that update our proof state by generating new hypotheses, modifying existing hypotheses, modifying our goal, generating new goals, or directly proving (sometimes known as "discharging") a goal. Our proof is complete when there are no more goals left to prove. Of course, the reasoning steps we take in our proof need to be valid: they need to correspond to forms of logical reasoning that are actually correct. We'll shortly discuss how we precisely specify which reasoning steps are valid, but for the moment, we'll leave this notion to intuition.
Let's look at how our proof state changes over the course of a proof of the proposition above.
A Sample Paper Proof
To motivate and understand the way Lean depicts proof structure, we'll examine a traditional paper proof. The example we provide may seem verbose to the point of tedium, but we'll see that it demonstrates several important proof concepts.
Before beginning, we need to define divisibility. We'll cover this concept toward the middle of the semester, but if you're reading this page prior to that lecture, here's a working definition1:
Definition. Let a and b be integers. We say that b is divisible by a if there exists some integer c such that b = ac.
With that definition out of the way, let's look at the proof:
Proposition. Let n be an integer. If n is divisible by 6, then n is divisible by 2 and n is divisible by 3.
Proof. Suppose n is divisible by 6. By the definition of divisibility, this means that there exists some integer, which we'll call k, such that n = 6k. Note that since 6 = 2 · 3, we can equivalently write this as n = (2 · 3) · k.
We need to show that n is divisible by 2 and by 3. We show each in turn, starting with the former. By the definition of divisibility, we want to find some integer c such that n = 2c. Since we have n = (2 · 3) · k and multiplication is associative, we equivalently have n = 2 · (3 · k). And now we see that c = 3 · k is an integer such that n = 2c, which is what we sought.
Finally, we show that n is divisible by 3, i.e., that there is some integer d such that n = 3d. From our knowledge that n = (2 · 3) · k, it follows by the commutativity of multiplication that n = (3 · 2) · k. Then, by the associativity of multiplication, we have n = 3 · (2 · k). So taking d = 2 · k gives n = 3d.
Thus, we've shown that n is divisible by 2 and by 3, as desired.
Hopefully you find this proof convincing! Now, let's break down exactly how it proves the proposition and how we can represent the steps it takes using the representations you'll find in Lean.
Analyzing a Paper Proof
As a reminder, our initial proof state is:
n is an integer
⊢ If n is divisible by 6, then n is divisible by 2 and n is divisible by 3
The first line of our proof is:
Suppose n is divisible by 6.
Since our goal is of the form "if…then…," we take the portion of the goal after the "if" and add it to our list of hypotheses (our context). This corresponds to how we prove propositions of this form: "if P then Q" should be true just in case Q holds in the event that P does; so, to prove a proposition of this form, we're only interested in a "world" where P is true, so we get to add that to our list of hypotheses. Our new proof state looks like this:
n is an integer
n is divisible by 6
⊢ n is divisible by 2 and n is divisible by 3
Next in our proof is the line
By the definition of divisibility, this means that there exists some integer, which we'll call k, such that n = 6k.
Here, we're "extracting" from the hypothesis "n is divisible by 6" the information contained in the definition of "is divisible by." In particular, we "extract" (i.e., give a name to) the integer k that multiplies by 6 to yield n, and we add a hypothesis saying that this property holds of k. Our updated context looks as follows:
n is an integer
k is an integer
n = 6k
⊢ n is divisible by 2 and n is divisible by 3
The next line in our proof is the following:
Note that since 6 = 2 · 3, we can equivalently write this as n = (2 · 3) · k.
What will our proof state look like after this line of the proof?
Solution
We update our proof state just as the line of our proof suggests—in our third hypothesis, we change 6 to 2 · 3:
n is an integer
k is an integer
n = (2 · 3) · k
⊢ n is divisible by 2 and n is divisible by 3
The next line of our proof is:
We need to show that n is divisible by 2 and by 3. We show each in turn, starting with the former.
The first sentence here doesn't affect our proof state. Instead, it reminds our reader (who doesn't have the benefit of a live proof state to look at throughout all of this verbiage!) what we need to prove (i.e., what our goal is). This is good practice in an informal proof!
The first clause of the second sentence ("We show each in turn") implicitly splits our goal into two goals: one to show divisibility by 2, and one to show divisibility by 3. This reasoning step corresponds to the fact that, in order to prove a proposition of the form "P and Q" (a single goal), we need to show P (one goal) and show Q (another goal).
So after the first clause of the second sentence, we have two goals, as shown in the proof state below. Note a key fact about proof states here: when we generate a new goal in some proof state, the new goal has its own, independent context. Anything we do to the hypotheses of one goal has no bearing on the hypotheses of other goals. (This is why we wanted to rewrite 6 as 2 · 3 before splitting, avoiding the need to do the same rewrite once for each sub-goal.) It turns out that this property is critical for ensuring that our proofs are logically valid, though the reason why won't be evident in this proof. (If you're familiar with "proof by cases," think about why this would be an important property!)
n is an integer
k is an integer
n = (2 · 3) · k
⊢ n is divisible by 2n is an integer
k is an integer
n = (2 · 3) · k
⊢ n is divisible by 3
The second clause of our second sentence ("starting with the former") "focuses" the first goal. Since we can only work on one goal at a time, we want to explicitly indicate which goal we're going to try to prove next. We'll depict this by collapsing the second goal into the text "+ 1 goal" in our diagram (this diverges slightly from Lean's representation):
n is an integer
k is an integer
n = (2 · 3) · k
⊢ n is divisible by 2
+ 1 goal
The next line of our proof is:
By the definition of divisibility, we want to find some integer c such that n = 2c.
Here, we're once again "unpacking" the definition of divisibility, but this time the thing that's being rewritten is our goal rather than a hypothesis. So our proof state is as follows:
n is an integer
k is an integer
n = (2 · 3) · k
⊢ There exists some integer c such that n = 2c
+ 1 goal
The next line of our proof is:
Since we have n = (2 · 3) · k and multiplication is associative, we equivalently have n = 2 · (3 · k).
This is modifying our third hypothesis: we're using the associativity of multiplication to "rewrite" (2 · 3) · k as 2 · (3 · k). Accordingly, our proof state is now as follows:
n is an integer
k is an integer
n = 2 · (3 · k)
⊢ There exists some integer c such that n = 2c
+ 1 goal
The proof of this first goal ends with the following sentence:
And now we see that c = 3 · k is an integer such that n = 2c, which is what we sought.
To prove a goal of the form "There exists X with property P", we need to (a) identify some candidate value for X and (b) show that property P does in fact hold of it. Here, our X is "an integer c" and our P is "n = 2c."
As the line of our proof above indicates, steps (a) and (b) are often consolidated in a paper proof: we identify 3 · k as our candidate value and then implicitly appeal to our third hypothesis to indicate that the desired property does hold of 3 · k. However, we'll write out the two steps as separate proof states to be fully explicit. After we identify 3 · k as our candidate value, our proof state is as follows (notice that since we've taken c = 3 · k, we just write 3 · k in our goal):
n is an integer
k is an integer
n = 2 · (3 · k)
⊢ n = 2 · (3 · k)
+ 1 goal
And then part (b) simply involves identifying that our goal matches something we already know (i.e., a hypothesis in our context). Notice that this step directly discharged our goal in this case: after identifying our candidate value and showing that the desired property holds, there is nothing left to prove in this case! We can represent our proof state as follows (remember that we look at our proof state one goal at a time, so when we say "nothing left to prove," we mean "nothing left to prove for this particular goal"):
Nothing left to prove.
+ 1 goal
The rest of our paper proof deals with the remaining goal.
Write out the proof states in the penultimate paragraph of the paper proof.
Solution
Finally, we show that n is divisible by 3,
n is an integer
k is an integer
n = (2 · 3) · k
⊢ n is divisible by 3
i.e., that there is some integer d such that n = 3d.
n is an integer
k is an integer
n = (2 · 3) · k
⊢ There exists an integer d such that n = 3d
From our knowledge that n = (2 · 3) · k, it follows by the commutativity of multiplication that n = (3 · 2) · k.
n is an integer
k is an integer
n = (3 · 2) · k
⊢ There exists an integer d such that n = 3d
Then, by the associativity of multiplication, we have n = 3 · (2 · k).
n is an integer
k is an integer
n = 3 · (2 · k)
⊢ There exists an integer d such that n = 3d
So taking d = 2 · k
n is an integer
k is an integer
n = 3 · (2 · k)
⊢ n = 3 · (2 · k)
gives n = 3d.
Nothing left to prove.
Finally, we conclude our proof with the sentence
Thus, we've shown that n is divisible by 2 and by 3, as desired.
to remind our reader what it was we set out to prove in the first place. This is again good practice for an informal proof; of course, from a logical perspective, we've already discharged all of our goals by this point!
Footnotes
-
When we discuss this in class, we'll prefer to use the active voice and say "a divides b," but the definition is the same. ↩