# Euclid's Theorem

## An annotated proof in Agda that there are infinitely many primes

*This document describes a proof in Agda that there are infinitely many primes, or more precisely, that for any natural number *$n$* there exists a prime *$p$* such that *$p>n$*. We have explained the code in great detail, as an introduction to Agda for mathematicians. The **original article** has been slightly changed (mostly due to Agda stdlib updates) in order to be runnable in nextjournal.*

As Agda is based on intuitionistic logic, we can only prove the existence of $p$ by constructing it, in some sense or other. Our approach is as follows:

(a) We prove that for any natural number $m>1$ there is a smallest natural number $p>1$ such that $p$ divides $m$, and that this $p$ is prime.

(b) Given an arbitrary natural number $n$ we show that the number $m=n!+1$ is larger than $1$, so we can apply (a) to get a prime $p$ dividing $m$.

(c) We then prove that this $p$ is larger than $n$. In more detail, we suppose that $p\leq n$, and then note that $p$ divides both $n!$ and $n!+1$, so $p$ divides $1$, so $p=1$, which is a contradiction because $1$ is not prime. This proves the double negation of the desired inequality $p>n$, which is enough even in Agda's constructive framework because the order relation on $ℕ$ is decidable.

The proof relies on a number of modules in the Agda standard library, and some new modules written for this project. The basic definitions of Peano arithmetic are set up in the Agda standard library (specifically, in the module `Data.Nat`

and its submodules). Facts about divisibility and primes are proved in `Data.Nat.Divisibility`

and `Data.Nat.Primality`

. The new modules are as follows:

The module

`Extra.Data.Nat.LargerPrime`

defined in this file assembles the ingredients mentioned below to prove the main result.The module

`Extra.Data.Nat.LeastDivisor`

implements step (a) in the above outline. It relies on a more general framework for finding least elements defined in the module`Extra.Data.Nat.Minimiser`

.The module

`Extra.Data.Nat.Primality`

proves some basic facts about primes that are not covered by the standard library module`Data.Nat.Primality`

.The module

`Extra.Data.Nat.Factorial`

defines the factorial function and proves some basic properties.

*In **nextjournal** each Agda **runtime** defines its own **.agda** file and can be exported as a library in order to be reused in this or other notebooks (check runtime settings in the sidebar on the left). When running a cell, the code from all preceding cells within the same runtime is joined and submitted for execution; this execution behaviour is specific to Agda only, if we split a construct into several cells, we need to execute the first cell of the runtime which reaches a valid expression.*

We start by declaring the module:

`module Extra.Data.Nat.LargerPrime where`

Modules provide a framework for packaging together related definitions. In ordinary mathematical writing it is common to quote results from different sources with incompatible notational conventions; one then has to redefine some of the notation in the sources to avoid ambiguity or clashes. Agda modules provide reasonably good support for maneuvers of this kind.

We next list some standard library modules whose results we need to use. Note that we use the keyword `open`

as well as `import`

. If we just say `import Data.Nat.Primality`

then we can use the definition `Prime`

given in the module `Data.Nat.Primality`

but we need to refer to it as `Data.Nat.Primality.Prime`

. If we then say `open Data.Nat.Primality`

then we can use the short form `Prime`

rather than `Data.Nat.Primality.Prime`

. The line `open import Data.Nat.Primality`

is equivalent to `import`

followed by `open`

. The code for the module `Data.Nat.Primality`

is in the file `src/Data/Nat/Primality.agda`

in the standard library. The location of the standard library depends on the details of your installation. If you already have Agda working under emacs then the command `C-h v agda2-include-dirs`

should tell you where to look.

`open import Data.Empty`

`open import Data.Nat`

`open import Data.Nat.Properties hiding (+-comm)`

`open import Data.Nat.Divisibility`

`open import Data.Nat.Primality`

`open import Relation.Nullary`

`open import Relation.Binary.PropositionalEquality`

The module `Data.Empty`

defines the empty set. The next four modules should be self-explanatory. The module `Relation.Nullary.Core`

contains the negation operator and some auxiliary definitions for decidable relations that will be discussed later. The module `Relation.Binary.PropositionalEquality`

contains some code that makes it easier to formalise proofs that use chains of equalities, like

It also contains many things that will not concern us for the moment.

Next, we will need to use the fact that addition of natural numbers is commutative. In order to keep the standard library tidy, this is not represented as an isolated fact, but is packaged with various other facts in a proof that $ℕ$ is a commutative semiring. We therefore need to import the definition of a semiring to gain access to the fact that we need. We use the following code:

