# Computing prime numbers

The aim of this exercise is to implement a sieve function that
computes all the prime numbers that are less than a given number.
The first step is to define a type of comparison values:
Inductive cmp : Set := Less : cmp | Equal : cmp | Greater : cmp.

Then define the following functions:
three_way_compare : nat -> nat -> cmp

for comparing two natural numbers.

update_primes: nat -> (list nat*nat) -> (list nat*nat)*bool

such that if *k* is a natural number and *l* is a list
of pairs *(p,m)* such that
*m* is the smallest multiple of *p*
greater than or equal to *k*, then
`update_primes k l` returns the list of pairs
*(p,m')* where *m'* is the smallest
multiple of *p* strictly greater than *k* and a boolean
value that is *true* if one of the *m* was equal to *k*.
prime_sieve: nat -> (list nat*nat)

to map a
number *k* to the list of pairs *(p,m)* where *p* is a prime
number smaller or equal to *k* and *m* is the smallest multiple of
*p* greater than or equal to *k+1*.

Prove that `prime_sieve` can be used to compute all the prime
numbers smaller than a given *k*.
## Solution

This file

Going home