Three exercises from Chapter 3 of How To Prove It, each done twice: once in prose,
the way you would write it by hand on a Friday, and once in Lean, with the goal state printed
after every single step. The Lean versions are the theorems named
Exercise_3_2_1a, Exercise_3_4_2 and Exercise_3_3_8
in the file Chap3Ex.lean. Same numbers as the book. That is not a coincidence
and it is the reason we are doing this.
How to read the goal states. Everything above the ⊢ is what you have.
The line below it is what you owe. A tactic is a legal move that changes this position.
When the position reads No goals, you have won.
Provenance. Under each code block is a line in small italics saying where it came
from. Blocks marked verbatim are copied from Velleman's own files and are known to
compile. Blocks marked written for this page are mine: the theorem statement is
verbatim from Chap3Ex.lean, but the proof is not machine-checked, because
this page was written without a Lean installation to hand. They are built out of the exact
tactic patterns Velleman uses, so they should be fine — but check them yourself in
Lean. That is the assignment anyway. If one fails, tell me and I will fix the page.
The problem. Suppose P → Q and Q → R are both true. Show that P → R.
This is the smallest interesting proof in the book, which makes it the right place to watch the machinery work. There is nothing to be clever about; the entire content is "do the obvious thing in the obvious order," and that is precisely what we want to watch Lean bookkeep.
Suppose P.
Since P → Q and P, it follows that Q.
Since Q → R and Q, it follows that R.
Therefore P → R. □
theorem Exercise_3_2_1a (P Q R : Prop)
(h1 : P → Q) (h2 : Q → R) : P → R := by
assume h3 : P
have h4 : Q := h1 h3
show R from h2 h4
doneStatement verbatim from Chap3Ex.lean; proof written for this page (not machine-checked).
Four lines against four sentences. The correspondence is exact, sentence for line, and that is the design goal of Velleman's dialect. Now the same thing slowly.
You place your cursor just after by and the Infoview shows:
P Q R : Prop h1 : P → Q h2 : Q → R ⊢ P → R
The first line says P, Q and R are propositions — the things
that can be true or false. The next two give names, h1 and h2,
to the two hypotheses. The last line is the goal. Note that the hypotheses are named:
in Lean you refer to a hypothesis by its name the way you refer to a variable, and this
is the first small discipline the system imposes. On paper you write "by the hypothesis";
here you have to say which one.
assume h3 : P
English: "Suppose P."
What it does: The goal is a conditional, P → R. The move for a
conditional goal is always the same: assume the antecedent, prove the consequent.
assume does exactly that, and makes you name the assumption — here
h3.
P Q R : Prop h1 : P → Q h2 : Q → R h3 : P ⊢ R
h3 : P has moved up above the line. It is now something you have, rather than
something you owe. The goal shrank from P → R to R. This
trade — the arrow's left side goes up, its right side stays down — is the
single most common event in Chapter 3, and Lean makes it literal.
have h4 : Q := h1 h3
English: "Since P → Q and P, we have Q."
What it does: have introduces a new fact into the list above the line.
You state what the fact is (Q), give it a name (h4), and after
:= supply the reason. The reason here is h1 h3, which is Lean's
notation for modus ponens: writing a proof of P → Q next to a proof of
P gives you a proof of Q.
P Q R : Prop h1 : P → Q h2 : Q → R h3 : P h4 : Q ⊢ R
The goal has not changed. That is normal and correct: have is how you make
progress by accumulating, rather than by simplifying what is owed. Most proofs alternate
between the two.
show R from h2 h4
English: "Since Q → R and Q, we have R, which is
what was to be shown."
What it does: show G from e says "the goal is G, and here
is a proof of it." It is have for the last step: same idea, except that
instead of adding a fact, it discharges the goal. Restating the goal explicitly is
optional in principle and mandatory in practice — it is what makes a Lean proof
readable a week later.
No goals
done
English: the little box at the end.
What it does: asserts that nothing remains. If something did remain,
done errors and tells you what. It is a checkpoint you write on purpose, and
you will come to like it: it converts "I think I'm finished" into a claim the machine can
contradict.
h1 h3 is written like a function call
Because it is one. In Lean's foundation, a proposition is a type and a proof of it is a
term of that type. The proposition P → Q is literally the type of functions
from proofs of P to proofs of Q. So h1 is a
function, h3 is an argument, and h1 h3 is an application whose
value is a proof of Q. Modus ponens is not a rule bolted onto the system;
it is function application, and the rule for a conditional goal is lambda abstraction.
This is the Curry–Howard correspondence, and it is the reason the whole enterprise
works at all: checking a proof reduces to typechecking a program, which is decidable and
fast. Once you have seen it, ∀ is a dependent product,
∃ is a dependent sum, and And.intro (which shows up in the next
example) is the pairing constructor. You do not need any of this to do the exercises.
It is worth knowing that the exercises are not pretending.
A visible consequence: everything after from or := is a
term, written in a different sublanguage from the tactics. h2 h4,
And.intro h4 h5, Exists.intro x h are all terms. Tactics like
assume and fix are, underneath, machinery for building such
terms without your having to write them out.
assume, fix, obtain, show,
define, by_cases on, by_induc,
contradict, demorgan, contrapos,
quant_neg, disj_syll, or_right and
exists_unique are all defined by Velleman in HTPIDefs.lean.
They are marked with an asterisk in the book's appendix for precisely this reason. Only
have, apply, rewrite, calc,
ring and a few others are standard.
Standard Lean writes intro h3 for both assume h3 : P and
fix x : U — one tactic doing two jobs, without the type annotation and
without the distinction between assuming a hypothesis and introducing a variable. That is
more concise and much less legible to a student in week eight, which is why Velleman split
it. Similarly, standard Lean writes h.mp and h.mpr where we write
h.ltr and h.rtl.
The book's appendix has a section titled Transitioning to Standard Lean that gives the replacement for every asterisked tactic. If you go on to use Lean for anything real, that page is a half-hour of reading and then you are fine.
The problem. Suppose A ⊆ B and A ⊆ C. Show that A ⊆ B ∩ C.
Now there are sets, and the interesting thing happens before the first tactic: you have to decide what A ⊆ B ∩ C even is. It is ∀x(x ∈ A → x ∈ B ∩ C). Unwinding that definition is the entire first move, and it is the move students most often skip on paper.
Let x be arbitrary, and suppose x ∈ A.
Since A ⊆ B, x ∈ B.
Since A ⊆ C, x ∈ C.
Hence x ∈ B and x ∈ C, so x ∈ B ∩ C.
Since x was arbitrary, A ⊆ B ∩ C. □
theorem Exercise_3_4_2 (U : Type) (A B C : Set U)
(h1 : A ⊆ B) (h2 : A ⊆ C) : A ⊆ B ∩ C := by
define
fix x : U
assume h3 : x ∈ A
have h4 : x ∈ B := h1 h3
have h5 : x ∈ C := h2 h3
show x ∈ B ∩ C from And.intro h4 h5
doneStatement verbatim from Chap3Ex.lean; proof written for this page (not machine-checked).
U : Type A B C : Set U h1 : A ⊆ B h2 : A ⊆ C ⊢ A ⊆ B ∩ C
U : Type is the universe of discourse — Velleman's U, made
explicit. A B C : Set U says the three sets are sets of elements of that
universe. Lean will not let you write a set without saying what it is a set of,
which is a small tax that buys you the entire absence of Russell's paradox.
define
English: "By the definition of ⊆, what we must show is: for every x,
if x ∈ A then x ∈ B ∩ C."
What it does: define unfolds the definition of whatever is outermost
in the goal. Here that is ⊆.
U : Type A B C : Set U h1 : A ⊆ B h2 : A ⊆ C ⊢ ∀ ⦃a : U⦄, a ∈ A → a ∈ B ∩ C
The double brackets ⦃ ⦄ mark a strict implicit argument, which is
Lean's way of saying that when you later write h1 h3, it will figure out from
h3 which element you meant, so you do not have to say. Ignore the brackets;
read the line as "for all a."
define is optional here — the next tactic would have unfolded it
silently. It is worth writing anyway, at least while you are learning, because looking
at what a definition unfolds to is the single most useful thing this tool does for you.
There is also define at h1, which unfolds a hypothesis instead of the goal.
fix x : U
English: "Let x be an arbitrary element of U."
What it does: The goal is universally quantified. The move for a universal goal is
to introduce an arbitrary object and prove the statement about it. fix is
that move. Note that it is a different tactic from assume: you assume
a hypothesis, you fix an object. Standard Lean uses intro for both and the
distinction is lost; Velleman keeps it because on paper it is the distinction between
"suppose" and "let."
U : Type A B C : Set U h1 : A ⊆ B h2 : A ⊆ C x : U ⊢ x ∈ A → x ∈ B ∩ C
x is now a name above the line, with no properties whatsoever. That
namelessness is exactly what "arbitrary" means, and it is enforced: there is no way to
accidentally use a property of x that you did not prove, because there are none
recorded.
assume h3 : x ∈ AConditional goal, same move as before.
U : Type A B C : Set U h1 : A ⊆ B h2 : A ⊆ C x : U h3 : x ∈ A ⊢ x ∈ B ∩ C
have h4 : x ∈ B := h1 h3 and have h5 : x ∈ C := h2 h3
English: "Since A ⊆ B and x ∈ A,
x ∈ B."
What it does: Here is the payoff for the unfolding in step 1. Since
A ⊆ B is the statement ∀ ⦃a⦄, a ∈ A → a ∈ B, and since a
conditional is a function, h1 is a function that eats a proof of
x ∈ A and returns a proof of x ∈ B. So h1 h3 is
that proof, written exactly the way modus ponens was written in the first example. You do
not have to define at h1 first; Lean sees through the definition.
U : Type A B C : Set U h1 : A ⊆ B h2 : A ⊆ C x : U h3 : x ∈ A h4 : x ∈ B h5 : x ∈ C ⊢ x ∈ B ∩ C
show x ∈ B ∩ C from And.intro h4 h5
English: "Therefore x is in both, i.e. in the intersection."
What it does: x ∈ B ∩ C unfolds to x ∈ B ∧ x ∈ C, and
And.intro is the thing that builds a proof of a conjunction out of proofs of
the two halves. Read And.intro h4 h5 as "the pair consisting of h4
and h5." Going the other way, if h : P ∧ Q then
h.left : P and h.right : Q; you will see those constantly.
No goals
Notice what did not happen. Nowhere did we say "since x was arbitrary." On
paper that sentence is load-bearing and forgetting it is a real error. In Lean it is
structural: x was introduced by fix, nothing about it was ever
assumed, and the proof term that gets built is a function of x. You cannot
forget to do it and you cannot fake having done it. This is the sort of thing formalizing
teaches by removing the possibility of the mistake, and it is why doing a few of these
makes the paper proofs better.
The problem. Suppose A ∈ F, where F is a family of sets. Show that A ⊆ ⋃F.
This one is short but it introduces the third kind of goal — existential — and it is the first time the definition you unfold is genuinely worth unfolding, because almost nobody has the definition of ⋃F memorized in the right form.
Let x be arbitrary and suppose x ∈ A.
To show x ∈ ⋃F, we must produce a set in F containing x.
Take that set to be A. Indeed A ∈ F by hypothesis, and x ∈ A by assumption.
Since x was arbitrary, A ⊆ ⋃F. □
theorem Exercise_3_3_8 (U : Type) (F : Set (Set U)) (A : Set U)
(h1 : A ∈ F) : A ⊆ ⋃₀ F := by
fix x : U
assume h2 : x ∈ A
define
apply Exists.intro A
show A ∈ F ∧ x ∈ A from And.intro h1 h2
doneStatement verbatim from Chap3Ex.lean; proof written for this page (not machine-checked). It follows the shape of Example_3_3_5 in HTPILib/Chap3.lean, which proves the analogous fact.
F : Set (Set U) is a set of sets of elements of U — Velleman's
ℱ. The symbol ⋃₀ is typed \bigcup and then
0; the little zero is Lean's way of distinguishing "union of a family" from
"union of two sets."
The two moves worth watching are these.
define on the goal x ∈ ⋃₀ FU : Type F : Set (Set U) A : Set U h1 : A ∈ F x : U h2 : x ∈ A ⊢ ∃ (t : Set U), t ∈ F ∧ x ∈ t
There it is: "x belongs to the union of the family" means "there is a member of the
family that x belongs to." Lean may print this using its shorthand
∃ t ∈ F, x ∈ t, which means the same thing, and the bound variable might be
called something other than t. What matters is the shape: an
∃ whose body is an ∧.
apply Exists.intro A
English: "Take the set to be A."
What it does: The move for an existential goal is to supply a witness. You name the
object and the goal becomes the claim about that specific object.
U : Type F : Set (Set U) A : Set U h1 : A ∈ F x : U h2 : x ∈ A ⊢ A ∈ F ∧ x ∈ A
The quantifier is gone and what remains is a conjunction of two things you already have. This is the formal counterpart of the sentence students most often omit: which object are you claiming exists? Lean makes you write it down before it will let you proceed, and the discipline of choosing the witness first — rather than gesturing at one mid-sentence — is worth carrying back to paper.
The dual move, for when an existential is a given rather than a goal, is
obtain:
obtain (a : U) (h3 : ∀ (y : U), P a → Q y) from h2Verbatim line from a Section 3.3 example in HTPILib/Chap3.lean (Velleman).
Read it as "let a be an object such that…, which exists by h2."
It is the existential instantiation of Chapter 3, and, like fix, it gives you
an object about which you know exactly one thing and nothing else.
Everything above has my proofs in it. Here are two of his, copied out of the package without changes, so that you have something on this page that is certainly correct to calibrate against. Both prove the same theorem, Example 3.2.4 in the book.
theorem Example_3_2_4_v2 (P Q R : Prop)
(h : P → (Q → R)) : ¬R → (P → ¬Q) := by
assume h2 : ¬R
assume h3 : P
by_contra h4
have h5 : Q → R := h h3
have h6 : R := h5 h4
show False from h2 h6
doneVerbatim from HTPILib/Chap3.lean (Velleman).
theorem Example_3_2_4_v3 (P Q R : Prop)
(h : P → (Q → R)) : ¬R → (P → ¬Q) := by
assume h2 : ¬R
assume h3 : P
by_contra h4
contradict h2
show R from h h3 h4
doneVerbatim from HTPILib/Chap3.lean (Velleman).
Both open the same way. The goal ¬Q is a negation, so by_contra h4
assumes h4 : Q and changes the goal to False. In v2
we then build R and finish by noting that h2 : ¬R applied to
h6 : R yields False. In v3, contradict h2
does the bookkeeping differently: it says "I will get my contradiction out of
h2," and so replaces the goal False with the goal R.
The two are the same proof written with different amounts of ceremony, and comparing them is a good exercise in seeing what a proof is as opposed to how it is spelled.
theorem Example_3_5_2
(U : Type) (A B C : Set U) :
A \ (B \ C) ⊆ (A \ B) ∪ C := by
fix x : U
assume h1 : x ∈ A \ (B \ C)
define; define at h1
have h2 : x ∉ B \ C := h1.right
define at h2; demorgan at h2
--h2 : x ∉ B ∨ x ∈ C
by_cases on h2
· -- Case 1. h2 : x ∉ B
apply Or.inl
show x ∈ A \ B from And.intro h1.left h2
done
· -- Case 2. h2 : x ∈ C
apply Or.inr
show x ∈ C from h2
done
doneVerbatim from HTPILib/Chap3.lean (Velleman), his comment included.
Three new things. demorgan at h2 rewrites a negated conjunction into a
disjunction, in place — De Morgan's law as a single legal move rather than a
paragraph. by_cases on h2 splits a disjunctive given into two cases, and the
two · bullets are the two cases; note that the block belonging to each bullet
is indented under it, and each ends with its own done. Or.inl and
Or.inr prove a disjunctive goal by choosing the left or right disjunct.
Also note h1.right and h1.left: h1 is (after
unfolding) a conjunction, and those are its two halves. And define; define at h1
on one line — a semicolon just sequences two tactics.
| Tactic | Use it when | What it means on paper |
|---|---|---|
assume h : P | the goal is P → Q | "Suppose P." |
fix x : U | the goal is ∀ x, ... | "Let x be arbitrary." |
have h : P := e | you can derive a useful fact | "Since …, we have P." |
show P from e | you can finish the current goal | "which is what was to be shown." |
define | the goal contains a definition to unwind | "By definition, this says…" |
define at h | a given contains a definition to unwind | same, applied to a hypothesis |
apply Exists.intro a | the goal is ∃ x, ... | "Take x = a." |
obtain (a : U) (h : ...) from h2 | a given is ∃ x, ... | "Let a be such that…" |
And.intro h1 h2 | the goal is P ∧ Q | "Both hold, so the conjunction does." |
h.left, h.right | a given is P ∧ Q | "In particular…" |
by_contra h | the goal is ¬P or you want contradiction | "Suppose not." |
contradict h | the goal is False | "It suffices to contradict h." |
by_cases on h | a given is P ∨ Q | "Case 1… Case 2…" |
demorgan at h | a given is a negated ∧ or ∨ | "By De Morgan's law…" |
done | you think you are finished | □ |
Every tactic in that table except have, apply and the
And/Or/Exists constructors is part of Velleman's
dialect. The book's appendix
has the complete list and the standard-Lean translations.
Open Chap3Ex.lean. These are in there, in this order, and you have done all of
them on paper already:
Exercise_3_2_1b — (h1 : ¬R → (P → ¬Q)) : P → (Q → R).
Two assumes and a by_contra.Exercise_3_2_2a — (h1 : P → Q) (h2 : R → ¬Q) : P → ¬R.Exercise_3_3_9 — (h1 : A ∈ F) : ⋂₀ F ⊆ A. The dual of
3.3.8 above; define tells you what changed.Exercise_3_3_10, Exercise_3_3_12, Exercise_3_4_4
— more of the same, slowly getting less mechanical.Exercise names and statements verbatim from Chap3Ex.lean.
When one of them stops being mechanical, stop and write it on paper first. That is not a retreat; it is the whole method.