`open import Algebra.Structures`

`open IsCommutativeSemiring *-+-isCommutativeSemiring using ( +-comm )`

The effect is that the name `+-comm`

now refers to a proof that $n+m=m+n$ for all $n,m\in ℕ$. (Note that names in Agda can use almost any character other than a space. It is common for names to include mathematical symbols or other punctuation.)

The details take some explanation, which could be skipped by the impatient. Firstly, `IsCommutativeSemigroup`

(with a capital `I`

) is a function of eight arguments that is defined in the module `Algebra.Structures`

. The first three arguments are given in curly brackets in the function definition, which means that in most circumstances these arguments need not be given explicitly because they can be deduced from the remaining arguments. The first two arguments are levels, which are used by Agda to avoid Russell-type paradoxes. One can usually ignore these completely. The third (implicit) argument is a set $A$. The remaining (explicit) arguments are a relation on $A$ (written as $≈$), two binary operations on $A$ (written as addition and multiplication) and two elements $0,1\in A$. The value of the function `IsCommutativeSemigroup`

at these arguments is, roughly speaking, the set of proofs that $≈$ is an equivalence relation and that $A/≈$ is a commutative semiring under the given operations. Of course this set could be empty, if the operations do not in fact make $A/≈$ into a commutative semiring. (For reasons that we will not discuss here, algebraic structures are always represented in Agda in this fashion, with operations defined on a set $A$, and axioms that hold only modulo a specified equivalence relation on $A$.)

Next, the natural numbers zero and one, and the operations of addition and multiplication of natural numbers, are defined in `Data.Nat`

. We also have the relation of equality on $ℕ$. Feeding these ingredients into the function `IsCommutativeSemiring`

we get the set $P$ of proofs that $ℕ$ is a commutative semiring. The module `Data.Nat.Properties`

constructs such a proof, which is a particular element called `Data.Nat.Properties.isCommutativeSemiring`

(with a lower case `i`

) of the set $P$. As we have imported and opened the module `Data.Nat.Properties`

, we can omit the prefix and use the name `isCommutativeSemiring`

.

We described `IsCommutativeSemiring`

as a set-valued function, which is essentially correct, but in more technical terms it is a parametrised record type. Agda automatically creates an associated module for each parametrised record type. The statement

`open IsCommutativeSemiring *-+-isCommutativeSemiring using ( +-comm )`

is a variant of the operation of opening a module, which we have seen before. The proof `*-+-isCommutativeSemigroup`

is a package of proofs of all the different axioms for a commutative semiring, and the effect of the above `open`

statement is to enable us to refer to the part of the package called `+-comm`

, which is a proof that addition is commutative. This process of opening a record is similar to the usual practice of saying "consider a semiring $R$" and then taking all semiring-related notation to refer to $R$ unless otherwise specified.

We need one more module from the standard library, called `∣-Reasoning`

. This is defined as a submodule of `Data.Nat.Divisibility`

, and it makes it easier to reason with chains of divisibility statements, analogous to the chains of equalities that we described previously.

`open Data.Nat.Divisibility.∣-Reasoning`

We also import three new modules that we mentioned previously:

`open import Extra.Data.Nat.LeastDivisor`

`open import Extra.Data.Nat.Primality`

`open import Extra.Data.Nat.Factorial`

We next specify what we hope to construct. In Agda, whenever we construct an object with certain properties, we need to package it together with a collection of proofs that it does indeed have those properties. In our case we construct a prime $p$ that is larger than $n$, and we need to remember a proof of that inequality. In Agda, the proposition that $p$ is greater than $n$ is denoted by `p > n`

, with spaces between the symbols. Like all propositions in Agda, this is a type, whose terms (if any) are the proofs that $p>n$. The string `p>n`

(with no space) is a valid variable name in Agda, and it is a standard idiom to use this name to refer to an arbitrary term of type `p > n`

. With this notation, we hope to construct a record consisting of a natural number $p$, a proof (denoted by `p-prime`

) that $p$ is prime, and a proof (denoted by `p>n`

) that $p>n$. The next block of code defines `LargerPrime n`

(with a capital L) to be the set of such records.

`record LargerPrime (n : ℕ) : Set where`

` field`

` p : ℕ`

` p-prime : Prime p`

` p>n : p > n`

We now want to define a function `largerPrime`

(with a lower case l) which constructs an element `largerPrime n`

of `LargerPrime n`

