This morning you learnt some fundamental tactics like
`rw`, `apply`, `exact`, `have` and `intro`.
To make complex mathematical statements, we need to be
able to use logical connectives and quantifiers. In this session
we'll learn how to do that, using the tactics you saw this morning,
For each logical construction, we need to know two things:
1. how to *use* a statement containing it, like a local hypothesis,
or a theorem in the library
2. how to *prove* a statement containing it.
## Tactics we'll use in this section:
Tactics we won't really discuss are in brackets.
# `→`, `¬`, `∀`: the function-like logical constructions
· To use: `apply`, `apply _ at _`, `exact`, `specialize`
· To prove: `intro`, `push_neg` (for `¬`), `rintro`
# `∧`, `↔`, `∃`: inductive propositions with 1 constructor
· To use: `rcases ⟨_, _⟩`, `rw` (for `↔`), (`choose`, `cases`,
`cases'`, `obtain`, `match`)
· To prove: `constructor`, `use`, (`exact ⟨_, _⟩`)
# `∨`: inductive proposition with 2 constructors
· To use: `rcases _ | _`, (`cases`, `cases'`, `match`)
· To prove: `left`, `right`
# Miscellaneous tactics we'll meet
· `assumption`, `exfalso`, `unfold`, `rfl`, `ext`, `by_contra`,
`by_cases`, `contrapose!`, `tauto`, `set`
Anything proved with `sorry` in this file is an exercise.
You can make the exercises easier by using `apply?`, `rw?`
or `exact?` and thus finding the corresponding result in
mathlib, but that's not really the point of them - the point is
to understand how to deal with logical connectives yourself.
Sometimes you might find yourself having to use the same sublemma
in multiple different exercises. See if you can state it as a
separate lemma (don't state it as an `example` - state it as `lemma`
and give it a name) so that you can use it whenever you need to.
Feel free to turn the existing `example`s into lemmas if you want to
Factoring out the right lemmas is a really important skill to learn.
Do whichever exercises you feel you need to; the last 2 are a little
set_option linter.unusedVariables false
## Function-like logical constructions: implication,
## negation, and the universal quantifier
We start with implication statements, `¬` statements and `∀` statements.
All three are kind of similar. -/
An implication statement is a statement of the form "P implies Q", where
`P` and `Q` are propositions. In Lean this is written as `P → Q`, like a
function type; a proof of `P → Q` behaves like a function too.
You can type `→` with `\to`.
(This is part of the "propositions-as-types paradigm". Types are where "data"
live - `ℕ` is a type, and it has terms like `0` and `5`. A proposition
`P : Prop` is like `ℕ` in that it can have terms - i.e. proofs - but any 2
"terms of type `P`" are equivalent in Lean, because it's proof-irrelevant. If
a proposition is false, it has no terms.)
/- First let's see how to *use* an implication statement;
you already know how to do this. -/
example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
So we can see `hPQ` as a function that eats a term of type `P` - i.e. a
proof - and spits out a proof of `Q`. You've already seen `apply`; we use
it to reason backwards, using `hPQ` to say "to prove `Q`, it suffices to
A more intuitive use of the word `apply` is in "`apply _ at _`":
this lets us apply an implication statement to an existing hypothesis
- i.e. use forward reasoning.
example (P Q : Prop) (hPQ : P → Q) (hP : P) : Q := by
Next we need to know how to prove an "implies" statement.
lemma one (P Q : Prop) (hQ : Q) : P → Q := by
/- `intro` lets us introduce assumptions and variables. From a function-y
perspective, we're defining a function from proofs of `P` to proofs of `Q`
and saying "let `hP` be any proof of `P` - we map it to `hQ`." -/
/- (Unimportant remark: `intro` is like moving things before the colon, i.e.
lemmas `one` and `two` are proofs of the same proposition.) -/
lemma two (P Q : Prop) (hQ : Q) (hP : P) : Q := by
#check two -- same output
/- As another example, let's prove transitivity of implication.
There are invisible brackets in the statement of our theorem, because `→`
We want to define a function that eats a proof of "`P` implies `Q`" and spits
out another function: one that eats a proof of "`Q` implies `R`" and spits out
a proof of "`P` implies `R`."
example (P Q R : Prop) : (P → Q) → (Q → R) → (P → R) := by
Next we'll look at `False` and negation statements. `False` is defined to
be a `Prop` with no terms. Meanwhile, negation statements are statements
beginning with `¬`, which you can type with `\not`. Given a proposition `P`,
`¬ P` is defined to mean `P → False`, so it's an implication statement in disguise.
/- In that example we both used and proved a `¬` statement.
Sometimes we also want to use the fact that any statement follows from
`False`. In practice this shows up when proving a proposition `P` by
case-splitting on some condition, since sometimes we can conclude `P` in
a particular case by showing that case can never occur.
To derive another proposition from a proof of `False`, we use the `exfalso` tactic: -/
example (P : Prop) : False → P := by
/- Finally, note that `x ≠ y` is notation for `¬(x = y)`. -/
example (a b : ℕ) : a ≠ b → b ≠ a := by
/- We'll see more tactics for working with negations when we've introduced
more complicated logical connectives to combine them with. -/
Now let's move onto universal quantifiers: `∀` statements, typed with `\all`.
We can treat `∀` statements just like we treated implications, because technically
implication statements are a special case of `∀` statements.
(If an implication `P → Q` is a bit like a function type, say, `ℕ → ℚ`,
then a `∀` statement is like a dependent function type: a type of functions
whose codomain is dependent on the function input.
For example, we can talk about functions that send a natural number `n : ℕ`
to an element of `ℤ/nℤ`; in Lean we can write the type of such functions
via `(n : ℕ) → ZMod n`, `Π (n : ℕ), ZMod n` or even `∀ n : ℕ, ZMod n`.
We can dress a non-dependent function type like `ℕ → ℚ` as a dependent one:
`∀ n : ℕ, ℚ` means the same thing as `ℕ → ℚ`.
Likewise, we can dress up an implication statement as a `∀` statement): -/
#check ∀ (hP : P), Q -- `P → Q : Prop`
/- But quantifying over all proofs of `P` is a bit pointless when they're
Here's a more meaningful `∀` statement:
example : ∀ P : Prop, False → P := by
We proved this earlier, except the `P` was before the colon; this time we
can use `intro` to introduce variables `P : Prop` and `hFalse : False` to
the local context, so indeed, proving a `∀` statement is just like proving
an implication. Let's quantify over some different types this time: -/
def Injective (f : α → β) : Prop :=
example (f : α → β) (g : β → γ) (hf : Injective f) (hg : Injective g) :
unfold Injective at hf hg ⊢
/- If you want to see what's going on better, you can use the `specialize`
tactic to partially apply a local hypothesis to some inputs. -/
example (f : α → β) (g : β → γ) (hf : Injective f) (hg : Injective g) :
specialize hg (f X) (f Y)
## Inductive propositions with 1 constructor:
## Conjunction, bi-implication and the existential quantifier
Now for a different group of similar logical connectives:
`∧` (\and), `↔` (\iff) and `∃` (\exists, except you just have to
type \ex). The previous group were all like function types; this group
correspond to a different kind of type - inductive types. In particular
they're all inductive propositions with 1 constructor, which is why they
behave similarly. It doesn't matter what this means; the important thing
is we can use the same tactics to deal with all 3.
The statements `P ∧ Q` and `P ↔ Q` both represent two pieces of
information, and each side is independent of the other one.
Meanwhile, like `∀`, `∃` is dependent: -/
/- Let `P` be a predicate on `α`: -/
variable (α : Type) (P : α → Prop)
/- (example of a predicate:) -/
def biggerThan10 : ℕ → Prop := by
/- Then `∃` statements look like this: -/
/- Here are some ways to use and prove `∧` statements: -/
example (h : P ∧ Q) : Q ∧ P := by
example (h : P ∧ Q) : Q ∧ P := by
example (h : P ∧ Q) : Q ∧ P := by
/- It's exactly the same story for `↔`: -/
example (h : P ↔ Q) : Q ↔ P := by
example (h : P ↔ Q) : Q ↔ P := by
example (h : P ↔ Q) : Q ↔ P := by
/- However, `↔` leads a double life - it also behaves just like
`=`, meaning we can `rw` `↔` statements the way we can `rw` equalities. -/
example (hPQ : P ↔ Q) (hQR : Q ↔ R) : P ↔ R := by
# Existential quantifiers
/- We can use an `∃` statement by deconstructing it and replacing
`∃ x, P x` with a term `x : α` and a hypothesis `hx : P x`. -/
example (α : Type) (P : α → Prop) (h : ∃ x, P x) : ¬ (∀ x, ¬ P x) := by
example (α : Type) (P Q : α → Prop) (h : ∃ x, P x ∧ Q x) :
rcases h with ⟨x, hPx, hQx⟩
example (α : Type) (P Q : α → Prop) (h : ∃ x, P x ∧ Q x) :
rcases h with ⟨x, hPx, hQx⟩
example (α : Type) (P Q : α → Prop) :
(∃ x, P x ∧ Q x) → ∃ x, Q x ∧ P x := by
As before, the tactics we're using can see underneath definitions
def Surjective {α β : Type} (f : α → β) : Prop :=example {α β γ : Type} (f : α → β) (g : β → γ) (hf : Surjective f) (hg : Surjective g) : Surjective (g ∘ f) := by
/- `rfl` proves definitional equalities; i.e. it succeeds when both
sides are equal by definition. -/
/- We can shorten this using the "`rfl` trick": because `hy` and `hz` are
equalities, if we name them `rfl`, they automatically get rewritten wherever
possible in the local context: -/
example {α β γ : Type} (f : α → β) (g : β → γ) (hf : Surjective f) (hg : Surjective g) : Surjective (g ∘ f) := by
rcases hg x with ⟨y, rfl⟩
rcases hf y with ⟨z, rfl⟩
# Inductive propositions with 2 constructors: Disjunction
Final logical connective: `∨` (type `\or`). This is a little like the
previous group, in that `∨` is an inductive proposition, but instead
of one constructor with 2 pieces of information, `∨` has two constructors:
you can prove `P ∨ Q` either by proving `P` or proving `Q`.
example (h : P ∨ Q) : Q ∨ P := by
/- Now there are 2 goals. -/
/- If you want to use `rintro` here you need to add brackets. -/
example : P ∨ Q → Q ∨ P := by
/- By combining the 2nd group of logical constructions and `∨` we can
start to see the power of `rcases`. -/
/- First of all here's the definition of "divides". Since `↔` behaves
like `=`, `rfl` can also prove this: -/
lemma dvd_def {m n : ℕ} : m ∣ n ↔ ∃ c, n = m * c := byexample {m n k : ℕ} (h : m ∣ n ∨ m ∣ k) : m ∣ n * k := by/- A tactic for next session, but we don't really need it here: -/
rcases h with ⟨a, rfl⟩ | ⟨b, rfl⟩
P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by
P ∨ (Q ∧ R) ↔ (P ∨ Q) ∧ (P ∨ R) := by
example : ¬P → P ∨ Q → Q := by
example : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q := by
/- But to prove the converse we need to use classical logic,
and apply the law of excluded middle: -/
lemma not_not : ¬¬P → P := by
by_cases hP : P -- we case-split on `P ∨ ¬P`
/- The tactic `by_contra` just applies `not_not`: -/
/- You can use `not_not` to prove the following lemma directly.
Alternatively, there are various tactics which use classical logic
example : ¬(P → Q) → P ∧ ¬Q := by
/- `tauto` can prove pretty much everything in this file so far. -/
/- `push_neg` simplifies negation statements by "pushing" the
negation as far inside the statement as possible: -/
example : ¬(P → Q) → P ∧ ¬Q := by
/- We can also `push_neg` at a hypothesis: -/
example (P : α → Prop) (h : ¬∀ x, ¬P x) : ∃ x, P x := by
/- And `push_neg` can also simplify inequalities: -/
example : ¬(∃ n : ℕ, ¬(3 < n) ∧ ¬(n ≤ 5)) := by
/- `contrapose` replaces a `p → q` goal with the contrapositive,
`¬q → ¬p`. `contrapose!` combines this with `push_neg`. -/
example : ¬(P → Q) → P ∧ ¬Q := by
/- Exercise: you can prove this without using classical logic if you're
careful. And then you can delete your proof and replace it with `tauto`. -/
example : ¬(P ↔ ¬P) := by
/- More exercises. You can do them step by step or you can speedrun
them with the tactics in this section. -/
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q := by
example : ¬ (∃ x, ¬ P x) → (∀ x, P x) := by
example : ¬ (∀ x, ¬ P x) → (∃ x, P x) := by
So far we've just applied local hypotheses, but applying or
deconstructing lemmas from the library works in just the same way.
Let's demonstrate this by proving that every nonzero element of a
finite integral domain has an inverse:
example (K : Type) [CommRing K] [IsDomain K] [Finite K]
(x : K) (hx : x ≠ 0) : ∃ y, x * y = 1 := by
/- `set` (or `let`) is like `have` but for data. -/
have hf : Function.Injective f := by
apply mul_left_cancel₀ hx
rcases Finite.surjective_of_injective hf 1 with ⟨y, hy⟩
Given a type `α`, `Set α` is the type of "subsets" of `α`. It's defined
to mean `α → Prop` - i.e. the type of predicates on `α`. To express a
particular set, we can use familiar notation:
{ p | 2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p }def IsPrime (p : ℕ) : Prop :=
2 ≤ p ∧ ∀ m, m ∣ p → m = 1 ∨ m = p
example : IsPrime = Primes := by
example (x : ℕ) : IsPrime x ↔ x ∈ Primes := by
/- You can also express a set with prescribed elements: -/
def mySet : Set ℕ := {1, 2, 3, 4}Let's prove some facts about sets. We state some lemmas below which are
all true by definition, so a lot of the time you don't really need to use them,
but you can if you like. Remember that they're `↔` statements, so you can
lemma not_mem_def {S : Set α} (x : α) : x ∉ S ↔ ¬(x ∈ S) := by rfllemma subset_def {S T : Set α} : S ⊆ T ↔ ∀ x, x ∈ S → x ∈ T := by rfllemma ssubset_def {S T : Set α} : (S ⊂ T) ↔ (S ⊆ T ∧ ¬T ⊆ S) := by rfl
lemma mem_compl_def {S : Set α} (x : α) :lemma mem_inter_def {S T : Set α} (x : α) : x ∈ S ∩ T ↔ x ∈ S ∧ x ∈ T := by rfl
lemma mem_union_def {S T : Set α} (x : α) : x ∈ S ∪ T ↔ x ∈ S ∨ x ∈ T := by rfl
lemma mem_diff_def {S T : Set α} (x : α) : x ∈ S \ T ↔ x ∈ S ∧ x ∉ T := by rfl
lemma mem_image_def {α β : Type} {f : α → β} {S : Set α} (x : β) : x ∈ f '' S ↔ ∃ y ∈ S, f y = x := by rfl
lemma mem_preimage_def {α β : Type} {f : α → β} {S : Set β} (x : α) : x ∈ f ⁻¹' S ↔ f x ∈ S := by rfl
lemma mem_singleton_def {x y : α} : x ∈ ({y} : Set α) ↔ x = y := bylemma mem_empty_def {x : α} : x ∈ (∅ : Set α) ↔ False := bylemma mem_univ_iff {x : α} : x ∈ Set.univ ↔ True := by/- Note that the `ext` tactic allows you to prove 2 sets are
equal by proving they have the same elements: -/
example {S T : Set α} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T := by/- The `ext` tactic also allows you to prove 2 functions are equal
by checking they're the same on every element: -/
example {f g : α → β} (h : ∀ x, f x = g x) : f = g := by/- The other direction can be useful too. -/
lemma ext_iff {S T : Set α} : S = T ↔ ∀ x, x ∈ S ↔ x ∈ T := by
variable {α β : Type} {f : α → β} {S T U : Set α}lemma inter_union_distrib_left : S ∩ (T ∪ U) = S ∩ T ∪ S ∩ U := by
lemma union_diff_inter : (S ∪ T) \ (S ∩ T) = S \ T ∪ T \ S := by
lemma image_subset_iff {T : Set β} : f '' S ⊆ T ↔ S ⊆ f ⁻¹' T := bylemma image_eq_empty_iff : f '' S = ∅ ↔ S = ∅ := by
lemma image_singleton {x : α} : f '' {x} = {f x} := bylemma image_union : f '' (S ∪ T) = f '' S ∪ f '' T := by
lemma image_diff_of_injective (hf : Injective f) :
f '' (S \ T) = f '' S \ f '' T := by
lemma image_inter_of_injective (hf : Injective f) :
f '' (S ∩ T) = f '' S ∩ f '' T := by
lemma image_inter_preimage {T : Set β} : f '' (S ∩ f ⁻¹' T) = f '' S ∩ T := by
lemma compl_compl : Sᶜᶜ = S := by
lemma compl_compl_inter_compl :
lemma const_apply {x : α} {y : β} : Function.const α y x = y := rfl
/- Hint: the `trivial` tactic can prove the goal `True`. -/
lemma exists_eq_const_of_preimage_singleton
(h : ∃ b : β, True) {f : α → β} (hf : ∀ b : β, f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = Set.univ) : ∃ b, f = Function.const α b := by
Here's something Timothy Gowers tweeted recently.
variable {α β : Type} (f : α → β)def Bijective : Prop := Injective f ∧ Surjective f
example : Bijective f ↔ ∀ S : Set α, (f '' S)ᶜ = f '' Sᶜ := by
