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