for each natural number $n$. In Agda's notation, this means that `largerPrime`

is a term of type `(n : ℕ) → LargerPrime n`

. Agda's type checking system is strong enough that to ensure that any term that it accepts as having the above type gives a valid proof of Euclid's theorem.

The next few lines are housekeeping:

`largerPrime : (n : ℕ) → LargerPrime n`

`largerPrime n = record {`

` p = p ;`

` p-prime = p-prime ;`

` p>n = p>n`

` } where`

The rest of the code is indented at least as much as the keyword `where`

, which means that it is treated as a single block. The above lines tell Agda that this block will define `p`

, `p-prime`

and `p>n`

with the advertised types.

We next invoke the `leastDivisor`

function defined in the module `Extra.Data.Nat.LeastDivisor`

.

` L = leastDivisor (1 + (n !)) (s≤s (n!≥1 n))`

The `leastDivisor`

function takes two arguments: a natural number and a proof that that number is at least two. For the number we take $1+(n!)$. The module `Extra.Data.Nat.Factorial`

defines a function `n!≥1`

such that `n!≥1 n`

is a proof that `1 ≤ n!`

, and `Data.Nat`

defines a function `s≤s`

that converts proofs of `a ≤ b`

to proofs of `1 + a ≤ 1 + b`

. We can thus use `s≤s (n!≥1 n)`

as the second argument to `leastDivisor`

, and we define `L`

to be the value returned by this function. Now `L`

is a record with seven fields. There is a field called `p`

whose value is a natural number, a field called `p-prime`

whose value is a proof that `p`

is prime, and a field called `p-least`

whose value is a proof that no number with $2\leq k<p$ divides $1+(n!)$.

There is also a field called `p∣n`

. The name of this field is designed to make sense when the first argument to `leastDivisor`

is called `n`

. Its value in our context is in fact a proof that $p$ divides $1+(n!)$, not a proof that $p$ divides $n$.

We now open the record `L`

:

` open LeastDivisor L renaming ( p≤n to p≤1+n! ; p∣n to p∣1+n! )`

This allows us to refer to the fields in `L`

by their short names, except that we have given two of the fields new names that make more sense in our context. In particular, this defines `p`

and `p-prime`

as required, so we just need to define `p>n`

.

We first declare the type of `p>n`

:

` p>n : p > n`

We next have a `with`

clause:

` p>n with (suc n) ≤? p`

Here `suc`

is the successor function, taking $n$ to $1+n$. Next, there is a function called `_≤?_`

defined in `Data.Nat`

. This is an example of a useful notational mechanism in Agda: when the name of a function involves underscores, the position of those underscores indicates how the arguments are placed relative to the function symbol. Because the name `_≤?_`

starts and ends with an underscore, we can write `n ≤? m`

for the value of the function at a pair of natural numbers `n`

and `m`

. That value will either have the form `yes r`

(where `r`

is a proof that $n\leq m$) or `no q`

(where `q`

is a proof that $n\not\leq m$ ). These are terms of the type `Dec (n ≤ m)`

, which is defined in `Relation.Nullary`

. The clause `p>n with (suc n) ≤? p`

indicates that we will define `p>n`

using two separate cases, depending on the value of `(suc n) ≤? p`

. If this value has the form `yes r`

then `r`

must be a proof that `p > n`

and we can just take `p>n`

to be `r`

. (This relies on the fact that `p > n`

is *by definition* the same as `(suc n) ≤ p`

, as we see by reading the code for `Data.Nat`

.) This is implemented by the following line:

` p>n | yes r = r`

Now what if `(suc n) ≤? p`

has the form `no q`

for some `q`

? Here `q`

would have to be a proof that `p ≤ n`

, which cannot actually happen. Nonetheless, Agda forces use to deal with this hypothetical case, and prove that it is vacuous. This works as follows. Agda notation for the empty type is `⊥`

. For any set `W`

there is a term `⊥-elim`

of type `(⊥ → W)`

. Logically, this corresponds to the principle that a falsity implies everything; set-theoretically, it corresponds to the fact that the empty set is initial in the category of sets. (The set `W`

is an implicit argument to the `⊥-elim`

function, given in curly brackets when that function is defined in `Data.Empty`

.) Next, the function `Prime`

defined in `Data.Nat.Primality`

sends a natural number $n$ to the set of proofs that $n$ is prime. When $n$ is given as a double successor, the set `(Prime n)`

