The contracts of the plain sieve

The contracts of the loops of the plain sieve of one denominator, the reference of the bit arrays of words, as @[spec] theorems proved with vcgen, the program logic of Lean core, with loop invariants that are named definitions.

Main statements

• Ratpoints.Sieve.sieveDen_spec: entry i of the sieve of a denominator b is the survivor test Ratpoints.Sieve.survives of the numerator i - H.
• Ratpoints.Sieve.checkDen_spec: if entry i of the array is keep (i - H) for every i, the survivors of the array give the points of the brute-force reference over b and the numerators that pass keep.

Implementation notes

The file uses Lean core and Std only, so that the grind calls of the proofs see only the lemmas of core, untouched by the updates of Mathlib. The lemmas on the brute-force reference that the contracts need, Ratpoints.BruteForce.pointsOfDen_nil, Ratpoints.BruteForce.pointsOfDen_append, Ratpoints.BruteForce.pointsOfDen_singleton and Ratpoints.BruteForce.pointsOfDen_filter, and those on the numerators -H, …, H that the contracts of the sieve need, Ratpoints.BruteForce.map_toList_range_eq_numerators, Ratpoints.BruteForce.natAbs_le_of_mem_numerators and Ratpoints.BruteForce.pairwise_lt_numerators, are stated here, without Mathlib, rather than with the other lemmas on the reference in Ratpoints.Proof.BruteForce.

@[simp]

theorem Ratpoints.BruteForce.pointsOfDen_nil (c : List Int) (d : Nat) (z : Int) : pointsOfDen c d z [] = []

theorem Ratpoints.BruteForce.pointsOfDen_append (c : List Int) (d : Nat) (z : Int) (xs ys : List Int) : pointsOfDen c d z (xs ++ ys) = pointsOfDen c d z xs ++ pointsOfDen c d z ys

theorem Ratpoints.BruteForce.pointsOfDen_singleton (c : List Int) (d : Nat) (z x : Int) : pointsOfDen c d z [x] = if x.gcd z = 1 then pointsAbove x z (horner (scaledCoeffs c d z) x * if d % 2 = 1 then z else 1) else []

theorem Ratpoints.BruteForce.pointsOfDen_filter (c : List Int) (d : Nat) (z : Int) (xs : List Int) (p : Int → Bool) : pointsOfDen c d z (List.filter p xs) = List.filter (fun (q : Int × Int × Int) => p q.fst) (pointsOfDen c d z xs)

Filtering the numerators by p filters the points by p of their first components, since the points of a numerator x are triples (x, y, z).

theorem Ratpoints.BruteForce.map_toList_range_eq_numerators (H : Nat) : List.map (fun (i : Nat) => ↑i - ↑H) (ForIn.toList [:2 * H + 1]) = numerators H

theorem Ratpoints.BruteForce.natAbs_le_of_mem_numerators {H : Nat} {a : Int} (h : a ∈ numerators H) : a.natAbs ≤ H

theorem Ratpoints.BruteForce.pairwise_lt_numerators (H : Nat) : List.Pairwise (fun (x1 x2 : Int) => x1 < x2) (numerators H)

The numerators -H, …, H are increasing.

The sieve of one denominator

def Ratpoints.Sieve.SieveDenInvariant (H b : Nat) (pref : List SieveEntry) (surv : Vector Bool (2 * H + 1)) : Prop

The invariant of the loop of Ratpoints.Sieve.sieveDen over the sieve entries: after the entries pref, the entry of each numerator i - H is its survivor test for them.

Equations

• Ratpoints.Sieve.SieveDenInvariant H b pref surv = ∀ (i : Nat) (hi : i < 2 * H + 1), surv[i] = Ratpoints.Sieve.survives pref b (↑i - ↑H)

def Ratpoints.Sieve.SieveDenRowInvariant (H b : Nat) (pref : List SieveEntry) (e : SieveEntry) (done : List Nat) (surv : Vector Bool (2 * H + 1)) : Prop

The invariant of the loop of Ratpoints.Sieve.sieveDen over the numerators for the sieve entry e, after the entries pref: after the positions done, the entry of each numerator i - H is its survivor test for pref followed by e if i is among them, and for pref otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem Ratpoints.Sieve.sieveDen_spec (H b : Nat) (entries : List SieveEntry) : ⦃ True ⦄ sieveDen H b entries ⦃ fun (surv : Vector Bool (2 * H + 1)) => ∀ (i : Nat) (hi : i < 2 * H + 1), surv[i] = survives entries b (↑i - ↑H) ⦄

The survivors of one denominator

def Ratpoints.Sieve.CheckDenInvariant (c : List Int) (d H b : Nat) (keep : Int → Bool) (pref : List Nat) (out : Array (Int × Int × Int)) : Prop

The invariant of the loop of Ratpoints.Sieve.checkDen over the positions: after the positions pref, the points found are those of the brute-force reference over the denominator b and the numerators i - H, i ∈ pref, that pass keep.

Equations

• Ratpoints.Sieve.CheckDenInvariant c d H b keep pref out = (out.toList = Ratpoints.BruteForce.pointsOfDen c d (↑b) (List.filter keep (List.map (fun (i : Nat) => ↑i - ↑H) pref)))

theorem Ratpoints.Sieve.checkDen_spec (c : List Int) (d H b : Nat) (surv : Vector Bool (2 * H + 1)) : ⦃ True ⦄ checkDen c d H b surv ⦃ fun (out : Array (Int × Int × Int)) => ∀ (keep : Int → Bool), (∀ (i : Nat) (hi : i < 2 * H + 1), surv[i] = keep (↑i - ↑H)) → out.toList = BruteForce.pointsOfDen c d (↑b) (List.filter keep (BruteForce.numerators H)) ⦄

The test keep of the numerators is quantified in the postcondition rather than taken as an argument, so that every argument occurs in the program and vcgen applies the contract at a call unaided.