Brent Yorgey: Proving the Fundamental Theorem of Arithmetic in Agda

tl;dr: This is a fully commentated, from-scratch proof of the Fundamental Theorem of Arithmetic in Agda, intended for those who already know a bit of Agda but might benefit from reading and working through a larger example. See the Introduction and the Table of Contents below for more details.

Introduction

Earlier this spring, I was idly brainstorming potential final projects for my Functional Programming students. Having just taught my Discrete Math students the Fundamental Theorem of Arithmetic, I wondered whether formalizingI mean formalizing it from scratch: of course, the FTA is already in the Agda standard library. As I later learned, it was added to the standard library by Nathan van Doorn, aka Taneb. it in Agda could make a nice project.

So I decided to spend about an hour trying to prove it in Agda, to gauge the level of the project. At the end of an hour, I had learned two things: (1) proving the Fundamental Theorem of Arithmetic is not an appropriate project for my students (who had only had a few weeks’ practice with Agda); (2) I was not going to be able to stop until I finished the proof myself!

Over the next week or so, I finished the proof completely from scratch—without using anything from the standard library, and without looking up any reference material. I based it only on my experience in Agda, knowledge of the relevant proofs on an informal level, and Agda techniques I’ve picked up along the way (from e.g. Conor McBride, Jacques Carette, colleagues at Penn, and elsewhere).

I decided to publish the proof, with extra commentary, in the hopes that it can be useful as an intermediate-level reference. That is, perhaps you’ve learned some basic Agda (if not, I suggest this tutorial to start) and have some basic familiarity with the Curry-Howard correspondence, but would benefit from seeing an example of a fully worked out, medium-sized proof.Another good source of information along these lines is this post by Jesper Cockx. The resulting blog post is extremely long, but I make no apologies for that—if you want an entertaining 5-minute read, you should look elsewhere!

The entire blog post and proof is available as a literate Agda document. Even better, I have also published another version of this blog post with holes in place of almost all the proofs. For a maximal learning experience, I suggest downloading it and trying to fill in the holes yourself as you go along.

Below is a table of contents. Depending on your background, you may of course choose to skip some sections. For example, if you have already had a good deal of practice dealing with basic natural number arithmetic, equality, and inequality in Agda, you might wish to skip over those sections.

Table of Contents

• Introduction
• (Half of) The Fundamental Theorem of Arithmetic (Constructively)
• Preliminaries
• Basic logic
• Equality
• Natural numbers
  • No confusion
  • Decidable equality
• Addition
• Multiplication
• Inequality
  • Relationships among equality and inequality
  • Arithmetic and inequality
• Divisibility, primes, and composites
  • Nontrivial divisors come in pairs
• Division
• Absolute difference
• Quotient and remainder are unique
• The division algorithm, take 1
  • Construct the evidence you would like to pattern-match on
• Well-founded induction
  • Accessibility
  • Well-founded induction, defined
  • Less-than is well-founded
• The division algorithm
• Primality testing
  • Counting up
  • Primality testing by trial division
• Lists
• The Fundamental Theorem of Arithmetic
• Further Directions

(Half of) The Fundamental Theorem of Arithmetic (Constructively)

The Fundamental Theorem of Arithmetic (FTA for short) states that any natural number \(n \geq 1\) can be written as a product of zero or more primes, and moreover that this product is unique up to permutation.

For now, we are only going to prove the existence part (I may write another blog post with the uniqueness proof later). Since a constructive existence proof is really an algorithm for constructing the thing that is claimed to exist, this can also be seen as a formally verified factorization program: put any number in, get a prime factorization out. Writing a prime factorization program is not hard, of course; it’s the formal verification part that is interesting!

Stop! Before reading on, if you want to get the most out of this tutorial, I strongly recommend downloading the version with holes and trying to complete as many of the proofs as you can before reading mine!

Preliminaries

We will often make use of A and B to stand for arbitrary sets/types, so we use a variable declaration to tell Agda that it should implicitly quantify them whenever they show up as free variables. That way we don’t have to write {A B : Set} → ... all the time.

Basic logic

Since we’re building this completely from scratch, we start with some types to represent basic logical building blocks (via the Curry-Howard correspondence). First, the “top” type ⊤ to stand for truth, i.e. a proposition with trivial evidence:

data ⊤ : Set where
  tt : ⊤

tt is declared to be the one and only value of type ⊤.