is defined in an obvious way in terms of divisibility properties. However, the two initial cases $n=0$ and $n=1$ are handled separately, with `Prime 0 = Prime 1 = ⊥`

by definition. We handle the `no q`

case by constructing from `q`

a proof that $1$ is prime, or in other words a term `1-prime`

of type `Prime 1 = ⊥`

. We then apply `⊥-elim`

to `1-prime`

to get a term of whatever type we want; in this case, a term of type `(p > n)`

. The line

` p>n | no q = ⊥-elim 1-prime where`

indicates that we will handle the `no q`

case by the general approach discussed above, and promises that the following block of code will eventually define `1-prime`

. Note that the type checker knows what type `p>n`

is supposed to have, and supplies this type as the implicit argument to `⊥-elim`

. It also knows that `1-prime`

must have type `⊥`

in order to be an acceptable explicit argument to `⊥-elim`

, and when we get to the definition of `1-prime`

it will check that we have indeed provided a term of type `⊥`

.

The rest of the code forms another `where`

block nested inside the `where`

block that we introduced earlier, so it is indented by two more spaces.

We now construct a proof that `p`

divides `n !`

. The module `Data.Nat.Factorial`

defines a function `k∣n!`

that takes a pair of inequalities `1 ≤ k`

and `k ≤ n`

, and returns a proof that `k`

divides `n !`

. We have a proof called `p-prime`

that `p`

is prime, and the function `prime≥1`

defined in `Extra.Data.Nat.Primality`

can be used to convert this to a proof that `1 ≤ p`

. By hypothesis we have a proof called `q`

that `p > n`

is false, and using the functions `≰⇒>`

and `≤-pred`

from `Data.Nat`

we convert this to a proof that `p ≤ n`

is true. After feeding these ingredients to the function `k∣n!`

we obtain the required proof that `p`

divides `n !`

. We denote this proof by `p∣n!`

.

` p∣n! : p ∣ n !`

` p∣n! = k∣n! (prime≥1 p-prime) (≤-pred (≰⇒> q))`

We now need a proof that `p`

divides `n ! + 1`

. We have already extracted from the record `L`

a proof (denoted by `p∣1+n!`

) that `p`

divides `1 + n !`

. Although `n ! + 1`

is provably equal to `1 + n !`

, these two terms have a different internal representation so we cannot just use `p∣1+n!`

as a proof that `p ∣ n ! + 1`

. However, we also extracted a function called `+-comm`

from `Data.Nat.Properties.isCommutativeSemiring`

, and `(+-comm 1 (n !))`

is a proof that `1 + n ! ≡ n ! + 1`

. Using notation established in the module `∣-Reasoning`

we can string these proofs together:

` p∣n!+1 : p ∣ n ! + 1`

` p∣n!+1 = begin p ∣⟨ p∣1+n! ⟩ 1 + (n !) ≡⟨ +-comm 1 (n !) ⟩ (n !) + 1 ∎`

We next use the function `∣m+n∣m⇒∣n`

defined in `Data.Nat.Divisibility`

. Given proofs that `i`

divides `n + m`

and `n`

, this returns a proof that `i`

divides `m`

. Thus, we can pass in our proofs that `p`

divides `n !`

and `n ! + 1`

, and get back a proof that `p`

divides `1`

.

` p∣1 : p ∣ 1`

` p∣1 = ∣m+n∣m⇒∣n p∣n!+1 p∣n!`

The module `Data.Nat.Divisibility`

also defines a function called `∣1⇒≡1`

, which can be used to convert our proof that $p$ divides $1$ to a proof that $p=1$.

` p≡1 : p ≡ 1`

` p≡1 = ∣1⇒≡1 p∣1`

We conclude by using the function `subst`

defined in `Relation.Binary.PropositionalEquality.Core`

. Roughly speaking, this works as follows. The first argument is a set `A`

depending on a parameter `x`

. The second argument is a proof of `u ≡ v`

, where `u`

and `v`

are possible values of `x`

. The third argument is an element of the set `(A u)`

, and the return value is the same thing regarded as an element of `(A v)`

. We have a proof that `p ≡ 1`

and a proof that `p`

is prime, so we can use `subst`

to produce a proof that `1`

is prime.

` 1-prime : Prime 1`

` 1-prime = subst Prime p≡1 p-prime`

As discussed previously, this element `1-prime`

can be fed into `⊥-elim`

to give a tautological proof of our theorem in the vacuous case where `p ≤ n`

.

## Divisibility

`module Extra.Data.Nat.Divisibility where`

