meta.yml

---
fullname: Bertrand
shortname: bertrand
organization: coq-community
community: true
action: true
doi: 10.1007/10930755_20

synopsis: Coq proof of Bertrand's postulate on existence of primes

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

publications:
- pub_url: https://link.springer.com/chapter/10.1007%2F10930755_20
  pub_title: "Proving Pearl: Knuth's Algorithm for Prime Numbers"
  pub_doi: 10.1007/10930755_20

authors:
- name: Laurent Théry
  initial: true

maintainers:
- name: Laurent Théry
  nickname: thery

license:
  fullname: GNU Lesser General Public License v2.1 or later
  identifier: LGPL-2.1-or-later

supported_coq_versions:
  text: Coq 8.18 or later
  opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'

tested_coq_opam_versions:
- version: 'dev'
- version: '8.19'
- version: '8.18'

tested_coq_nix_versions:
- coq_version: 'master'

namespace: Bertrand

keywords:
- name: primality
- name: prime numbers
- name: Bertrand's postulate

categories:
- name: Mathematics/Arithmetic and Number Theory/Number theory
- name: Miscellaneous/Extracted Programs/Arithmetic

documentation: |
  ## Contents

  This 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 little program in OCaml, based on code extracted from Coq,
    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.
  - 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](http://why3.lri.fr) 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](https://alt-ergo.ocamlpro.com) prover.

  ## Extracting and running the OCaml partition program

  To extract code and obtain the program, run
  ```shell
  make run_partition.ml
  ```

  Next, open an OCaml toplevel (e.g., `ocaml`) and do
  ```ocaml
  #use "run_partition.ml";;
  ```

  To get a partition from 1...30:
  ```ocaml
  let part30 = part 15;;
  ```

  ## Replaying the WhyML program correctness proof

  To replay the proof of correctness for the WhyML program for computing primes,
  first make sure the following packages are installed (in addition to Coq 8.18.0
  and the proof of Bertrand's postulate):

  - [Alt-Ergo 2.5.4](https://alt-ergo.ocamlpro.com)
  - [Why3 1.4.1](http://why3.lri.fr) and its Coq library

  These packages can be installed via OPAM using the following command:
  ```
  opam install alt-ergo.2.5.4 why3.1.7.2 why3-coq.1.7.2
  ```
  Then, the proof can be replayed by running
  ```
  make why
  ```
---