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.