`open import Algebra`

`open import Algebra.Structures`

`open import Data.Nat`

`open import Data.Nat.Properties renaming (*-comm to nat-comm)`

`open import Data.Nat.Divisibility.Core`

`open import Data.Nat.Divisibility using (∣-poset)`

`open import Relation.Binary`

`open import Relation.Binary.PropositionalEquality`

`private`

` module CS = CommutativeSemiring Data.Nat.Properties.*-+-commutativeSemiring`

`open IsCommutativeSemiring *-+-isCommutativeSemiring hiding (refl ; sym ; trans)`

`left-* : {m n : ℕ} → (p : ℕ) → m ∣ n → m ∣ (p * n)`

`left-* p m∣n = Poset.trans ∣-poset m∣n (divides p refl)`

`right-* : {m n : ℕ} → (p : ℕ) → m ∣ n → m ∣ (n * p)`

`right-* {m} {n} p m∣n = Poset.trans ∣-poset m∣n (divides p (nat-comm n p))`

## The Factorial Function

This file defines the factorial function in Agda and proves some basic properties. We start by declaring a module:

`module Extra.Data.Nat.Factorial where`

We next list some standard library modules whose results we need to use. Recall that after importing and opening a module we can use all the definitions from that module without needing to give the module name as a prefix.

`open import Data.Nat`

`open import Data.Nat.Properties -- using (≤-trans)`

`open import Data.Nat.Divisibility.Core`

`open import Data.Nat.Divisibility using (∣-poset)`

`open import Extra.Data.Nat.Divisibility`

`open import Relation.Nullary`

`open import Relation.Binary`

`open import Relation.Binary.PropositionalEquality`

`open ≡-Reasoning`

`open DecTotalOrder ≤-decTotalOrder hiding (_≤_ ; _≤?_ ) renaming (refl to ≤-refl)`

We now give the obvious recursive definition of the factorial function. Note that the official name of this function is `_!`

, and that the placement of the underscore indicates that we can write the argument on the left, giving the traditional notation `n !`

for `n`

factorial.

`_! : ℕ → ℕ`

`0 ! = 1`

`(suc n) ! = (suc n) * (n !)`

We now want to prove some divisibility statements. The first of these says that if $k\leq n$ then $k!$ divides $n!$. Recall that there are two different, but essentially equivalent, formulations of the order relation on `ℕ`

, denoted by `≤`

and `≤′`

. (The first treats `0 ≤ n`

as a special case, whereas the second treats `n ≤′ n`

as a special case instead.) It is convenient to prove the result using `≤′`

first and then deduce the result for `≤`

using the conversion function `≤⇒≤′`

defined in `Data.Nat`

.

We start by defining a function called `k!∣n!′`

. It takes two implicit arguments called `k`

and `n`

, and an explicit argument which is a proof that `k ≤′ n`

. It then returns a proof that `k !`

divides `n !`

. These facts are represented by the following declaration:

`k!∣n!′ : {k n : ℕ} → k ≤′ n → (k !) ∣ (n !)`

To see how the definition works, we need to understand the explicit argument in more detail. As with all propositions in Agda, the proposition `k ≤′ n`

is actually a type, and terms of that type count as proofs of the proposition. The type is defined inductively by the following rules:

For each natural number

`n`

, there is a term`≤′-refl`

of type`n ≤′ n`

. Here`n`

is an implicit argument to the function`≤′-refl`

so Agda will deduce it from the context in which the function is used.For every term

`i≤′j`

of type`i ≤′ j`

, there is a term`(≤′-step i≤′j)`

of type`i ≤′ (1 + j)`

.All terms of type

`n ≤′ m`

arise from one of the above two constructors.

We can thus define `k!∣n!′`

by specifying its value on terms constructed in the above two ways.

The value on a term `≤′-refl`

of type `n ≤′ n`

should be a proof that `n ∣ n`

. The module `Data.Nat.Divisibility`

contains such a proof, as part of a package that describes `ℕ`

as a partially ordered set under the relation of divisibility. The whole package has the fully qualified name `Data.Nat.Divisibility.poset`

, but we imported and opened the module `Data.Nat.Divisibility`

with renaming, so we can use the shorter name `∣-poset`

instead. This is a record of type `Poset`

as defined in `Relation.Binary`

. One of the fields in this record is a function called `refl`

that takes a natural number `n`

as an implicit argument and returns a term of type `n ∣ n`

. To refer to the `refl`

field in the record `∣-poset`