Note that some things we define here—such as ⊤—will have the same names as they do in the Agda standard library. However, many things won’t, since I either didn’t know the standard name and made up my own, or (in a few cases) did know the standard name but didn’t like it, and made up my own anyway.

Next, the “bottom” type ⊥ with no constructors, representing falsity, along with a corresponding elimination principle, absurd. The elimination principle says that anything follows from ⊥ (“ex falso quodlibet”), and is implemented using Agda’s absurd pattern, written (). If Agda can tell that there are no possible constructors which could give rise to a value of a certain type, we can pattern-match on it with (), and are absolved of providing a right-hand side for the definition in that case.

data ⊥ : Set where

absurd : ⊥ → A
absurd ()

We can now define negation as an implication to ⊥.

¬ : Set → Set
¬ P = P → ⊥

Dependent pairs are next: a pair of values where the type of the second component can depend on the value of the first. That is, a value of type Σ A B is a value a of type A paired with a value of type B a. Via Curry-Howard, this is used to represent existential quantification: a (constructive) proof of \(\exists a : A.\; B(a)\) is a value \(a\) of type \(A\) (the witness) paired with a proof that \(a\) has property \(B\) (i.e. a value of type \(B(a)\)).

infixr 1 _,_
data Σ (A : Set) (B : A → Set) : Set where
  _,_ : (a : A) → B a → Σ A B

We also define a projection function (we only end up needing fst; defining snd is left as an exercise for the readerThe definition of snd is trivial; writing down its type is a worthwhile exercise.), along with a type of non-dependent pairs, corresponding to logical conjunction (and).

fst : ∀ {A B} → Σ A B → A
fst (a , _) = a

infixr 3 _×_
_×_ : (A B : Set) → Set
A × B = Σ A (λ _ → B)

Finally, we define a disjoint (tagged) union type corresponding to logical disjunction (or).

infixr 2 _⊎_
data _⊎_ (A B : Set) : Set where
  inj₁ : A → A ⊎ B
  inj₂ : B → A ⊎ B

Equality

Next, we write down the standard equality (aka identity, aka path) type, with a single constructor refl that witnesses when its two arguments are identical.It still seems somewhat magical to me that this seemingly too-simple definition encapsulates everything we want in an equality relation (well, almost everything). We also define a convenient synonym for inequality.

infix 4 _≡_
data _≡_ (a : A) : A → Set where
  refl : a ≡ a

_≢_ : A → A → Set
x ≢ y = ¬ (x ≡ y)

Besides reflexivity, equality enjoys various properties that we will need: symmetry, transitivity, and congruence (i.e., we can apply any function to both sides of an equation).

sym : {x y : A} → x ≡ y → y ≡ x
sym refl = refl

trans : {x y z : A} → x ≡ y → y ≡ z → x ≡ z
trans refl y≡z = y≡z

