Lecture 4.3: Mathematics — Rational and Real Numbers

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

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 ℚ:

Use (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

Real numbers

ℚ 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

Cauchy sequences

ℚ cannot represent √2, but it can approximate it:

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

Constructing `ℝ`

ℝ 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

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