(of type `Poset`

) we use the syntax `Poset.refl ∣-poset`

. This leads to the following clause as the first half of the definition of `k!∣n!′`

:

`k!∣n!′ ≤′-refl = (Poset.refl ∣-poset)`

For the second half of the definition, we must cover the case where the explicit argument has the form `(≤′-step k≤′n)`

for some natural numbers `k`

and `n`

, so the implicit arguments are `k`

and `suc n`

. It is convenient here to make the implicit arguments explicit, which is permitted if we enclose them in curly brackets. We may assume by induction that `(k!∣n!′ k≤′n)`

is defined as a term of type `k ! ∣ n !`

. The module `Extra.Data.Nat.Divisibility`

defines a function `left-*`

which accepts an integer `a`

and a proof that `b ∣ c`

and returns a proof that `b ∣ a * c`

. We have `(suc n) * (n !) = (suc n) !`

by definition, so `left-* (suc n) (k!∣n!′ k≤′n)`

is a proof that `k !`

divides `(suc n) !`

. This validates the following clause, which completes the definition of `k!∣n!′`

`k!∣n!′ {k} {suc n} (≤′-step k≤′n) = left-* (suc n) (k!∣n!′ k≤′n)`

The module `Data.Nat`

defines a function `≤⇒≤′`

that converts terms of type `i ≤ j`

to terms of type `i ≤′ j`

. This provides a straightforward way to define `k!∣n!`

in terms of `k!∣n!′`

:

`k!∣n! : {k n : ℕ} → k ≤ n → k ! ∣ n !`

`k!∣n! k≤n = k!∣n!′ (≤⇒≤′ k≤n)`

We now prove that if `0 < k ≤ n`

then `k`

divides `n !`

. It is again convenient to prove a version using `≤'`

first. It is also convenient to prove the shifted statement that if `k < n`

then `suc k`

divides `n !`

, and deduce the unshifted statement from this. We have the following declaration for the shifted version:

`k+1∣n!′ : {k n : ℕ} → k <′ n → suc k ∣ n !`

The explicit argument is of type `k <′ n`

, which is by definition the same as `(suc k) ≤′ n`

. Our function is again defined by two separate clauses for the two possible forms of this explicit argument. If it has the form `≤′-refl`

then `n`

is forced to be the same as `suc k`

. The function `(Poset.refl ∣-poset)`

(with implicit argument `k`

) provides a proof that `suc k ∣ suc k`

, and we can use the function `right-*`

(from `Extra.Data.Nat.Divisibility`

) to convert this to a proof that `suc k`

divides `n ! = (suc k) * (k !)`

. The required syntax is as follows:

`k+1∣n!′ {k} .{suc k} ≤′-refl = right-* (k !) (Poset.refl ∣-poset)`

Note that the first two arguments on the left hand side are in curly brackets, because they are implicit arguments that we have chosen to make explicit. Note also the dot attached to `{suc k}`

which indicates that the second argument is forced to be `suc k`

in order for the left hand side to be meaningful. This is the only circumstance in which one is allowed to repeat a variable name on the left hand side of a definition.

We now cover the second case of `k+1∣n!′`

. Here we have natural numbers `k`

and `n`

, and a proof (named `k<′n`

) that `k <′ n`

, which is converted by `≤′-step`

to a proof that `k <′ suc n`

. We may assume inductively that `(k+1∣n!′ k<′n)`

is defined and gives a proof that `suc k`

divides `n !`

. We use the function `left-*`

(from `Extra.Data.Nat.Divisibility`

) to convert this to a proof that `suc k`

divides `(suc n) ! = (suc n) * (n !)`

.

`k+1∣n!′ {k} {suc n} (≤′-step k<′n) = left-* (suc n) (k+1∣n!′ k<′n)`

We again use the function `≤⇒≤′`

from `Data.Nat`

to reformulate our statement in terms of `≤`

rather than `≤′`

.

`k+1∣n! : {k n : ℕ} → k < n → suc k ∣ n !`

`k+1∣n! k<n = k+1∣n!′ (≤⇒≤′ k<n)`

It is also convenient to give a further reformulation in which we unshift the first argument. The declaration is as follows:

`k∣n! : {k n : ℕ} → 0 < k → k ≤ n → k ∣ n !`

It is straightforward to define this function by pattern matching. The first explicit argument is a proof that `0 < j`

, or equivalently that `suc 0 ≤ j`

. The propositions `n ≤ m`

are again defined (in `Data.Nat`

) by inductive rules:

For any natural number

`n`

, there is a term`z≤n`

(with`n`

as an implicit argument) of type`0 ≤ n`

.For any term

`t`

of type`n ≤ m`

, there is a term`s≤s t`

of type`suc n ≤ suc m`

.All terms of type

`n ≤ m`

(for any`n`

and`m`

) are obtained by iterated application of these constructors.

The only possible pattern for a proof of `suc 0 ≤ k`

is `s≤s z≤n`

, where the implicit argument to `z≤n`

must be a natural number `j`

with `suc j ≡ k`

. In this context the second argument to `k∣n!`

must be a proof that `suc j ≤ n`

, or equivalently that `j < n`

. We can thus feed this proof into the function `k+1∣n!`

to see that `k`

divides `n !`

. The relevant syntax is as follows:

`k∣n! (s≤s z≤n) j<n = k+1∣n! j<n`

We conclude with a proof that `n ! ≥ 1`

for all `n`

. TODO: explain this.

`n!≥1 : (n : ℕ) → ((n !) ≥ 1)`

`n!≥1 0 = s≤s z≤n`

`n!≥1 (suc m) = ≤-trans (n!≥1 m) (m≤n+*m (m !) m) where`

` m≤n+*m : (m n : ℕ) → (m ≤ (suc n) * m)`

` m≤n+*m m n = m≤m+n m (n * m)`

## A Minimiser Function

This file defines a function that finds the smallest element of a nonempty decidable subset of the natural numbers. In more detail, the input consists of

A map

`P : ℕ → Set`

. We treat`P n`

as a proposition in the usual way, so we can consider the set $S$ of numbers $n$ such that`P n`

is nonempty. This is the set whose minimum element we wish to find.A term

`P?`

of type`Decidable P`

(which is defined in`Relation.Unary`

). This means that for each natural number $n$ we have a term`P? n`

which has the form`yes p`

(with`p`

of type`P n`

) or`no q`

(with`q`

of type`¬ P n`

). In other words,`P?`

is a proof that`P`

is decidable.A natural number

`n`

and a term`p`

of type`P n`

, witnessing the fact that $S$ is nonempty.

The output consists of

A natural number

`n`

.A term

`Pn`

of type`P n`

, proving that $n\in S$.A proof that no smaller number lies in $S$.

The definition of our function is roughly as follows.

If $0\in S$ then we just have to provide a vacuous proof that all smaller numbers are not in $S$.

Otherwise $n$ will be $n'+1$ for some $n'$. We then find the smallest element of the set $S'=\{k\in ℕ : k+1\in S\}$ and add one to it. The main work is just in preparing the auxiliary information for $S'$ from the auxiliary information for $S$, and then performing the reverse translation for the minimal element.

We start with the module header and import statements:

`module Extra.Data.Nat.Minimiser where`

`open import Data.Empty`

`open import Data.Nat`

`open import Relation.Nullary`

`open import Relation.Unary`

`import Level`

We now define an ℕ-set to be a decidable subset of ℕ, encoded as a record consisting of terms `P`

and `P?`

as discussed previously. As a slight complication, we need to allow for the values of `P`

to be sets of an arbitrary but specified level `c`

, which is supplied as an implicit argument. I do not understand all the issues about levels, but the code below seems to do the job.

The line `constructor _,_`

just declares an abbreviated syntax for definining ℕ-sets. We will see examples below.

`record ℕ-set {c} : Set (Level.suc c) where`

` constructor _,_`

` field`

` P : ℕ → Set c`

` P? : Decidable P`

We now declare another record type `Minimiser S`

depending on an ℕ-set $S$. A term of this type packages the smallest element of $S$ together with evidence that it is the smallest element.

`record Minimiser (S : ℕ-set) : Set where`

` constructor _,_,_`

` open ℕ-set S`

` field`

` n : ℕ`

` Pn : P n`

` minimal : (k : ℕ) → (k < n) → ¬ (P k)`

We now define a function `0-min`

. This takes an ℕ-set $S$, and a proof that $0$ is an element of that ℕ-set, and wraps it up with some trivial data to produce a term of type `Minimiser S`

.

`0-min : {S : ℕ-set} → (P0 : (ℕ-set.P S zero)) → Minimiser S`

`0-min P0 = 0 , P0 , λ k → λ ()`

We can now define the function that is the main point of this module.

`minimiser : (S : ℕ-set) → (n : ℕ) → (ℕ-set.P S n) → (Minimiser S)`