cong : (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
cong _ refl = refl

Since we will spend a good amount of time reasoning about equality, it is worthwhile building up some machinery for writing more readable equality proofs. Instead of writing, say,

trans p (trans q (trans (sym r) s))

we will be able to instead write equality proofs like so:

begin
  v      ≡[ p ⟩≡
  w      ≡[ q ⟩≡
  x      ≡⟨ r ]≡
  y      ≡[ s ⟩≡
  z      ∎

The intention is that this proof shows v ≡ z, by first using p to show that v ≡ w, then q to show w ≡ x, and so on. This notation is one of my favorite applications of Agda’s mixfix operator syntax, and has several benefits:

• We can avoid nested parentheses when chaining uses of transitivity.
• We can automatically apply symmetry by using a left-pointing instead of right-pointing operator.
• We get to explicitly mention (and have Agda check for us) all the intermediate values, making it easier to write the proof incrementally, and much easier for humans to read.

This is one of the places where I deliberately chose different operator names than the standard library, which uses _≡⟨_⟩_ and _≡⟨_⟨_. The operator names I decided to use are inspired by Conor McBride. I just like the way they look better.

infix 1 begin_
begin_ : {x y : A} → x ≡ y → x ≡ y
begin x≡y = x≡y

infixr 2 _≡[_⟩≡_
_≡[_⟩≡_ : (x : A) → {y z : A} → (x ≡ y) → (y ≡ z) → (x ≡ z)
_ ≡[ x≡y ⟩≡ y≡z = trans x≡y y≡z

infixr 2 _≡⟨_]≡_
_≡⟨_]≡_ : (x : A) → {y z : A} → (y ≡ x) → (y ≡ z) → (x ≡ z)
_ ≡⟨ y≡x ]≡ y≡z = trans (sym y≡x) y≡z

infixr 5 _∎
_∎ : (x : A) → x ≡ x
_ ∎ = refl

Finally, a few Applicative-like operators for more conveniently writing common forms of congruence. For example, instead of writing cong f x≡y, we can write f $≡ x≡y; or to use congruence on both arguments of a two-place function at once, we can write f $≡ x≡y ≡$≡ z≡w. (These operators were also inspired by Conor.)

infixl 4 _$≡_
_$≡_ : (f : A → B) → {x y : A} → x ≡ y → f x ≡ f y
f $≡ x≡y = cong f x≡y

infixl 4 _≡$_
_≡$_ : {f g : A → B} → f ≡ g → (x : A) → f x ≡ g x
f≡g ≡$ x = cong (λ h → h x) f≡g

infixl 4 _≡$≡_
_≡$≡_ : {f g : A → B} → f ≡ g → {x y : A} → x ≡ y → f x ≡ g y
f≡g ≡$≡ x≡y = trans (f≡g ≡$ _) (_ $≡ x≡y)

Natural numbers

Of course, we will need a type to represent the natural numbers. We can also tell Agda that our natural number type should correspond to its built-in notion of natural numbers, so we can use numeric literals like 2 : ℕ instead of having to write suc (suc zero).

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

No confusion

For our natural number type—and often, for any algebraic data type—we need to know that the constructors are

1. disjoint, meaning that different constructors always generate different values (so it’s a contradiction to have an equality between values built with different constructors); and
2. injective, meaning that if we have an equality between values built with the same constructor, we can decompose it into equalities between the components.

We can prove both of these simultaneously using a property called “no confusion”. This property and its name is well-known in the literature; for example, see McBridge or Cornes + Terrasse.

For natural numbers m and n, the type NoConf m n should be thought of as the type of evidence that m ≡ n, based on looking at the top-level constructors of m and n. If m and n have different constructors, then no evidence can possibly show that they are equal, so NoConf m n = ⊥ in that case. If m and n are both zero, then they are evidently equal, so NoConf 0 0 = ⊤. Otherwise, if m and n are both successors, NoConf m n reduces to a proof of equality between their predecessors.

NoConf : ℕ → ℕ → Set
NoConf zero zero = ⊤
NoConf zero (suc n) = ⊥
NoConf (suc m) zero = ⊥
NoConf (suc m) (suc n) = m ≡ n

Now we can prove the no confusion lemma for our natural number type, which says that NoConf m n always holds whenever m ≡ n. Since m ≡ n, we only have to deal with the cases when m and n are both zero or both a successor—but this also justifies assigning a type of ⊥ to the cases when the constructors do not match. noConf can therefore be used to strip suc from both sides of an equation, or to derive a contradiction when we have an equation between non-matching constructors.

noConf : {m n : ℕ} → m ≡ n → NoConf m n
noConf {zero} refl = tt
noConf {suc m} refl = refl

As an aside, this definition of the no confusion property uses a technique I like: defining a type starting with a capital letter, then defining a term that returns that type starting with a lowercase letter. This pattern will come up again later. Sometimes we define named types in this way just for convenience, say, to be able to refer to the type multiple times in a concise way; or, as in the above case, sometimes the type is actually defined via some nontrivial computation.

Decidable equality

We can now show how to decide equality of natural numbers. We first define a simple type representing decidability in general: Dec P represents either a proof of P, or a proof of ¬ P.You may be aware that the law of excluded middle, which says that \(P \lor \neg P\) for all propositions \(P\), is rejected in constructive logic. However, even though \(P \lor \neg P\) does not hold for all \(P\), it can still hold for certain specific propositions. Propositions \(P\) for which \(P \lor \neg P\) holds constructively are called decidable. (The standard library version is much more sophisticated, but this simple version will do just fine.)

data Dec (P : Set) : Set where
  yes : P → Dec P
  no : ¬ P → Dec P

We can then prove that for any natural numbers x and y, we can decide whether x ≡ y. Notice the several different uses of the no confusion lemma: two to handle impossible situations, and one to strip suc off both sides of an equality.

_≟_ : (x y : ℕ) → Dec (x ≡ y)
zero ≟ zero = yes refl
zero ≟ suc y = no noConf
suc x ≟ zero = no noConf
suc x ≟ suc y with x ≟ y
... | yes x≡y = yes (suc $≡ x≡y)
... | no x≢y = no (λ sx≡sy → x≢y (noConf sx≡sy))

Addition

We next turn to defining addition (by pattern-matching on the left-hand argument), along with several properties of addition we will need: zero is a right identity for addition; we can pull out a suc from the right-hand argument; and addition is commutative, associative, and left-cancellable.

infixl 6 _+_
_+_ : ℕ → ℕ → ℕ
zero + y = y
suc x + y = suc (x + y)

_+0 : (n : ℕ) → (n + 0 ≡ n)
zero +0 = refl
(suc n) +0 = suc $≡ (n +0)

_+suc_ : (x y : ℕ) → (x + suc y) ≡ suc (x + y)
zero +suc y = refl
(suc x) +suc y = suc $≡ (x +suc y)

+-comm : (x y : ℕ) → x + y ≡ y + x
+-comm zero y = sym (y +0)
+-comm (suc x) y = trans (suc $≡ (+-comm x y)) (sym (y +suc x))

+-assoc : (x y z : ℕ) → (x + y) + z ≡ x + (y + z)
+-assoc zero y z = refl
+-assoc (suc x) y z = suc $≡ (+-assoc x y z)

+-cancelˡ : (x y z : ℕ) → x + y ≡ x + z → y ≡ z
+-cancelˡ zero y z x+y≡x+z = x+y≡x+z
+-cancelˡ (suc x) y z x+y≡x+z = +-cancelˡ x y z (noConf x+y≡x+z)

Multiplication

Multiplication is next: we start by defining the multiplication operation (by pattern-matching on the left-hand argument) and proving a few lemmas about multiplying by known arguments on the right. The proof of *suc is the most involved proof we have seen yet, but it ultimately just comes down to algebra, and we can make good use of our notation for writing chained equality proofs.

infixl 7 _*_
_*_ : ℕ → ℕ → ℕ
zero * y = zero
suc x * y = y + x * y

_*0 : (n : ℕ) → (n * 0 ≡ 0)
zero *0 = refl
(suc n) *0 = n *0

_*1 : (n : ℕ) → (n * 1 ≡ n)
0 *1 = refl
(suc n) *1 = suc $≡ (n *1)

_*suc_ : (x y : ℕ) → (x * suc y ≡ x + x * y)
zero *suc y = refl
(suc x) *suc y = suc $≡ (
  begin
  y + x * suc y               ≡[ (y +_) $≡ (x *suc y) ⟩≡
  y + (x + x * y)             ≡⟨ +-assoc y x (x * y) ]≡
  (y + x) + x * y             ≡[ _+_ $≡ +-comm y x ≡$ x * y ⟩≡
  (x + y) + x * y             ≡[ +-assoc x _ _ ⟩≡
  x + (y + x * y)             ∎)

We prove some standard properties of multiplication: commutativity, distributivity over addition, associativity. Again, the proofs mostly consist of a whole bunch of algebra, using the special notation for building chained equality proofs.

*-comm : (x y : ℕ) → x * y ≡ y * x
*-comm zero y = sym (y *0)
*-comm (suc x) y = begin
  y + x * y                   ≡[ y +_ $≡ *-comm x y ⟩≡
  y + y * x                   ≡⟨ y *suc x ]≡
  y * suc x                   ∎

*-distribˡ : (x y z : ℕ) → x * (y + z) ≡ x * y + x * z
*-distribˡ zero y z = refl
*-distribˡ (suc x) y z = begin
  y + z + x * (y + z)         ≡[ (y + z) +_ $≡ *-distribˡ x y z ⟩≡
  y + z + (x * y + x * z)     ≡[ +-assoc y _ _ ⟩≡
  y + (z + (x * y + x * z))   ≡⟨ y +_ $≡ +-assoc z _ _ ]≡
  y + ((z + x * y) + x * z)   ≡[ y +_ $≡ (_+_ $≡ +-comm z _ ≡$ x * z) ⟩≡
  y + ((x * y + z) + x * z)   ≡[ y +_ $≡ +-assoc (x * y) _ _ ⟩≡
  y + (x * y + (z + x * z))   ≡⟨ +-assoc y _ _ ]≡
  y + x * y + (z + x * z)     ∎

*-distribʳ : (x y z : ℕ) → (x + y) * z ≡ x * z + y * z
*-distribʳ x y z = begin
  (x + y) * z                 ≡[ *-comm (x + y) _ ⟩≡
  z * (x + y)                 ≡[ *-distribˡ z _ _ ⟩≡
  z * x + z * y               ≡[ _+_ $≡ *-comm z _ ≡$≡ *-comm z _ ⟩≡
  x * z + y * z               ∎

*-assoc : (x y z : ℕ) → (x * y) * z ≡ x * (y * z)
*-assoc zero y z = refl
*-assoc (suc x) y z = begin
  (y + x * y) * z             ≡[ *-distribʳ y _ _ ⟩≡
  y * z + (x * y) * z         ≡[ y * z +_ $≡ *-assoc x _ _ ⟩≡
  y * z + x * (y * z)         ∎

Finally, we prove that multiplication is left-cancellative. This proof is somewhat tricky—in the case that x, y, and z are all successors, we need to use the induction hypothesis (i.e. a recursive call to *-cancelˡ) on x and the predecessors of y and z, using the fact that + is left-cancellative to construct the required input equality.

*-cancelˡ : (x y z : ℕ) → (0 ≢ x) → x * y ≡ x * z → y ≡ z
*-cancelˡ zero y z x≢0 xy≡xz = absurd (x≢0 refl)
*-cancelˡ (suc x) zero zero x≢0 xy≡xz = refl
*-cancelˡ (suc x) zero (suc z) x≢0 xy≡xz = absurd (noConf (trans (sym (x *0)) xy≡xz))
*-cancelˡ (suc x) (suc y) zero x≢0 xy≡xz = absurd (noConf (trans xy≡xz (x *0)))
*-cancelˡ (suc x) (suc y) (suc z) x≢0 xy≡xz = suc $≡
  ( *-cancelˡ (suc x) y z x≢0
    ( +-cancelˡ (suc x) (suc x * y) (suc x * z)
      ( begin
          suc x + suc x * y   ≡⟨ (suc x) *suc y ]≡
          suc x * suc y       ≡[ xy≡xz ⟩≡
          suc x * suc z       ≡[ (suc x) *suc z ⟩≡
          suc x + suc x * z   ∎
      )
    )
  )

Inequality

Next, we give a standard definition of the “less than or equal to” relation on natural numbers. Note that the structure of a proof of \(x \leq y\) exactly matches the structure of \(x\) itself.

data _≤_ : ℕ → ℕ → Set where
  zle : {n : ℕ} → zero ≤ n
  sle : {m n : ℕ} → m ≤ n → suc m ≤ suc n

We also prove some standard properties of \(\leq\): it is reflexive and transitive, and is related to suc in various ways.

≤-refl : {m : ℕ} → m ≤ m
≤-refl {zero} = zle
≤-refl {suc m} = sle ≤-refl

≤-trans : {x y z : ℕ} → x ≤ y → y ≤ z → x ≤ z
≤-trans zle y≤z = zle
≤-trans (sle x≤y) (sle y≤z) = sle (≤-trans x≤y y≤z)

≤-sucr : {m n : ℕ} → m ≤ n → m ≤ suc n
≤-sucr zle = zle
≤-sucr (sle m≤n) = sle (≤-sucr m≤n)

≤-sucl : {m n : ℕ} → suc m ≤ n → m ≤ n
≤-sucl (sle sm≤n) = ≤-sucr sm≤n

≤-pred : {x y : ℕ} → suc x ≤ suc y → x ≤ y
≤-pred (sle sx≤sy) = sx≤sy

For convenience, we define \(<\) in terms of \(\leq\), and prove a few properties: any number is less than its successor, and \(<\) is transitive and non-reflexive.

_<_ : ℕ → ℕ → Set
x < y = suc x ≤ y

_<suc : (x : ℕ) → x < suc x
_<suc zero = sle zle
_<suc (suc x) = sle (x <suc)

<-trans : {x y z : ℕ} → x < y → y < z → x < z
<-trans (sle x<y) (sle y<z) = ≤-trans (sle x<y) (≤-sucr y<z)

x≮x : {x : ℕ} → ¬ (x < x)
x≮x {zero} = λ ()
x≮x {suc x} = λ { (sle x<x) → x≮x x<x}

Relationships among equality and inequality

Of course, equality, \(<\) and \(\leq\) have various relationships that we will need. First, equality implies \(\leq\).

≡→≤ : {x y : ℕ} → x ≡ y → x ≤ y
≡→≤ refl = ≤-refl

Next, \(x < y\) implies that \(x\) and \(y\) are not related by \(\equiv\) or \(\geq\). The first lemma in particular—that \(<\) implies \(\not\equiv\)—gets used quite a bit. Note that it can be read in two equivalent ways: on the surface, it is a way to turn a proof of \(x < y\) into a proof of \(x \not\equiv y\); but since \(x \not\equiv y\) is really an abbreviation for \((x \equiv y) \to \bot\), it can be used to derive a contradiction if we have proofs that \(x < y\) and also \(x \equiv y\).

<→≢ : {x y : ℕ} → x < y → x ≢ y
<→≢ x<y refl = x≮x x<y

<→≱ : {x y : ℕ} → x < y → ¬ (y ≤ x)
<→≱ (sle x<y) (sle y≤x) = <→≱ x<y y≤x

If \(x \leq y\) but they are not equal, then \(x < y\).

≤≢→< : {x y : ℕ} → x ≤ y → x ≢ y → x < y
≤≢→< {y = zero} zle x≢y = absurd (x≢y refl)
≤≢→< {y = suc y} zle x≢y = sle zle
≤≢→< (sle x≤y) x≢y = sle (≤≢→< x≤y (λ m≡n → x≢y (suc $≡ m≡n)))

We will need a form of transitivity that says if \(x \leq y\) and \(y < z\), then \(x < z\), as well as the other way around.

≤-<-trans : {x y z : ℕ} → x ≤ y → y < z → x < z
≤-<-trans x≤y (sle y<z) = ≤-trans (sle x≤y) (sle y<z)

<-≤-trans : {x y z : ℕ} → x < y → y ≤ z → x < z
<-≤-trans (sle x<y) y≤z = ≤-trans (sle x<y) y≤z

Finally, a very specific lemma we will need: if a number is not equal to either 0 or 1, then it must be greater than or equal to 2.

¬01-is-≥2 : (a : ℕ) → (a ≢ 0) → (a ≢ 1) → (2 ≤ a)
¬01-is-≥2 zero a≢0 a≢1 = absurd (a≢0 refl)
¬01-is-≥2 (suc zero) a≢0 a≢1 = absurd (a≢1 refl)
¬01-is-≥2 (suc (suc a)) a≢0 a≢1 = sle (sle zle)

Arithmetic and inequality

The last lemmas we need relate arithmetic operations and inequality. First, adding and multiplying cannot make anything smaller (unless we multiply by zero, of course).

≤+ : {x y : ℕ} → x ≤ (x + y)
≤+ {zero} = zle
≤+ {suc x} = sle ≤+

≤* : {x y : ℕ} → (x ≢ 0) → y ≤ (x * y)
≤* {zero} x≢0 = absurd (x≢0 refl)
≤* {suc x} x≢0 = ≤+

As a result, if we know that one thing is equal to a sum or product of other things, we can conclude something about their relative sizes.

+→≤ : {x y z : ℕ} → x + y ≡ z → x ≤ z
+→≤ refl = ≤+

+→< : {x y z : ℕ} → 0 < y → x + y ≡ z → x < z
+→< {x} {suc y} _ x+y≡z = +→≤ (trans (sym (x +suc y)) x+y≡z)

*→≤ : {x y z : ℕ} → (y ≢ 0) → y * x ≡ z → x ≤ z
*→≤ {x} {y} y≢0 refl = ≤* y≢0

Divisibility, primes, and composites

With the preliminaries out of the way, we can finally get on with the meat of the problem—and we finally get to make use of a dependent pair! A constructive proof that a divides b is a specific natural number witness k, along with a proof that k * a ≡ b.

_∣_ : ℕ → ℕ → Set
a ∣ b = Σ ℕ (λ k → k * a ≡ b)

Proofs of divisibility are unique—that is, for given \(a\) and \(b\) there is at most one value of \(k\) such that \(ka = b\). We won’t need this, but it follows easily from the fact that multiplication is cancellative. More interesting is the fact that divisibility is decidable—that is, for given numbers \(a\) and \(b\) we can calculate either a proof that \(a \mid b\), or a proof that \(\neg (a \mid b)\). This will play a starring role later on—to factor a number we need to be able to try potential divisors and find out whether they work—but proving it is not easy! It will take us several hundred more lines of Agda to get there.

In any case, using this notion of divisibility, we can now define prime and composite numbers. A number \(n\) is defined to be prime if it is at least two, and every \(2 \leq d < n\) does not divide \(n\).

Prime : ℕ → Set
Prime n = (2 ≤ n) × (∀ (d : ℕ) → (d < n) → (2 ≤ d) → ¬ (d ∣ n))

One could equivalently define primality by saying that any divisor of \(n\) must be equal to \(1\) or \(n\); I just decided I liked this formulation better, especially because it directly matches up with the way we will test a number for primality later.

A composite number is one that has a nontrivial divisor—that is, a number \(d\) such that \(2 \leq d < n\) and \(d\) divides \(n\).Note that we could easily prove that if \(n\) is prime then \(n\) is not composite, and likewise if \(n\) is composite then it is not prime, but we won’t end up needing these lemmas.

Composite : ℕ → Set
Composite n = Σ ℕ (λ d → 2 ≤ d × d < n × d ∣ n)

Unlike proofs of divisibility, proofs of Composite n are not unique. For example, we could prove Composite 12 by showing that \(2\) is a nontrivial divisor of \(12\), or by showing that \(3\) is. Although this does not matter from a purely logical point of view, it matters computationally; in general, we care which specific proof of Composite n we have.

Nontrivial divisors come in pairs

Before moving on to other things, we will prove a lemma about composite numbers. If \(n\) is composite, by definition it has a nontrivial divisor \(a\); but this means it must also have a second nontrivial divisor \(b\) such that \(ab = n\). This fact seems almost trivial to us. Indeed, it’s easy to show that if \(n\) has a divisor \(a\), then it must have another divisor \(b\) such that \(ab = n\). The tricky part is showing that if \(a\) is a nontrivial divisor, then \(b\) is also nontrivial. The proof relies on much of the infrastructure we have built up about natural numbers, multiplication, and inequality.

First, we define a type representing two factors of a number \(n\): a pair of proofs that \(n\) is composite (i.e. two nontrivial divisors of \(n\)), along with a proof that the product of those divisors is \(n\).

FactorsOf : ℕ → Set
FactorsOf n = Σ (Composite n × Composite n) (λ {(f₁ , f₂) → fst f₁ * fst f₂ ≡ n})

Now, we prove that if \(n\) is composite, then it has two nontrivial factors. We begin by pattern-matching on the proof that \(n\) is composite, which consists of a divisor \(a\), evidence that \(a\) is nontrivial (i.e. \(2 \leq a\) and \(a < n\)), and a proof that \(a\) is a divisor of \(n\), which itself consists of a number \(b\) paired with a proof that \(ba = n\).

factorsOf : (n : ℕ) → Composite n → FactorsOf n
factorsOf n (a , 2≤a , a<n , b , ba≡n) =

To construct the proof of FactorsOf n, we need two proofs of Composite n along with a proof that the product of the two divisors is \(n\). We already have a proof that \(ba = n\), so we use that, with \(a\) as the second divisor (replicating the corresponding proof of Composite n), and \(b\) as the first. Proving that \(b\) is a divisor of \(n\) is easy: \(a\) is the witness, and proving that \(ab = n\) is easy since we already know \(ba = n\) and multiplication is commutative. The only thing left is to prove that \(b\) is nontrivial, i.e. that \(2 \leq b\) and \(b < n\).

  ((b , 2≤b , b<n , a , trans (*-comm a b) ba≡n) , (a , 2≤a , a<n , b , ba≡n)) , ba≡n

First, we need a lemma that \(0 < n\), which follows because \(0 < 1 < a < n\) (remember that a proof of \(1 < a\) is actually defined to be the same thing as a proof of \(2 \leq a\)).

 where
  0<n : 0 < n
  0<n = <-trans (sle zle) (<-trans 2≤a a<n)

Next, we tackle \(2 \leq b\), by showing that \(b\) can’t possibly be \(0\) or \(1\) (using our previous lemma that anything not equal to 0 or 1 must be greater than or equal to 2).

  2≤b : 2 ≤ b
  2≤b = ¬01-is-≥2 b

If \(b\) were \(0\), then \(ba = n\) would imply \(0 = n\), but we know \(0 < n\), so this is a contradiction.

    (λ b≡0 → <→≢ 0<n
      (begin
        0                     ≡[ refl ⟩≡
        0 * a                 ≡⟨ _*_ $≡ b≡0 ≡$ a ]≡
        b * a                 ≡[ ba≡n ⟩≡
        n                     ∎
      )
    )

If \(b\) were \(1\), then \(ba = n\) would imply \(a = n\), but we know \(a < n\), so this is also a contradiction.

    (λ b≡1 → <→≢ a<n
      (begin
        a                     ≡⟨ a *1 ]≡
        a * 1                 ≡[ *-comm a 1 ⟩≡
        1 * a                 ≡⟨ _*_ $≡ b≡1 ≡$ a ]≡
        b * a                 ≡[ ba≡n ⟩≡
        n                     ∎
      )
    )

Finally, we prove \(b < n\), by showing \(b \leq n\) and \(b \neq n\).

\(b \leq n\) since \(ba = n\) and \(a\) is not zero (if \(a\) were zero it would contradict the fact that \(2 \leq a\)).

    (*→≤ (λ a≡0 → <→≢ (<-trans (sle zle) 2≤a) (sym a≡0)) (trans (*-comm a b) ba≡n))

\(b \neq n\), since \(b = n\) together with \(ba = n\) would imply \(a = 1\) (since multiplication is cancellative), but \(2 \leq a\) so it cannot equal 1.

    (λ b≡n → <→≢ 2≤a
      (sym
        (*-cancelˡ n a 1 (<→≢ 0<n)
          (begin
            n * a             ≡⟨ _*_ $≡ b≡n ≡$ a ]≡
            b * a             ≡[ ba≡n ⟩≡
            n                 ≡⟨ n *1 ]≡
            n * 1             ∎
          )
        )
      )
    )

Division

Let’s start working our way towards proving that divisibility is decidable. To check whether \(d \mid n\), the usual idea would be to divide \(n\) by \(d\) and check whether we get a remainder of zero. So we need to formalize this notion of division with remainder.

Specifically, when we divide \(n\) by \(d\), we expect to get a quotient \(q\) and a remainder \(r\), such that \(r + qd = n\), and \(0 \leq r < d\). The first condition, \(r + qd = n\), just defines what we mean by division: \(n\) is \(q\) times \(d\), plus a remainder of \(r\). The second condition will ensure that the result is unique. We wouldn’t want to divide \(17\) by \(2\) and end up with a quotient of \(6\) and a remainder of \(5\); the remainder should be as small as possible.

The DivMod type simply encodes these requirements.

data DivMod (n d q r : ℕ) : Set where
  DM : (r + q * d ≡ n) → (r < d) → DivMod n d q r

We can prove a few lemmas about DivMod. First, whenever we have DivMod n d q r, then d must be positive, since \(r < d\) and \(r\) is a natural number.

divMod→0<d : {n d q r : ℕ} → DivMod n d q r → 0 < d
divMod→0<d (DM _ r<d) = ≤-<-trans zle r<d

We can also show that for nonzero \(d\), the remainder is zero if and only if \(d \mid n\):

mod0→divides : (n d : ℕ) {q : ℕ} → DivMod n d q 0 → d ∣ n
mod0→divides n d {q} (DM eq _) = q , eq

divides→mod0 : (n d : ℕ) → (0 < d) → d ∣ n → Σ ℕ (λ q → DivMod n d q 0)
divides→mod0 n d 0<d (q , qd≡n) = q , (DM qd≡n 0<d)

We would also like to show that if the remainder when dividing \(n\) by \(d\) is not zero, then \(d\) does not divide \(n\). This is almost the contrapositive of divides→mod0—which would be trivial to show—but not quite: I said “the” remainder, but actually we don’t yet know that the quotient and remainder are unique! Perhaps we could get a remainder of 0 and some other remainder for the same \(n\) and \(d\), by choosing different quotients?

Of course, quotients and remainders are unique: that is, if \(q_1, r_1\) and \(q_2, r_2\) both satisfy the properties to be the quotient and remainder of \(n\) divided by \(d\), then in fact \(q_1 = q_2\) and \(r_1 = r_2\). But how can we prove this? The usual idea is to look at the difference \(r_1 - r_2 = dq_1 - dq_2\), which is divisible by \(d\); but since \(r_1 < d\) and \(r_2 < d\), the only way for the difference \(r_1 - r_2\) to be divisible by \(d\) is if in fact \(r_1 - r_2 = 0\). From here we can also derive \(q_1 = q_2\) via algebra.

Subtraction, eh? In order to formalize this, it seems as though we might need to define the integers… but there is a better way!

Absolute difference

The previous informal argument mentioned the difference \(r_1 - r_2\). But we could just as easily have talked about \(r_2 - r_1\) instead, and the same argument would work just as well. This observation shows that we do not actually care about the (signed) difference between \(r_1\) and \(r_2\), but only the d