Today we will go through the construction of ℚ
and ℝ
as quotient types
A similar construction will be shown in the next lecture for the p-adic integers
Rational numbers can be expressed as n / d
where n
, d : ℤ
, representing the unique solution of x
in the equation x * d = n
for d ≠ 0
We use the following general idea to construct new types with specific properties:
Create a new type to "syntactically" represent all elements
Quotient this representation, equating syntactic elements that should be considered equal
Define functions by lifting functions from the syntactic representation and prove that they respect the quotient relation
For ℚ
:
We simply introduce a dependent triple (n : ℤ, d : ℤ, hd : d ≠ 0)
to represent n / d
As quotient relation, we use n / d ≈ n' / d' := n * d' = n' * d
Define 0 := 0 / 1
, 1 := 1 / 1
, and addition, multiplication, and order:
n / d + n' / d' := (n * d' + n' * d) / (d * d')
(n / d) * (n' / d') := (n * n') / (d * d')
n / d ≤ n' / d' := n * d' ≤ n' * d
and show that they respect the relation ≈
Since these functions respect ≈
, we can lift
them into functions on ℚ
Now we can prove that ℚ
forms a linear_orderd_field
Alternative (extreme) definitions of ℚ
:
(n : ℤ, d : ℤ, hd : 0 < d, h : coprime n d)
, where coprime n d
says that n
and d
do not have a common divisor (except 1
and -1
)This is the definition used in mathlib
Advantages: no quotient required; more efficient computation; more theorems are definitional equalities
Disadvantage: more complicated function definitions
Define all elements syntactically, including the desired operations:
inductive pre_ℚ : Type | zero, one : pre_ℚ | add, sub, mul, div : pre_ℚ → pre_ℚ → pre_ℚ
Define ≈
to include congruence rules and to follow the field
equations:
inductive ≈ : pre_ℚ → pre_ℚ → Prop
| add_congr {a b c d : pre_ℚ} : a ≈ b → c ≈ d → add a c ≈ add b d
| add_comm {a b : pre_ℚ} : add a b ≈ add b a
| add_assoc {a b c : pre_ℚ} : add a (add b c) ≈ add (add a b) c
...
Advantages: does not require ℤ
; easy to prove the field
equations; general recipe reusable for other algebraic constructions (e.g. free monoids, free groups)
Disadvantage: the definition of orders and lemmas about them are more complicated
ℚ
is incomplete: the sets {x ∈ ℚ | x² < 2}
and {x ∈ ℚ | x² > 2}
partition ℚ
, but the supremum or infimum is not in ℚ
The sequence of rationals
1, 1.4, 1.41, 1.414, 1.4142, 1.41421, 1.414213, 1.4142135, 1.41421356, ...
does not converge to a rational number
There are different ways to construct the real numbers:
Cauchy sequences
Dedekind cuts: r : ℝ
is represented essentially as {x : ℚ | x < r}
, i.e. as values of type set ℚ
corresponding to sets that are nonempty, bounded to the right, and downwards closed
Binary sequences ℕ → bool
for the interval [0, 1]
Cauchy sequences are the easiest approach, especially if ℚ
is already available
We follow the general recipe described above, using Cauchy sequence as the "syntactic" concept
ℚ
cannot represent √2, but it can approximate it:
1
1.4
1.41
1.414
1.4142
1.41421
1.414213
1.4142135
1.41421356
...
One way to approximate the missing numbers is to use Cauchy sequences
A sequence f : ℕ → α
is Cauchy if the distance between two elements gets arbitrarily small:
cauchy f := ∀ε > 0, ∃N, ∀n ≥ N, |f N - f n| < ε
where α
is equipped with an "absolute value" operator | | : α → ℚ
To construct ℝ
, α
will be ℚ
It is easy to define the operations on Cauchy sequences:
0 := λn, 0
1 := λn, 1
f + g := λn, f n + g n
f * g := λn, f n * g n
The definitions requires us to prove that when f
and g
form a Cauchy sequence, then f + g
and f * g
form Cauchy sequences
However, two different Cauchy sequences can approximate the same point:
1 2
1.4 1.5
1.41 1.42
1.414 1.415
1.4142 1.4143
1.41421 1.41422
1.414213 1.414214
1.4142135 1.4142136
1.41421356 1.41421357
... ...
Both converge towards √2
Two sequences are equivalent if they approximate the same point:
equiv f g := ∀ε > 0, ∃N, ∀m ≥ N, ∀n ≥ N, |f m - g n| < ε
Cauchy sequences also have a order:
0 < f := ∃ε > 0, ∃N, ∀m ≥ N, ε < f m
This is all we need since f < g ↔ 0 < g - f
ℝ
ℝ
is defined as the quotient of Cauchy sequences on ℚ
with respect to the relation equiv
To define the ordered field structure on ℝ
, all operations are lifted from Cauchy sequences
Unlike ℚ
, ℝ
is complete—i.e. all Cauchy sequence on ℝ
have a limit:
∀f : ℕ → ℝ, cauchy f → ∃x, ∀ε > 0, ∃N, ∀m ≥ N, |f m - x| < ε
Analysis does not stop with introducing ℝ
mathlib
has more material on analysis:
topological and metric spaces
linear algebra with modules and vector spaces
normed vector spaces
measures and simple integrals
But one of the more important concepts, derivatives, is still missing
In the next lecture, we will hear from Robert Y. Lewis about a related topic from number theory: p-adic numbers