`minimiser S 0 P0 = 0-min P0`

`minimiser S (suc m) Q with (ℕ-set.P? S) 0`

`... | yes P0 = 0-min P0`

`... | no ¬P0 = suc n′ , P′n′ , minimal where`

` P′ : ℕ → Set`

` P′ k = (ℕ-set.P S) (suc k)`

` P′? : Decidable P′`

` P′? k = (ℕ-set.P? S) (suc k)`

` S′ : ℕ-set`

` S′ = P′ , P′?`

` M′ = minimiser S′ m Q`

` n′ = Minimiser.n M′`

` P′n′ = Minimiser.Pn M′`

` minimal′ = Minimiser.minimal M′`

` minimal : (k : ℕ) → (k < suc n′) → ¬ ((ℕ-set.P S) k)`

` minimal 0 _ = ¬P0`

` minimal (suc k) (s≤s k<n′) = minimal′ k k<n′`

## Primality

`module Extra.Data.Nat.Primality where`

`open import Data.Nat`

`open import Data.Nat.Primality`

`prime≥1 : {p : ℕ} → (Prime p) → (1 ≤ p)`

`prime≥1 {zero} ()`

`prime≥1 {suc zero} ()`

`prime≥1 {suc (suc n)} _ = (s≤s z≤n)`

`prime≥2 : {p : ℕ} → (Prime p) → (2 ≤ p)`

`prime≥2 {zero} ()`

`prime≥2 {suc zero} ()`

`prime≥2 {suc (suc n)} _ = s≤s (s≤s z≤n)`

## Least Divisor

`module Extra.Data.Nat.LeastDivisor where`

`open import Data.Nat`

`open import Data.Nat.Divisibility.Core`

`open import Data.Nat.Divisibility using (∣-poset ; _∣?_ ; ∣⇒≤)`

`open import Data.Nat.Primality`

`open import Relation.Nullary`

`open import Relation.Unary`

`open import Relation.Binary`

`open import Relation.Binary.PropositionalEquality`

`open import Data.Fin hiding (_≤_ ; _<_ ; _+_)`

`open Data.Nat.Divisibility.∣-Reasoning`

`open import Extra.Data.Nat.Minimiser`

`record LeastDivisor {n : ℕ} : Set where`

` field`

` 2≤n : 2 ≤ n`

` p : ℕ`

` 2≤p : 2 ≤ p`

` p≤n : p ≤ n`

` p∣n : p ∣ n`

` p-least : (k : ℕ) → 2 ≤ k → k < p → ¬ ( k ∣ n )`

` p-prime : Prime p`

`leastDivisor : (n : ℕ) → (2≤n : 2 ≤ n) → (LeastDivisor {n})`

`leastDivisor 0 ()`

`leastDivisor (suc 0) (s≤s ())`

`leastDivisor (suc (suc n-2)) 2≤n = record {`

` 2≤n = 2≤n ;`

` p = p ;`

` 2≤p = s≤s (s≤s z≤n) ;`

` p∣n = p∣n ;`

` p≤n = ∣⇒≤ p∣n ;`

` p-least = p-least ;`

` p-prime = p-prime`

` } where`

` n = suc (suc n-2)`

` P : ℕ → Set`

` P k-2 = suc (suc k-2) ∣ n`

` P? : Relation.Unary.Decidable P`

` P? k-2 = suc (suc k-2) ∣? n`

` S : ℕ-set`

` S = P , P?`

` M = minimiser S n-2 (Poset.refl ∣-poset)`

` open Minimiser M renaming ( n to p-2 ; Pn to p∣n )`

` p = suc (suc p-2)`

` p-least : (k : ℕ) → 2 ≤ k → k < p → ¬ ( k ∣ n )`

` p-least zero () _ _`

` p-least (suc zero) (s≤s ()) _ _`

` p-least (suc (suc k-2)) 2≤k (s≤s (s≤s k-2<p-2)) k∣n =`

` minimal k-2 k-2<p-2 k∣n`

` p-prime : Prime p`

` p-prime k k+2∣p = minimal (toℕ k) (Fin<top k) k+2∣n where`

` Fin<top : {n : ℕ} → (k : Fin n) → (toℕ k < n)`

` Fin<top zero = s≤s z≤n`

` Fin<top (suc i) = s≤s (Fin<top i)`

` k+2∣n = begin (2 + (toℕ k)) ∣⟨ k+2∣p ⟩ p ∣⟨ p∣n ⟩ n ∎`