One theorem, done properly: the composition of two one-to-one functions is one-to-one
— Theorem 5.2.5(1) in How To Prove It. In the package it is
Theorem_5_2_5_1, in HTPILib/Chap5.lean, and the proof below is
Velleman's own, copied without changes. Everything on this page except the last section is
verbatim, so you can trust it.
By the time we look at this, you will already have proved it on paper: Chapter 5 is done in class in November, and the Lean side of it comes afterwards. That ordering is deliberate; see the hub page.
Reading the goal states. Above the ⊢: what you have. Below it: what
you owe. Velleman writes the intermediate states as comments in his own source, and the
states quoted below are his, verbatim, which is as authoritative as it gets.
Before the theorem there is a question worth a minute: what, exactly, is a function to
Lean? In Chapter 5 Velleman defines a function as a set of ordered pairs with a
single-valuedness property, and then proves that this matches the built-in notion. Lean's
built-in notion is primitive: f : A → B is a first-class object, and
f a is its value. The two are reconciled in Section 5.1 by
func_from_graph. For our purposes, f : A → B is a function and
that is that.
The two properties we care about are defined like this:
def onto {A B : Type} (f : A → B) : Prop :=
∀ (y : B), ∃ (x : A), f x = y
def one_to_one {A B : Type} (f : A → B) : Prop :=
∀ (x1 x2 : A), f x1 = f x2 → x1 = x2Verbatim from HTPILib/Chap5.lean (Velleman).
These are the book's definitions, transcribed. Nothing is hidden and nothing is cleverer
than what is on the page. The braces in {A B : Type} mean those arguments are
implicit: Lean works out the types from f, so you write
one_to_one f, not one_to_one A B f.
Note that one_to_one f is a defined notion, so it is opaque until you
unfold it. That is what define is for, and on this page define
does most of the work.
The theorem. If f : A → B and g : B → C are both one-to-one, then g ∘ f is one-to-one.
Suppose f and g are one-to-one.
Let a1 and a2 be arbitrary elements of A, and suppose (g ∘ f)(a1) = (g ∘ f)(a2).
By the definition of composition, this says g(f(a1)) = g(f(a2)).
Since g is one-to-one, f(a1) = f(a2).
Since f is one-to-one, a1 = a2.
Since a1 and a2 were arbitrary, g ∘ f is one-to-one. □
theorem Theorem_5_2_5_1 {A B C : Type} (f : A → B) (g : B → C) :
one_to_one f → one_to_one g → one_to_one (g ∘ f) := by
assume h1 : one_to_one f
assume h2 : one_to_one g
define at h1
define at h2
define
fix a1 : A
fix a2 : A
define : (g ∘ f) a1; define : (g ∘ f) a2
assume h3 : g (f a1) = g (f a2)
have h4 : f a1 = f a2 := h2 (f a1) (f a2) h3
show a1 = a2 from h1 a1 a2 h4
doneVerbatim from HTPILib/Chap5.lean (Velleman), with his inline goal-state comments moved into the walkthrough below.
Nine tactic lines for six sentences, and the extra three are all define. That
is the honest ratio for Chapter 5: what costs you lines in Lean is the unfolding that on
paper you do silently, in your head, correctly, most of the time.
A B C : Type f : A → B g : B → C ⊢ one_to_one f → one_to_one g → one_to_one (g ∘ f)
Note the shape of the goal. It is not "P and Q imply R"; it is
"P implies (Q implies R)." Those are equivalent, and Lean prefers the
second because it composes better. It is why there are two assumes in a row.
assume h1 : one_to_one f, assume h2 : one_to_one g"Suppose f is one-to-one. Suppose g is one-to-one." Conditional goal, twice.
A B C : Type f : A → B g : B → C h1 : one_to_one f h2 : one_to_one g ⊢ one_to_one (g ∘ f)
define at h1 and define at h2
English: "By the definition of one-to-one, h1 says: for all
x1, x2 in A, if
f(x1) = f(x2) then
x1 = x2."
What it does: unfolds the definition inside a hypothesis, in place. The
hypothesis keeps its name and changes its displayed form.
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2 h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2
This is the step that matters, and it is worth pausing on. one_to_one f is a
name. It is not usable as a name; it is usable as the universally quantified conditional
it abbreviates. On paper, "since g is one-to-one" is a phrase you deploy without
consciously expanding. In Lean you expand it, look at it, and then apply it — and
having looked at it, you notice things, such as that it quantifies over two
variables, which is exactly what you will need in a moment.
defineSame unfolding, applied to the goal.
Goal : ∀ (x1 x2 : A), (g ∘ f) x1 = (g ∘ f) x2 → x1 = x2
The goal is now universally quantified over two variables, with a conditional inside.
Chapter 3 tells you exactly what to do with that, and it does not matter in the least that
the subject is functions: fix, fix, assume. This is
the payoff of Chapter 3, and it is the reason the Lean pass over Chapter 5 comes at the end
of the term rather than as a new topic in September. There is no November Lean day: Chapters 5
and 6 share the partial Lean slot on Friday, December 11, which also carries Quiz 11 and
§8.3, so that meeting is a demonstration. This page is written so that you can work through
the theorem on your own without it.
fix a1 : A, fix a2 : A"Let a1 and a2 be arbitrary."
Goal : (g ∘ f) a1 = (g ∘ f) a2 → a1 = a2
define : (g ∘ f) a1; define : (g ∘ f) a2
English: "By the definition of composition, (g ∘ f)(a)
means g(f(a))."
What it does: a third form of define. Written
define : e, it unfolds the specific expression e wherever it
appears, rather than unfolding whatever happens to be outermost. You need the pointed
version here because the outermost thing in the goal is the arrow, not the composition.
The semicolon just runs two tactics in sequence on one line.
Goal : g (f a1) = g (f a2) → a1 = a2
This is the whole substance of the proof, made visible. Composition is a definition, not a fact; unfolding it is the only move available, and once it is unfolded the rest is two applications of hypotheses.
assume h3 : g (f a1) = g (f a2)A B C : Type f : A → B g : B → C h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2 h2 : ∀ (x1 x2 : B), g x1 = g x2 → x1 = x2 a1 a2 : A h3 : g (f a1) = g (f a2) ⊢ a1 = a2
Look at this position for a moment. It is the entire proof, laid out: two universally quantified conditionals and one equation, and one equation owed. Everything from here is forced.
have h4 : f a1 = f a2 := h2 (f a1) (f a2) h3
English: "Since g is one-to-one, f(a1) =
f(a2)."
What it does: h2 is a ∀ over two variables followed by a
conditional. You instantiate a ∀ by writing the objects after it, and you
apply a conditional by writing the proof of the antecedent after that. So
h2 (f a1) (f a2) h3 reads left to right as: take h2, specialize
it at f a1 and f a2, then feed it h3. The result is
a proof of f a1 = f a2.
Notice that we instantiate h2 — the one about g — at
elements of B, namely f a1 and f a2. Getting that
backwards is the classic error in this proof, and on paper it is easy to make and hard to
see. Here it does not typecheck.
... h3 : g (f a1) = g (f a2) h4 : f a1 = f a2 ⊢ a1 = a2
show a1 = a2 from h1 a1 a2 h4"Since f is one-to-one, a1 = a2." The same move with the other hypothesis, and the goal is discharged.
No goals
The one thing to take away. The proof has exactly two ideas — unfold "one-to-one," unfold "composition" — and after that it is bookkeeping. That is true of the paper proof too, but on paper the bookkeeping is invisible, so students conclude the proof was mostly idea and cannot reproduce it. Watching the goal state shrink line by line shows you the real ratio, which is roughly one idea to five mechanical steps. Knowing that ratio is calming, and it is a large part of what a first proofs course is for.
onto, and where obtain comes back
The companion theorem — the composition of two onto functions is onto — has
the same skeleton with the quantifiers the other way round, so the Chapter 3 moves swap:
obtain instead of have, apply Exists.intro instead
of fix.
theorem Theorem_5_2_5_2 {A B C : Type} (f : A → B) (g : B → C) :
onto f → onto g → onto (g ∘ f) := by
assume h1 : onto f
assume h2 : onto g
define at h1 --h1 : ∀ (y : B), ∃ (x : A), f x = y
define at h2 --h2 : ∀ (y : C), ∃ (x : B), g x = y
define --Goal : ∀ (y : C), ∃ (x : A), (g ∘ f) x = y
fix c : C
obtain (b : B) (h3 : g b = c) from h2 c
obtain (a : A) (h4 : f a = b) from h1 b
apply Exists.intro a --Goal : (g ∘ f) a = c
rewrite [comp_def] --Goal : g (f a) = c
rewrite [←h4] at h3
show g (f a) = c from h3
doneVerbatim from HTPILib/Chap5.lean (Velleman), his comments included.
Two things are new. rewrite [comp_def] uses a previously proved lemma
(comp_def, one line above it in Velleman's file, which says
(g ∘ f) x = g (f x)) to rewrite the goal. And
rewrite [←h4] at h3 rewrites backwards — the left arrow
←, typed \l, means "use this equation right-to-left" —
inside the hypothesis h3, turning g b = c into
g (f a) = c by replacing b with f a.
rewrite is substitution of equals for equals, which on paper is invisible and
in Lean is a tactic you invoke by name. It is the single largest source of "why won't it
just do the obvious thing" among beginners. The answer is that Lean will not substitute
without being told where and in which direction.
calc proof, and a genuinely slick argumentTheorem 5.3.3(1): if g ∘ f = id, then f is one-to-one. The paper proof is a chain of equalities, and Lean has a construct that writes chains of equalities the way you would on a blackboard.
theorem Theorem_5_3_3_1 {A B : Type} (f : A → B) (g : B → A)
(h1 : g ∘ f = id) : one_to_one f := by
define --Goal : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
fix a1 : A; fix a2 : A
assume h2 : f a1 = f a2
show a1 = a2 from
calc a1
_ = id a1 := by rfl
_ = (g ∘ f) a1 := by rw [h1]
_ = g (f a1) := by rfl
_ = g (f a2) := by rw [h2]
_ = (g ∘ f) a2 := by rfl
_ = id a2 := by rw [h1]
_ = a2 := by rfl
doneVerbatim from HTPILib/Chap5.lean (Velleman).
Read the calc block as one long chain: a1 = id
a1 = (g∘f)(a1) = … =
a2. The underscore stands for "the right-hand side of the previous line."
After each := is the justification for that one step. rfl
(reflexivity) means "these two are the same thing by definition, nothing to prove";
rw [h1] means "rewrite using the equation h1."
Every step here is either a definitional unfolding or one substitution. The proof is
completely mechanical, and yet on paper this is the argument that makes students say "how
would I ever have thought of that." The answer, visible in the calc block, is
that you would not have to: there is only one direction to go at each stage.
In Chap5Ex.lean, Section 5.2:
theorem Exercise_5_2_10b {A B C : Type} (f: A → B) (g : B → C) :
one_to_one (g ∘ f) → one_to_one f := sorryVerbatim from Chap5Ex.lean (Velleman). sorry is Lean's placeholder meaning "trust me" — your job is to replace it with by and a proof.
It is the converse-ish direction: if the composite is injective, the first function
must have been. Prove it on paper first. Then note that you now need to go the other way
through the composition — you have an equation about f and you need one about
g ∘ f — which means calc rather than plain
have.
Related, and a good second one: Exercise_5_2_10a, which says
onto (g ∘ f) → onto g. Ask yourself before starting why the exercises pair
"one-to-one" with f and "onto" with g, and not the other way. The asymmetry
is the content.
theorem Exercise_5_2_10b {A B C : Type} (f: A → B) (g : B → C) :
one_to_one (g ∘ f) → one_to_one f := by
assume h1 : one_to_one (g ∘ f)
define at h1
define
fix a1 : A; fix a2 : A
assume h2 : f a1 = f a2
have h3 : (g ∘ f) a1 = (g ∘ f) a2 :=
calc (g ∘ f) a1
_ = g (f a1) := by rfl
_ = g (f a2) := by rw [h2]
_ = (g ∘ f) a2 := by rfl
show a1 = a2 from h1 a1 a2 h3
doneStatement verbatim from Chap5Ex.lean; proof written for this page (not machine-checked). It is assembled from the exact patterns in Theorem_5_2_5_1 and Theorem_5_3_3_1 above — but check it in Lean rather than believing this page.
Notice that g never appears as a hypothesis and is never assumed to be
anything. It is along for the ride. That is the content of the exercise: injectivity of a
composite says nothing about the outer function, and everything about the inner one.