{-# OPTIONS --cubical-compatible #-}
module Padova2025.Explorations.Bertrand where
Bertrand’s postulate
open import Padova2025.ProgrammingBasics.Naturals.Base open import Padova2025.ProgrammingBasics.Naturals.Arithmetic open import Padova2025.ProgrammingBasics.Lists open import Padova2025.ProvingBasics.Negation open import Padova2025.ProvingBasics.Equality.Base open import Padova2025.ProvingBasics.Connectives.Conjunction open import Padova2025.ProvingBasics.Connectives.Disjunction open import Padova2025.ProvingBasics.Connectives.Existential open import Padova2025.ProvingBasics.Connectives.More hiding (de-morgan₃) open import Padova2025.ProvingBasics.Termination.Ordering open import Padova2025.ProvingBasics.Termination.Gas
Bertrand’s postulate is a basic result in number theory. It states that for every positive natural number n, there is a prime number p with n < p ≤ 2n. The standard proof of this fact proceeds in two steps: First, for the numbers n ≥ 427, an argument involving binomial coefficients is given. Second, for the finitely many numbers n < 427, the claim is just checked by brute force, without specific mathematical insight.
In this module, we aim to formalize this second step in Agda, as it is a refreshing change of pace from typical conceptual proofs. (A correct but hard to read full proof was offered by Thiago Felicissimo and Frédéric Blanqui, as a case study in mechanically translating proofs in the impredicative Matita system to predicative Agda.) First, let’s formalize the claim.
Formalization of the claim
-- `a ∣ b` expresses that `a` divides `b`. _∣_ : ℕ → ℕ → Set a ∣ b = b % a ≡ zero -- An alternative (and perhaps better) formulation would be: -- dec-∣ a b = Σ[ k ∈ ℕ ] b ≡ k · a -- `IsPrime p` expresses that `p` is a prime number. IsPrime : ℕ → Set IsPrime p = p ≥ two × All (λ k → k > zero → k ∣ p → k ≡ one) (downFrom p) -- `BertrandClaim n` expresses that there is a prime number which is -- more than `n` and at most `2 · n` (or alternatively that `n` is zero). BertrandClaim : ℕ → Set BertrandClaim n = n ≡ zero ⊎ ∃[ p ] n < p × p ≤ twice n × IsPrime p
Decision procedures and partial decision procedures
A value of type Dec X decides X in the
sense of either supplying an inhabitant of X or supplying a
witness that no such inhabitant exists. Divisibility, primality, the
existence of a prime below a given upper bound: these are all decidable.
But in the following, we sometimes settle for partial decision
procedures, functions which either return a witness or leave the
matter undecided. We do this both to cut down on the number of proof
obligations and for fun, to explore this approximative version of
decidability.
dec-∣ : (a b : ℕ) → Dec (a ∣ b)
dec-∣ = {!!}
dec-trivial-divisor : (p k : ℕ) → Dec (k > zero → k ∣ p → k ≡ one)
dec-trivial-divisor = {!!}
prime? : (p : ℕ) → Maybe (IsPrime p)
prime? p with dec-≤ two p | dec-All (dec-trivial-divisor p) (downFrom p)
... | yes two≤p | yes f = {!!}
... | _ | _ = {!!}
bertrand₀? : (n p : ℕ) → Maybe (n < p × p ≤ twice n × IsPrime p)
bertrand₀? n p with dec-< n p | dec-≤ p (twice n) | prime? p
... | yes n<p | yes p≤2n | just f = {!!}
... | _ | _ | _ = {!!}
The following function is the analogue of find
from Padova2025.ProvingBasics.Connectives.More for partial
decidability instead of full decidability.
find' : {A : Set} {P : A → Set} → ((x : A) → Maybe (P x)) → (xs : List A) → Maybe (Any P xs)
find' = {!!}
bertrand? : (n : ℕ) → Maybe (BertrandClaim n)
bertrand? n with n ≟ zero | find' (bertrand₀? n) (downFrom (succ (twice n)))
... | yes n≡zero | _ = {!!}
... | no n≢zero | just f = {!!}
... | no n≢zero | nothing = {!!}
Empirically observing the claim
With the partial decision procedure bertrand? at hand,
we can collect all the positive verdicts into an All
structure.
claim? : Maybe (All BertrandClaim (downFrom ten)) claim? = collect bertrand? ten -- We should really put 427 here, but use 10 to reduce the load on the Let's play Agda server.
We don’t supply a reason that claim? is of the form
just _. But it is, and Agda will verify this (by blithely
evaluating it) when we put claim? in the following
hole:
empirical-fact : All BertrandClaim (downFrom ten)
empirical-fact = from-just {!!}
To explore this further, put your favorite number below ten into the
hole below and then press C-c C-v to run
example, obtaining a printout of a prime number which is
more than your number and at most twice your number.
fav : ℕ
fav = {!!}
example : BertrandClaim fav
example = lookup empirical-fact fav<ten
where
fav<ten = {!!}