Euclid's Theorem

An annotated proof in Agda that there are infinitely many primes

Neil P. Strickland - CC BY-NC-SA 4.0

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:

1. The module Extra.Data.Nat.LargerPrime defined in this file assembles the ingredients mentioned below to prove the main result.

2. 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.

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

4. 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:

1. 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.

2. For every term i≤′j of type i ≤′ j, there is a term (≤′-step i≤′j) of type i ≤′ (1 + j).

3. 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:

1. For any natural number n, there is a term z≤n (with n as an implicit argument) of type 0 ≤ n.

2. For any term t of type n ≤ m, there is a term s≤s t of type suc n ≤ suc m.

3. 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 ∎