2. Proofs with structure
The proofs by calculation of Chapter 1 were all, from a certain point of view, one-step proofs. In this chapter we gradually introduce the ingredients for multi-step proofs. These include establishing “intermediate” facts which get referred back to later, invoking named lemmas previously proved by yourself or other people, and taking apart complicated mathematical statements which have been built up from simpler ones using the logical symbols \(\lor\), \(\land\) and \(\exists\).
This chapter also introduces the key interactivity feature of the Lean language: the live-updating infoview keeping track of your current hypotheses and goals.
The work of this chapter continues (after a break) in Chapter 4.
2.1. Intermediate steps
2.1.1. Example
Every proof we’ve seen so far has been a single calculation. More typically, though, a proof will have a more complex structure, with facts established at an early stage which are not used immediately, but instead brought in later.
For example, here’s the algebra problem from Example 1.3.3.
Problem
Let \(a\) and \(b\) be real numbers and suppose that \(a-5b=4\) and \(b+2=3\). Show that \(a=9\).
We previously solved it by a single long calculation,
But another way to express the solution – maybe more natural, and closer to how you might have learned to solve it in high school – is to first solve for \(b\), and then substitute that in to help solve for \(a\).
Solution
Since \(b+2=3\), we have \(b=1\). Therefore
This is the first time we have seen a proof with words. The sentence
Since \(b+2=3\), we have \(b=1\).
is a use of the reasoning discussed in Section 1.5: The fact \(b=1\) is deduced from the hypothesis \(b+2=3\) by mentally subtracting 2 from both sides, and this is considered sufficiently obvious that we don’t explain the reasoning apart from indicating which of the hypotheses is being invoked.
We have now added one more fact, \(b=1\), to our list of known facts in this problem, and we carry out a calculational proof in which this fact is used (it is substituted, together with \(a-5b=4\), at the step \((a - 5b) + 5b = 4 + 5 \cdot 1\)). The word “Therefore” (synonyms: “Thus”, “So”) introduces this calculational proof; its meaning is that the fact just proved will be used in the reasoning which follows.
Here is how this argument looks in Lean. We state \(b=1\) with the keyword have hb. This is
immediately followed by the reasoning to justify this fact: adding/subtracting something from the
hypothesis \(b+2=3\), which in this problem is named h2. Then we give a calculational
proof as usual, in which the fact \(b=1\) (under the name hb) gets used at some point.
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 := by
have hb : b = 1 := by addarith [h2]
calc
a = a - 5 * b + 5 * b := by ring
_ = 4 + 5 * 1 := by rw [h1, hb]
_ = 9 := by ring
It’s not so hard to understand this proof step by step by reading the Lean code. But Lean actually provides a powerful tool to help us understand multi-step proofs: the Lean Infoview window, which we will now use for the first time. Let’s walk through what the infoview can tell us as we work through this problem.
Put your cursor at the start of the line
have hb : b = 1
and look at the Lean Infoview window. We see this:
a b : ℝ h1 : a - 5 * b = 4 h2 : b + 2 = 3 ⊢ a = 9
This is simply a vertically-displayed version of the problem we started with:
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 :=
It lists all the variables and hypotheses given to us in the problem, and, next to the symbol
⊢, it displays our goal: to showa = 9.Next, move your cursor to the start of the lines
calc a = (a - 5 * b) + 5 * b := by ring
The newly-proved fact
hb, thatb = 1, has been added to the list of hypotheses in the infoview.a b : ℝ h1 : a - 5 * b = 4 h2 : b + 2 = 3 hb : b = 1 ⊢ a = 9
Finally, move your cursor to the start of the line below the last line of code,
_ = 9 := by ring
The infoview now displays no tasks for us. Instead it displays the message
No goals
which serves as a visual confirmation that the
calcblock solved the goal, thus completing the problem.
2.1.2. Example
Here’s another example of reasoning in which we establish an intermediate statement before the main proof.
Problem
Let \(m\) and \(n\) be integers, and suppose that \(m+3\le 2n-1\) and \(n\le 5\). Show that \(m\le 6\).
Solution
We have that
so \(m \le 6\).
Here, the intermediate step is the fact \(m+3\le 9\). This can be read off by looking at the calculational proof following the text
We have that
The top left expression in the calculation is \(m+3\), the bottom right expression is \(9\), and the sequence of relations \(\le\), \(\le\), \(=\) at the steps in between together establish the relation \(\le\) between \(m+3\) and \(9\).
We discussed in Example 2.1.1 the meaning of “therefore”/”thus”/”so”. Here the text
so \(m \le 6\).
tells us that the fact just proved (\(m+3\le 9\)) implies that \(m \le 6\), by a proof which is too straightforward to require further details; in this case it’s another example of the add/subtract-from-both-sides reasoning discussed in Section 1.5.
Here is the same proof in Lean. A calculation block which is being used to establish an
intermediate step is introduced and named by have:
example {m n : ℤ} (h1 : m + 3 ≤ 2 * n - 1) (h2 : n ≤ 5) : m ≤ 6 := by
have h3 :=
calc
m + 3 ≤ 2 * n - 1 := by rel [h1]
_ ≤ 2 * 5 - 1 := by rel [h2]
_ = 9 := by numbers
addarith [h3]
Notice that, right at the beginning of the final line
addarith [h3]
the goal state (as displayed in the infoview) is
m n : ℤ
h1 : m + 3 ≤ 2 * n - 1
h2 : n ≤ 5
h3 : m + 3 ≤ 9
⊢ m ≤ 6
The fact \(m + 3 ≤ 9\), which was established by the calc block and given the name h3, is
now available as an additional fact to use in future steps, and indeed it is used in the next step
(addarith [h3]).
2.1.3. Example
Let’s redo another example, this time Example 1.4.2. The problem was:
Problem
Let \(r\) and \(s\) be rational numbers, and suppose that \(s+3\geq r\) and \(s+r \leq 3\). Show that \(r\leq 3\).
We did it before by a single, clever, calculation, but the following solution, though longer, might be easier to come up with.
Solution
From \(s + 3 \geq r\) we have \(r \leq 3 + s\), and from \(s + r \leq 3\) we have \(r \leq 3 - s\). Therefore
There are two intermediate steps in this problem: proving that \(r \leq 3 + s\) and that \(r \leq 3 - s\).
Exercise: Here is a Lean setup for this problem, with the stated intermediate intermediate steps (not yet justified), and the outline of the stated calculational proof as the final step. Fill in all the sorries. Also, try to predict what the infoview will display at each position in the proof, and then compare your prediction with reality.
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 := by
have h3 : r ≤ 3 + s := by sorry -- justify with one tactic
have h4 : r ≤ 3 - s := by sorry -- justify with one tactic
calc
r = (r + r) / 2 := by sorry -- justify with one tactic
_ ≤ (3 - s + (3 + s)) / 2 := by sorry -- justify with one tactic
_ = 3 := by sorry -- justify with one tactic
2.1.4. Example
The next problem features a new form of reasoning.
Problem
Let \(t\) be a real number, and suppose that \(t^2=3t\) and \(t \geq 1\). Show that in fact \(t\geq 2\).
Solution
We have that
so \(t=3\). Thus \(t\geq 2\).
The first step of this proof is a calculation establishing the intermediate statement \(t\cdot t=3t\). Then, with the phrase
so \(t=3\)
we establish another intermediate statement, \(t=3\), by cancelling \(t\) from the left and right sides of \(t\cdot t=3t\). Finally, we deduce the goal, \(t=3\).
In Lean, cancellation reasoning is done with the cancel tactic. In the proof below, you will
see that before the line cancel t at h3 the goal state contains the hypothesis
h3 : t * t = 3 * t
and after that line it has been modified to
h3 : t = 3
Here is the full proof in Lean.
example {t : ℝ} (h1 : t ^ 2 = 3 * t) (h2 : t ≥ 1) : t ≥ 2 := by
have h3 :=
calc t * t = t ^ 2 := by ring
_ = 3 * t := by rw [h1]
cancel t at h3
addarith [h3]
There is a mathematical subtlety here. You can only cancel a common factor from both
sides of an equation if that common factor is known to be nonzero. In this problem, Lean can deduce
that the common factor, t, is nonzero. Why?
2.1.5. Example
Here’s another problem in which we establish an intermediate fact and then simplify it.
Problem
Let \(a\) and \(b\) be real numbers, and suppose that \(a ^ 2 = b ^ 2 + 1\) and that \(a\) is nonnegative. Show that \(a \geq 1\).
Solution
We have that
so \(a\geq 1\).
The deduction from \(a ^ 2 \geq 1 ^ 2\) that \(a \geq 1\) is again something that the
cancel tactic can do. Notice that Lean is silently checking the condition for this to be
valid (that \(a\geq 0\)). Check that if you delete the hypothesis h2 : a ≥ 0 then the
cancellation step fails in Lean.
example {a b : ℝ} (h1 : a ^ 2 = b ^ 2 + 1) (h2 : a ≥ 0) : a ≥ 1 := by
have h3 :=
calc
a ^ 2 = b ^ 2 + 1 := by rw [h1]
_ ≥ 1 := by extra
_ = 1 ^ 2 := by ring
cancel 2 at h3
2.1.6. Example
We conclude the section with some exercises translating prose proofs into Lean proofs. The difficult part with these problems is to pick out, from the text, what the intermediate statements are.
First, we redo one more example, this time Example 1.4.1. The problem was:
Problem
Let \(x\) and \(y\) be integers, and suppose that \(x + 3 \le 2\) and \(y + 2x\geq 3\). Show that \(y>3\).
Here is a solution which uses an intermediate step.
Solution
Since \(x + 3 \le 2\), we have \(x \leq -1\). So
Exercise: Identify the intermediate step, and express this solution in Lean.
example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 := by
sorry
2.1.7. Example
This next one is mathematically a little harder.
Problem
Let \(a\) and \(b\) be real numbers and suppose that \(-b \le a \le b\). Show that \(a ^ 2 \le b ^ 2\).
Solution
By the first part of the hypothesis, \(0 \le b + a\), and by the second part of the hypothesis, \(0 \le b - a\).
Therefore \((b + a)(b - a)\) is nonnegative, so
Exercise: Identify the two intermediate steps, and express this solution in Lean. (Note that Lean is a little more powerful here than the human reader: you do not need to give any Lean translation of the step
Therefore \((b + a)(b - a)\) is nonnegative,
instead Lean will figure this out by itself at the point where this is needed.)
example (a b : ℝ) (h1 : -b ≤ a) (h2 : a ≤ b) : a ^ 2 ≤ b ^ 2 := by
sorry
2.1.8. Example
Problem
Let \(a\) and \(b\) be real numbers and suppose that \(a \le b\). Show that \(a ^ 3 \le b ^ 3\).
Notice that we are not assuming that \(a\) and \(b\) be positive, so our easier tricks for the behaviour of inequalities under multiplication/powers do not apply.
Solution
Since \(a \le b\), we have \(0 \le b - a\).
Therefore \(\frac{(b - a)\left[(b - a)^2+3(b+a)^2\right]}{4}\) is nonnegative, so
Exercise: Identify the intermediate step, and express this solution in Lean.
example (a b : ℝ) (h : a ≤ b) : a ^ 3 ≤ b ^ 3 := by
sorry
2.1.9. Exercises
Let \(x\) be a rational number whose square is 4, and which is greater than 1. Show that \(x=2\).
Suggested steps: Prove that \(x(x+2)=2(x+2)\), then cancel to deduce that \(x=2\).
example {x : ℚ} (h1 : x ^ 2 = 4) (h2 : 1 < x) : x = 2 := by sorry
Let \(n\) be an integer satisfying \(n^2+4=4n\). Prove that \(n=2\).
Suggested steps: Prove that \((n-2)^2=0\), cancel the square to deduce that \(n-2=0\), then finish off.
example {n : ℤ} (hn : n ^ 2 + 4 = 4 * n) : n = 2 := by sorry
Let \(x\) and \(y\) be rational numbers, and suppose that \(xy=1\) and \(x \ge 1\). Show that \(y \le 1\).
Suggested steps: Prove that \(0<xy\), cancel \(x\) to deduce that \(0<y\), then give a calculation to prove the goal.
example (x y : ℚ) (h : x * y = 1) (h2 : x ≥ 1) : y ≤ 1 := by sorry
2.2. Invoking lemmas
2.2.1. Example
Here’s a style of problem we haven’t seen before, in which the goal is a disequality, \(x\ne 1\), rather than an equality (\(=\)) or inequality (\(\le\), \(<\), \(\ge\), \(>\)).
Problem
Let \(x\) be a rational number, and suppose that \(3x=2\). Show that \(x\ne 1\).
Solution
It suffices to prove that \(x< 1\). Indeed,
What happened in this problem? We used a piece of “general knowledge”, that if one number is strictly smaller than another then they can’t be the same. Or at least, this feels like general knowledge – just common sense! – but really it is a lemma: a fact that has been proved already 1 by us or someone else, and which we are allowed to invoke in our proof.
When working in Lean, if we want to invoke a lemma in this way, we need to call it out by name.
Someone earlier, in the big Lean mathematical library, has proved this fact and named it
ne_of_lt: 2
lemma ne_of_lt {a b : ℚ} (h : a < b) : a ≠ b :=
We can invoke this lemma in our problem using the Lean apply tactic. At the start of our work
on the problem,
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
our goal state looks like this:
x : ℚ
hx : 3 * x = 2
⊢ x ≠ 1
When we apply the lemma, with our cursor at the end of this line,
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
apply ne_of_lt
the goal state has changed to this:
x : ℚ
hx : 3 * x = 2
⊢ x < 1
So apply ne_of_lt changes (only) the goal: it transforms the goal x ≠ 1 into the goal
x < 1, which we can then solve by our usual methods for inequalities.
example {x : ℚ} (hx : 3 * x = 2) : x ≠ 1 := by
apply ne_of_lt
calc
x = 3 * x / 3 := by ring
_ = 2 / 3 := by rw [hx]
_ < 1 := by numbers
Comparing the text proof and the Lean proof, you will notice that the phrasing in invoking the lemma is rather different. In text, I said,
It suffices to prove that \(x< 1\). Indeed, ….
That is, I effectively stated what the new goal would be, and left the reader to figure out what piece of general knowledge I used to make this change to the goal. In Lean, I don’t need to state what the new goal is, because my reader can find this out for herself by inspecting the goal state. But I do need to explicitly mention the name of the lemma,
apply ne_of_lt
because “it’s general knowledge!” is not a precise enough justification for Lean to find it.
2.2.2. Example
Here’s a similar problem, in which I will prove a disequality by showing the left-hand side is larger, rather than (as in the previous problem) smaller.
Problem
Let \(y\) be a real number. Show that \(y ^ 2 + 1\ne 0\).
Solution
It suffices to prove that \(0 < y ^ 2 + 1\), which is clear since squares are nonnegative.
Exercise: Express the solution to this problem in Lean.
example {y : ℝ} : y ^ 2 + 1 ≠ 0 := by
sorry
Use the lemma ne_of_gt:
lemma ne_of_gt {a b : ℝ} (h : a > b) : a ≠ b :=
2.2.3. Example
Problem
Let \(a\) and \(b\) be real numbers, and suppose that \(a^2+b^2=0\). Show that \(a ^ 2 = 0\).
Solution
It suffices to prove that both \(a ^ 2 \le 0\) and \(a ^ 2 ≥ 0\). The second is clear since squares are nonnegative. For the first,
In Lean use this lemma, the “antisymmetry of the \(\le\) relation”:
lemma le_antisymm {a b : α} (h1 : a ≤ b) (h2 : b ≤ a) : a = b :=
Here is the full proof in Lean.
example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a ^ 2 = 0 := by
apply le_antisymm
calc
a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
_ = 0 := h1
extra
Notice that after applying the lemma, the infoview shows two goals!
2 goals
a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ a ^ 2 ≤ 0
a b : ℝ
h1 : a ^ 2 + b ^ 2 = 0
⊢ 0 ≤ a ^ 2
This mathematically is not surprising, since the lemma had two preconditions, both of which we need to justify. Anyway, having multiple goals is perfectly possible in Lean – there can be many goals at any one time, and the mechanism is simply that any code you write acts on the first goal on the list (until it’s resolved, then work starts on the second goal, etc).
2.2.4. Exercises
Let \(m\) be an integer for which \(m + 1=5\). Show that \(3m\ne 6\).
You may wish to use the fact that two numbers are not equal if the first is greater than the second (you’ll need the lemma
ne_of_gt, as in Example 2.2.2).example {m : ℤ} (hm : m + 1 = 5) : 3 * m ≠ 6 := by sorry
Let \(s\) be a rational number for which \(3s ≤ -6\) and \(2s \ge -4\). Show that \(s=-2\).
You will probably use the lemma
le_antisymm, stating if \(x\le y\) and \(x\ge y\) then \(x = y\).example {s : ℚ} (h1 : 3 * s ≤ -6) (h2 : 2 * s ≥ -4) : s = -2 := by sorry
Footnotes
- 1
In this case, as a consequence of the definition of the relation \(<\) on the rational numbers.
- 2
Here
nestands for “not equal”,ltstands for “less than”, and theofmeans that we are deducing anestatement from altstatement. The standard Lean mathematical library has many such naming conventions, but you don’t need to follow them; you can call your own lemmasfooandbananaif you like.
2.3. “Or” and proof by cases
2.3.1. Example
In mathematics, the word “or” (denoted \(\lor\) as a logical symbol) can connect two statements. For example, here is a problem in which the hypothesis is an “or”-statement.
Problem
Let \(x\) and \(y\) be real numbers and suppose that either \(x=1\) or \(y=-1\). Show that \(xy+x=y + 1\).
The hypothesis
\(x=1\) or \(y=-1\)
tells us that at least one of the alternatives \(x=1\), \(y=-1\) must occur (and possibly both, but this needs no special consideration). So a solution to this problem simply involves considering these two alternatives in turn. This is called a proof by cases.
Solution
If \(x=1\), then
and if \(y=-1\) then
In Lean, an “or”-statement is represented using the logical symbol ∨. At the start of
this problem, the infoview displays one task, with h as the “or”-statement hypothesis, and the
goal as proving that \(xy+x=y + 1\).
x y : ℝ
h : x = 1 ∨ y = -1
⊢ x * y + x = y + 1
To consider in turn the two cases represented by an “or”-statement, we use the tactic obtain.
After applying this tactic, the infoview now displays two simpler tasks. The goal in each task is
still to prove that \(xy+x=y + 1\), but the hypothesis has changed: to the left alternative,
x = 1, in the first task, and to the right alternative, y = -1, in the second task.
x y : ℝ
hx : x = 1
⊢ x * y + x = y + 1
x y : ℝ
hy : y = -1
⊢ x * y + x = y + 1
We can then solve these simpler tasks one by one, giving a calculational proof of each.
example {x y : ℝ} (h : x = 1 ∨ y = -1) : x * y + x = y + 1 := by
obtain hx | hy := h
calc
x * y + x = 1 * y + 1 := by rw [hx]
_ = y + 1 := by ring
calc
x * y + x = x * -1 + x := by rw [hy]
_ = -1 + 1 := by ring
_ = y + 1 := by rw [hy]
2.3.2. Example
More commonly, you will give a proof by cases for a problem in which there is no hypothesis directly structured as an “or”-statement. Instead, you will create such a hypothesis yourself, by setting up and proving an intermediate statement which is an “or”-statement.
Problem
Let \(n\) be any natural number. Show that \(n ^ 2 \ne 2\).
In this problem, we will case-split on the “or”-statement
\(n \le 1\) or \(2 \le n\).
On paper this can be stated without a proof, although really it comes as the application of a lemma about the natural numbers: in general, either \(n\) is less than or equal to one natural number or it’s greater than or equal to the next one. The solution to the problem is easy after this case-split.
Solution
We consider separately the cases \(n \le 1\) and \(2 \le n\).
Case 1 (\(n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,
Case 2 (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,
In Lean, we set up this “or”-statement explicitly as an intermediate fact, the application of a lemma,
lemma le_or_succ_le (a b : ℕ) : a ≤ b ∨ b + 1 ≤ a :=
We have not previously invoked lemmas in this way. The syntax uses have,
have hn := le_or_succ_le n 1
and after this line of code, the infoview displays the or-statement we want:
hn : n ≤ 1 ∨ 2 ≤ n
After establishing the intermediate fact, we case-split on that fact, and are left with two tasks corresponding to the two cases:
n : ℕ
hn : n ≤ 1
⊢ n ^ 2 ≠ 2
n : ℕ
hn : 2 ≤ n
⊢ n ^ 2 ≠ 2
Exercise: The first case has been written up in Lean. Fill in the details of the second case.
example {n : ℕ} : n ^ 2 ≠ 2 := by
have hn := le_or_succ_le n 1
obtain hn | hn := hn
apply ne_of_lt
calc
n ^ 2 ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
sorry
2.3.3. Example
So far we have discussed how to deal with an “or”-statement appearing in a hypothesis. Let us turn to how to deal with an “or”-statement appearing in a goal. This is quite easy: you have to prove one or the other of the alternatives in the “or”-statement, so just announce which one you expect to work, and then prove it.
Problem
Let \(x\) be a real number for which \(2x+1=5\). Show that either \(x=1\) or \(x=2\).
Solution
We will show \(x=2\). Indeed,
In Lean, use the tactic right to announce you will be proving the right alternative of the goal
(or left for the left one). This changes the goal displayed in the infoview: from
⊢ x = 1 ∨ x = 2
before the tactic application to
⊢ x = 2
afterwards.
example {x : ℝ} (hx : 2 * x + 1 = 5) : x = 1 ∨ x = 2 := by
right
calc
x = (2 * x + 1 - 1) / 2 := by ring
_ = (5 - 1) / 2 := by rw [hx]
_ = 2 := by numbers
2.3.4. Example
Let’s do an example which features both these styles of logical reasoning. We solve a quadratic equation; this is a classic situation where the result has an “or” in it. We will get to use the following lemma: if the product of two numbers is zero, then one of them is zero.
Problem
Let \(x\) be a real number for which \(x^2-3x+2=0\). Show that either \(x=1\) or \(x=2\).
Solution
We have that
So either \(x-1=0\) or \(x-2=0\).
If \(x-1=0\), then \(x=1\).
If \(x-2=0\), then \(x=2\).
In this solution, the case division argument is written a little more casually than in previous examples. The phrases “If \(x-1=0\)” and “If \(x-2=0\)” silently introduce the two cases, and it is left to the reader to observe that \(x=1\) is the left alternative of “\(x=1\) or \(x=2\)”, which finishes the problem (similarly for the second case).
I have done the first part of the Lean argument: writing up the calculation which establishes that
\((x-1)(x-2)=0\), then calling on the lemma eq_zero_or_eq_zero_of_mul_eq_zero to turn this
into an “or” hypothesis. The goal state now looks like this, with both an “or” hypothesis and an
“or” goal.
x : ℝ
hx : x ^ 2 - 3 * x + 2 = 0
h1 : (x - 1) * (x - 2) = 0
h2 : x - 1 = 0 ∨ x - 2 = 0
⊢ x = 1 ∨ x = 2
Exercise: Fill in the rest of the Lean version of the argument.
example {x : ℝ} (hx : x ^ 2 - 3 * x + 2 = 0) : x = 1 ∨ x = 2 := by
have h1 :=
calc
(x - 1) * (x - 2) = x ^ 2 - 3 * x + 2 := by ring
_ = 0 := by rw [hx]
have h2 := eq_zero_or_eq_zero_of_mul_eq_zero h1
sorry
2.3.5. Example
In Example 2.3.2 we showed that no natural number squares to 2. It is also true that no integer squares to 2, but since order laws are more complicated when negative numbers are involved, the proof is more complicated, requiring cases within cases.
Problem
Let \(n\) be any integer. Show that \(n ^ 2 \ne 2\).
Solution
We consider separately the cases \(n \le 0\) and \(1 \le n\).
Case 1 (\(n \le 0\)): In this case we have \(0 \le -n\). We consider separately the cases \(-n \le 1\) and \(2 \le -n\).
Case 1(i) (\(-n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,
Case 1(ii) (\(2 \le -n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,
Case 2 (\(1 \le n\)): We consider separately the cases \(n \le 1\) and \(2 \le n\).
Case 2(i) (\(n \le 1\)): It suffices to prove that \(n ^ 2 < 2\). Indeed,
Case 2(ii) (\(2 \le n\)): It suffices to prove that \(n ^ 2 > 2\). Indeed,
When a proof becomes this complicated, you may find it helpful to mark the start of each new
sub-proof with the symbol ·, as follows.
example {n : ℤ} : n ^ 2 ≠ 2 := by
have hn0 := le_or_succ_le n 0
obtain hn0 | hn0 := hn0
· have : 0 ≤ -n := by addarith [hn0]
have hn := le_or_succ_le (-n) 1
obtain hn | hn := hn
· apply ne_of_lt
calc
n ^ 2 = (-n) ^ 2 := by ring
_ ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
· apply ne_of_gt
calc
(2:ℤ) < 2 ^ 2 := by numbers
_ ≤ (-n) ^ 2 := by rel [hn]
_ = n ^ 2 := by ring
· have hn := le_or_succ_le n 1
obtain hn | hn := hn
· apply ne_of_lt
calc
n ^ 2 ≤ 1 ^ 2 := by rel [hn]
_ < 2 := by numbers
· apply ne_of_gt
calc
(2:ℤ) < 2 ^ 2 := by numbers
_ ≤ n ^ 2 := by rel [hn]
We record this theorem for future use under the name sq_ne_two.
2.3.6. Exercises
Let \(x\) be a rational number and suppose that \(x=4\) or \(x=-4\). Show that \(x^2+1=17\).
example {x : ℚ} (h : x = 4 ∨ x = -4) : x ^ 2 + 1 = 17 := by sorry
Let \(x\) be a real number and suppose that either \(x=1\) or \(x=2\). Show that \(x^2-3x+2=0\).
example {x : ℝ} (h : x = 1 ∨ x = 2) : x ^ 2 - 3 * x + 2 = 0 := by sorry
Let \(t\) be a rational number and suppose that \(t=-2\) or \(t=3\). Show that \(t^2-t-6=0\).
example {t : ℚ} (h : t = -2 ∨ t = 3) : t ^ 2 - t - 6 = 0 := by sorry
Let \(x\) and \(y\) be real numbers and suppose that \(x=2\) or \(y=-2\). Show that \(x^2+2x=2y+4\).
example {x y : ℝ} (h : x = 2 ∨ y = -2) : x * y + 2 * x = 2 * y + 4 := by sorry
Let \(s\) and \(t\) be rational numbers for which \(s = 3 - t\). Show that either \(s + t = 3\) or \(s + t = 5\).
example {s t : ℚ} (h : s = 3 - t) : s + t = 3 ∨ s + t = 5 := by sorry
Let \(a\) and \(b\) be rational numbers for which \(a + 2b < 0\). Show that either \(b < a / 2\) or \(b < -a/2\).
example {a b : ℚ} (h : a + 2 * b < 0) : b < a / 2 ∨ b < - a / 2 := by sorry
Let \(x\) and \(y\) be real numbers for which \(y = 2x+1\). Show that either \(x<y/2\) or \(x>y/2\).
example {x y : ℝ} (h : y = 2 * x + 1) : x < y / 2 ∨ x > y / 2 := by sorry
Let \(x\) be a real number for which \(x^2+2x-3=0\). Show that either \(x=-3\) or \(x=1\).
You will probably use the same lemma as in Example 2.3.4.
example {x : ℝ} (hx : x ^ 2 + 2 * x - 3 = 0) : x = -3 ∨ x = 1 := by sorry
Let \(a\) and \(b\) be real numbers for which \(a^2+2b^2=3ab\). Show that either \(a=b\) or \(a=2b\).
You will probably use the same lemma as in Example 2.3.4.
example {a b : ℝ} (hab : a ^ 2 + 2 * b ^ 2 = 3 * a * b) : a = b ∨ a = 2 * b := by sorry
Let \(t\) be a real number for which \(t^3=t^2\). Show that either \(t=1\) or \(t=0\).
You will probably use the same lemma as in Example 2.3.4, as well as the
canceltactic.example {t : ℝ} (ht : t ^ 3 = t ^ 2) : t = 1 ∨ t = 0 := by sorry
Let \(n\) be any natural number. Show that \(n ^ 2 \ne 7\).
You will probably use the same lemma as in Example 2.3.2.
example {n : ℕ} : n ^ 2 ≠ 7 := by sorry
Let \(x\) be any integer. Show that \(2x \ne 3\).
You will probably use the same lemma as in Example 2.3.2.
example {x : ℤ} : 2 * x ≠ 3 := by sorry
Let \(t\) be any integer. Show that \(5t \ne 18\).
You will probably use the same lemma as in Example 2.3.2.
example {t : ℤ} : 5 * t ≠ 18 := by sorry
Let \(m\) be any natural number. Show that \(m ^ 2 +4m\ne 46\).
You will probably use the same lemma as in Example 2.3.2.
example {m : ℕ} : m ^ 2 + 4 * m ≠ 46 := by sorry
2.4. “And”
2.4.1. Example
In mathematics, the word “and” (denoted \(\land\) as a logical symbol), like “or”, can connect two statements. For example, here is a problem in which the hypothesis is an “and”-statement.
Problem
Let \(x\) and \(y\) be integers and suppose that \(2x-y=4\) and \(y-x+1=2\). Prove that \(x=5\).
In fact, we studied this problem before, in Example 1.3.6. Then, we considered the problem as having two separate hypotheses:
\(2x-y=4\)
\(y-x+1=2\)
but now for the sake of argument we’re considering it as having a single hypothesis:
\(2x-y=4\) and \(y-x+1=2\).
The distinction is pretty pedantic, and invisible in the text. In Lean, it’s more visible: we
might find ourselves in a situation with a hypothesis which explicitly features the ∧ symbol,
like
x y : ℤ
h : 2 * x - y = 4 ∧ y - x + 1 = 2
⊢ x = 5
In such a situation, the tactic obtain will split up an “and” hypothesis into its constituent
parts,
x y : ℤ
h1 : 2 * x - y = 4
h2 : y - x + 1 = 2
⊢ x = 5
and then the problem can be solved accessing each of these parts separately, as needed. In this case we have effectively brought the problem back to the setup of Example 1.3.6.
example {x y : ℤ} (h : 2 * x - y = 4 ∧ y - x + 1 = 2) : x = 5 := by
obtain ⟨h1, h2⟩ := h
calc
x = 2 * x - y + (y - x + 1) - 1 := by ring
_ = 4 + 2 - 1 := by rw [h1, h2]
_ = 5 := by ring
2.4.2. Example
“And” hypotheses turn up relatively rarely in the wild. One situation in which one might occur is when a single hypothesis has two natural consequences, which are paired together in a lemma. For example, if \(x^2 \le y^2\) for some positive number \(y\), then one can draw the conclusion \(-y \le x \le y\), which is shorthand (recall Example 1.4.4) for “\(-y\leq x\) and \(x\le y\).”
Problem
Let \(p\) be a rational number for which \(p^2\le 8\). Show that \(p\ge -5\).
Solution
We have that
and 3 is positive, so \(-3\le p\le 3\). Thus
In Lean, we use the lemma abs_le_of_sq_le_sq' for this argument. This lemma was added to Lean’s
library by a Fordham student, Ben Davidson. Note the ∧ in the conclusion of the lemma statement.
theorem abs_le_of_sq_le_sq' {x y : ℚ} (h1 : x ^ 2 ≤ y ^ 2) (h2 : 0 ≤ y) :
-y ≤ x ∧ x ≤ y :=
Exercise: I have written up in Lean the part of the proof which gets us to the intermediate fact
hp' : -3 ≤ p ∧ p ≤ 3. Deal with this “and” hypothesis and then finish the proof in Lean.
example {p : ℚ} (hp : p ^ 2 ≤ 8) : p ≥ -5 := by
have hp' : -3 ≤ p ∧ p ≤ 3
· apply abs_le_of_sq_le_sq'
calc
p ^ 2 ≤ 9 := by addarith [hp]
_ = 3 ^ 2 := by numbers
numbers
sorry
Note a new piece of Lean syntax in the above proof: a line like
have hp' : -3 ≤ p ∧ p ≤ 3
without a justification will cause Lean to ask you for that justification – that is, a new goal will appear, the goal of proving that statement.
2 goals
p : ℚ
hp : p ^ 2 ≤ 8
⊢ -3 ≤ p ∧ p ≤ 3
p : ℚ
hp : p ^ 2 ≤ 8
hp' : -3 ≤ p ∧ p ≤ 3
⊢ p ≥ -5
After you complete the proof (as I did here),
you are back to where you were before except that the fact hp' is now a fully-justified
intermediate fact, available for use.
2.4.3. Example
It also sometimes happens that the goal of a problem features an “and” statement. For example, you might be given a system of simultaneous equations, and asked to determine the values of all the variables appearing. Here’s a system of simultaneous equations we saw before in Example 1.3.3, but the problem statement has been tweaked to ask us to find the values of both \(a\) and \(b\).
Problem
Let \(a\) and \(b\) be real numbers and suppose that \(a-5b=4\) and \(b+2=3\). Show that \(a=9\) and \(b=1\).
One way to solve such a problem is to establish the two facts asked for completely independently:
Solution
We have,
and since \(b+2=3\), we have \(b=1\).
In Lean, we write this proof using the constructor tactic, which takes a problem in which the
goal is an “and” statement,
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9 ∧ b = 1
and reduces it two simpler tasks, one for each part of the “and”.
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ a = 9
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
⊢ b = 1
We then write up Lean proofs for these two tasks, one after the other.
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
constructor
· calc
a = 4 + 5 * b := by addarith [h1]
_ = -6 + 5 * (b + 2) := by ring
_ = -6 + 5 * 3 := by rw [h2]
_ = 9 := by ring
· addarith [h2]
Alternatively, there might be an intermediate fact which you wish to note and then use in both parts of the proof. For example, you might want to first solve for \(b\), and then use that to shorten the work of solving for \(a\).
Solution
Since \(b+2=3\), we have \(b=1\). Therefore
It is typically left to the reader to check that both parts of the desired goal, \(a=9\) and \(b=1\), are established somewhere along the way.
Here is how this proof looks in Lean. The important observation is that if there is something you
want to use in both parts of the proof (here, the fact \(b=1\)), then this must be established
before the tactic constructor is used. When the tactic constructor is used, all facts
established so far become available for both of the two tasks created:
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ a = 9
a b : ℝ
h1 : a - 5 * b = 4
h2 : b + 2 = 3
hb : b = 1
⊢ b = 1
example {a b : ℝ} (h1 : a - 5 * b = 4) (h2 : b + 2 = 3) : a = 9 ∧ b = 1 := by
have hb : b = 1 := by addarith [h2]
constructor
· calc
a = 4 + 5 * b := by addarith [h1]
_ = 4 + 5 * 1 := by rw [hb]
_ = 9 := by ring
· apply hb
2.4.4. Example
One more example with an “and” in the goal.
Problem
Let \(a\) and \(b\) be real numbers and suppose that \(a^2+b^2=0\). Show that \(a=0\) and \(b=0\).
Solution
We first show that \(a^2=0\). \((\star)\) Indeed,
and also since squares are nonnegative \(a^2\geq 0\).
By \((\star)\), \(a=0\). Also by \((\star)\),
so \(b=0\).
Part of this problem might feel familiar. The proof of the intermediate goal, \(a^2=0\), is a repeat of Example 2.2.3.
Here is the problem statement in Lean, together with a proof of the intermediate goal \(a^2=0\)
copied from Example 2.2.3. Fill in the rest of the proof. The tactic
cancel will be helpful to deduce that quantities are zero when their squares are known to be
zero.
example {a b : ℝ} (h1 : a ^ 2 + b ^ 2 = 0) : a = 0 ∧ b = 0 := by
have h2 : a ^ 2 = 0
· apply le_antisymm
calc
a ^ 2 ≤ a ^ 2 + b ^ 2 := by extra
_ = 0 := by rw [h1]
extra
sorry
2.4.5. Exercises
Let \(a\) and \(b\) be rational numbers and suppose that \(a \le 1\) and \(a + b \le 3\). Show that \(2a+b \le 4\).
example {a b : ℚ} (H : a ≤ 1 ∧ a + b ≤ 3) : 2 * a + b ≤ 4 := by sorry
Let \(r\) and \(s\) be real numbers and suppose that \(r + s \le 1\) and \(r - s \le 5\). Show that \(2r \le 6\).
example {r s : ℝ} (H : r + s ≤ 1 ∧ r - s ≤ 5) : 2 * r ≤ 6 := by sorry
Let \(m\) and \(n\) be integers and suppose that \(n \le 8\) and \(m + 5 \le n\). Show that \(m \le 3\).
example {m n : ℤ} (H : n ≤ 8 ∧ m + 5 ≤ n) : m ≤ 3 := by sorry
Let \(p\) be an integer and suppose that \(p + 2 \ge 9\). Show that \(p^2\geq 49\) and \(7 \le p\).
example {p : ℤ} (hp : p + 2 ≥ 9) : p ^ 2 ≥ 49 ∧ 7 ≤ p := by sorry
Let \(a\) be a rational number and suppose that \(a - 1 \ge 5\). Show that \(a \ge 6\) and \(3a \ge 10\).
example {a : ℚ} (h : a - 1 ≥ 5) : a ≥ 6 ∧ 3 * a ≥ 10 := by sorry
Let \(x\) and \(y\) be rational numbers and suppose that \(x + y = 5\) and \(x + 2y = 7\). Show that \(x=3\) and \(y=2\).
example {x y : ℚ} (h : x + y = 5 ∧ x + 2 * y = 7) : x = 3 ∧ y = 2 := by sorry
Let \(a\) and \(b\) be real numbers and suppose that \(ab=a=b\). Show that either \(a=b=0\) or \(a=b=1\).
You will probably need the lemma
eq_zero_or_eq_zero_of_mul_eq_zeroproved in Example 2.3.4.example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) : a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by sorry
2.5. Existence proofs
2.5.1. Example
This section covers the existential quantifier, the logical concept expressed in English as
There exists … such that ….
For example, here is a problem in which a hypothesis features an existential quantifier.
Problem
Let \(a\) be a rational number, and suppose that there exists a rational number \(b\), such that \(a=b^2+1\). Show that \(a>0\).
The hypothesis “there exists a rational number \(b\), such that \(a=b^2+1\)” can be broken down immediately to actually get our hands on the witness for the existential: a rational number \(b\) satisfying \(a=b^2+1\) (there might be more than one, but this will just choose one witness). Then we can do a regular calculational proof which involves the witness \(b\).
Solution
Let \(b\) be a rational number such that \(a=b^2+1\). We have,
The logical symbol for an existential is \(\exists\). In Lean, the tactic obtain is used to
break up an existential hypothesis into a witness and a hypothesis about that witness. The syntax
is the same as the syntax for breaking apart an “and” (see Section 2.4).
example {a : ℚ} (h : ∃ b : ℚ, a = b ^ 2 + 1) : a > 0 := by
obtain ⟨b, hb⟩ := h
calc
a = b ^ 2 + 1 := hb
_ > 0 := by extra
In this problem, the goal view is initially
a : ℚ
h : ∃ b, a = b ^ 2 + 1
⊢ a > 0
After the use of the obtain tactic, the existential is broken apart, so the witness appears
separately on the variable list and can be accessed in the succeeding proof:
a b : ℚ
hb : a = b ^ 2 + 1
⊢ a > 0
2.5.2. Example
Here’s another problem with an existential hypothesis, “there exists a real number \(a\), such that \(at<0\)”. As before we break it apart and then follow earlier methods.
Problem
Let \(t\) be a real number, and suppose that there exists a real number \(a\), such that \(at<0\). Show that \(t\ne 0\).
Solution
Let \(x\) be a real number such that \(xt<0\). We consider separately the cases \(x\le 0\) and \(0<x\).
Case 1 (\(x \le 0\)): We have \(0<(-x)t\) and \(0 \le -x\), so we have that \(0 < t\), and so \(t\ne 0\).
Case 2 (\(0<x\)): We have that
and \(0 \le x\), so \(0 < -t\), so \(t<0\), so \(t\ne 0\),
Here is a partial solution in Lean (using obtain for the first step to break apart the
existential, and then again later to perform the case division). Case 2 is missing; do that
yourself.
example {t : ℝ} (h : ∃ a : ℝ, a * t < 0) : t ≠ 0 := by
obtain ⟨x, hxt⟩ := h
have H := le_or_gt x 0
obtain hx | hx := H
· have hxt' : 0 < (-x) * t := by addarith [hxt]
have hx' : 0 ≤ -x := by addarith [hx]
cancel -x at hxt'
apply ne_of_gt
apply hxt'
· sorry
2.5.3. Example
To prove a problem in which the goal has an existential, you need to provide a witness yourself, and then verify that your proposed witness works.
Problem
Show that there exists an integer \(n\), such that \(12n=84\).
Solution
The integer \(7\) has this property. Indeed, \(12 \cdot 7=84\).
In Lean the tactic use is used to state what you have chosen as the witness.
example : ∃ n : ℤ, 12 * n = 84 := by
use 7
numbers
In this problem, the goal was initially
⊢ ∃ n : ℤ, 12 * n = 84
but after the tactic use 7 the goal has changed to checking that the proposed witness, 7,
works.
⊢ 12 * 7 = 84
This is what numbers checks.
2.5.4. Example
Often, it requires some creativity to come up with a witness for an existential goal. The rest of this section consists of practice coming up with witnesses.
Problem
Let \(x\) be a real number. Show that there exists a real number \(y\), such that \(y>x\).
Solution
The real number \(x + 1\) has this property. Indeed, \(x+1>x\).
example (x : ℝ) : ∃ y : ℝ, y > x := by
use x + 1
extra
2.5.5. Example
Problem
Show that there exist integers \(m\) and \(n\), such that \(m^2-n^2=11\).
Solution
We can take \(m=6\), \(n=5\). Indeed,
example : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 11 := by
sorry
2.5.6. Example
Sometimes you may wish to leave out the sentence “We can take …” explicitly stating what the witness is. In this case you should be extra pedantic about verifying the desired properties exactly in the form they are stated.
Problem
Let \(a\) be an integer. Show that there exist integers \(m\) and \(n\), such that \(m^2-n^2=2a+1\).
Solution
In Lean, you still have to use use to state the witnesses.
example (a : ℤ) : ∃ m n : ℤ, m ^ 2 - n ^ 2 = 2 * a + 1 := by
sorry
2.5.7. Example
Problem
Let \(p\) and \(q\) be real numbers, and suppose \(p<q\). Show that there exists a real number \(x\), such that \(p<x<q\).
Solution
We will show that \(\frac{p+q}{2}\) has this property. Indeed,
and
example {p q : ℝ} (h : p < q) : ∃ x, p < x ∧ x < q := by
sorry
2.5.8. Example
I remember once going to see him [Ramanujan] when he was lying ill at Putney. I had ridden in taxi cab number 1729 and remarked that the number seemed to me rather a dull one, and that I hoped it was not an unfavorable omen. “No,” he replied, “it is a very interesting number; it is the smallest number expressible as the sum of two cubes in two different ways.”
—G. H. Hardy, Ramanujan: Twelve lectures on subjects suggested by his life and work
Problem
Show that there exist natural numbers \(a\), \(b\), \(c\) and \(d\), such that \(a^3+b^3=1729=c^3+d^3\), but \(a\ne c\) and \(a\ne d\). 3
Solution
\(1^3+12^3=1729=9^3+10^3\), but \(1\ne 9\) and \(1\ne 10\).
example : ∃ a b c d : ℕ,
a ^ 3 + b ^ 3 = 1729 ∧ c ^ 3 + d ^ 3 = 1729 ∧ a ≠ c ∧ a ≠ d := by
use 1, 12, 9, 10
constructor
numbers
constructor
numbers
constructor
numbers
numbers
2.5.9. Exercises
Show that there exists a rational number \(t\), such that \(t^2=1.69\).
example : ∃ t : ℚ, t ^ 2 = 1.69 := by sorry
Show that there exist integers \(m\) and \(n\), such that \(m^2+n^2=85\).
example : ∃ m n : ℤ, m ^ 2 + n ^ 2 = 85 := by sorry
Show that there exists a real number \(x\), such that \(x<0\) and \(x^2<1\).
example : ∃ x : ℝ, x < 0 ∧ x ^ 2 < 1 := by sorry
Show that there exist natural numbers \(a\) and \(b\), such that \(2 ^ a = 5b+1\).
example : ∃ a b : ℕ, 2 ^ a = 5 * b + 1 := by sorry
Let \(x\) be a rational number. Show that there exists a rational number \(y\), such that \(y^2>x\).
example (x : ℚ) : ∃ y : ℚ, y ^ 2 > x := by sorry
Let \(t\) be a real number, and suppose that there exists a real number \(a\), such that \(at+1<a+t\). Show that \(t\ne 1\).
As in Example 2.5.2, I used the lemma
le_or_gt, which says that if \(s\) and \(t\) are real numbers then either \(s \le t\) or \(t < s\); it can be a useful case division.example {t : ℝ} (h : ∃ a : ℝ, a * t + 1 < a + t) : t ≠ 1 := by sorry
Let \(m\) be an integer, and suppose that there exists an integer \(a\), such that \(2a=m\). Show that \(m\ne 5\).
example {m : ℤ} (h : ∃ a, 2 * a = m) : m ≠ 5 := by sorry
Let \(n\) be an integer. Show that there exists an integer \(a\), such that \(2a^3 ≥ na+7\).
example {n : ℤ} : ∃ a, 2 * a ^ 3 ≥ n * a + 7 := by sorry
Let \(a\), \(b\) and \(c\) be real numbers, and suppose that \(a\le b+c\), \(b\le a+c\) and \(c\le a+b\). Show that there exist nonnegative real numbers \(x\), \(y\) and \(z\) such that \(a=y+z\), \(b=x+z\) and \(c=x+y\).
example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) : ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by sorry
Footnotes
- 3
Example adapted from Hammack, Book of Proof, Section 7.3.