A Coq proof of Bertrand's postulate, which says that there always exists a prime between n and 2n for n greater than 2. Includes an application of the postulate to compute partitions.
- Author(s):
- Laurent Théry (initial)
- Coq-community maintainer(s):
- Laurent Théry (@thery)
- License: GNU Lesser General Public License v2.1 or later
- Compatible Coq versions: Coq 8.8 or later
- Additional dependencies: none
- Coq namespace:
Bertrand - Related publication(s):
The easiest way to install the latest released version of Bertrand is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-bertrandTo instead build and install manually, do:
git clone https://github.com/coq-community/bertrand.git
cd bertrand
make # or make -j <number-of-cores-on-your-machine>
make installThis project consists of:
- A Coq proof of Bertrand's postulate: there always exists a prime between
n and 2n for n greater than 2 (
Bertrand.v). - A proof of correctness of an implementation of the algorithm for computing primes described in "The Art of Computer Programming: Fundamental Algorithms" by Knuth, pages 147-149. The proof uses the Why3 tool to generate verification conditions for the WhyML program that implements the algorithm. These verification conditions can then be discharged by Coq and the Alt-Ergo prover.
- A little program in OCaml that generates a partition of 1..2n in pairs (i,j)
such that i+j is always prime (
run_partition.ml). The proof of correctness of this program is a direct consequence of Bertrand's postulate (Partition.v). This nice application of Bertrand's postulate was suggested by Gérard Huet.
To check the correctness of the WhyML program, first make sure the following packages are installed (in addition to Coq 8.12.1 and the proof of Bertrand's postulate):
- Alt-Ergo 2.3.3
- Why3 1.3.3 and its Coq library
These packages can be installed via OPAM using the following command:
opam install alt-ergo.2.3.3 why3.1.3.3 why3-coq
Then, the Why3 proof can be replayed by running
make why