The valuation of an integer at a prime

The loop of Ratpoints.Setup.valuation, repeated division with remainder, gives for n ≠ 0 and p > 1 an exponent v and the remainder r ≠ 0 with |n| = p ^ v m and m mod p = r: the p-adic valuation of |n| and the unit part of |n| modulo p.

Main statements

• Ratpoints.Setup.valuation_spec: for p > 1 the loop ends with |n| = p ^ v m and m mod p = r ≠ 0, and with (Ratpoints.veryBig, 0) for n = 0; Ratpoints.Setup.exists_eq_run_valuation states this for n ≠ 0 without the program logic, with p ∤ m, and Ratpoints.Setup.exists_eq_of_eq_run_valuation for a natural number w ≠ 0, as w = p ^ v m with p ∤ m.
• Ratpoints.Setup.fst_run_valuation: for p > 1 and n ≠ 0, the valuation is padicValNat p |n|.

Implementation notes

The contract is proved with vcgen, the program logic of Lean core, with a loop invariant that is a named definition, in a file with Mathlib, since the valuation of the C code is Mathlib's padicValNat. Ratpoints.Setup.valuation_value gives the result as its own value, for the contracts of the loops that bind it and read it through the plain statements.

def Ratpoints.Setup.ValuationInvariant (n : ℤ) (p : ℕ) : Std.WP.WhileInvariant (ℕ × ℕ × ℕ) Prop

The invariant of the loop of Ratpoints.Setup.valuation on n and p, on the quotient q, the remainder r and the count v: |n| = p ^ v (p q + r) with r < p, and r ≠ 0 at the exit.

Equations

• Ratpoints.Setup.ValuationInvariant n p = Std.WP.WhileInvariant.mk fun (exit : Bool) (s : ℕ × ℕ × ℕ) => n.natAbs = p ^ s.2.2 * (p * s.1 + s.2.1) ∧ s.2.1 < p ∧ (exit = true → s.2.1 ≠ 0)

theorem Ratpoints.Setup.valuationInvariant_div_mod {n : ℤ} {p : ℕ} (hp : 1 < p) : ValuationInvariant n p false (n.natAbs / p, n.natAbs % p, 0)

theorem Ratpoints.Setup.ValuationInvariant.add_one {n : ℤ} {p q r v mb : ℕ} (hp : 1 < p) (hn : n ≠ 0) (h : q = mb ∧ ValuationInvariant n p false (q, r, v)) (hr : (r == 0) = true) : q / p < mb ∧ ValuationInvariant n p false (q / p, q % p, v + 1)

theorem Ratpoints.Setup.ValuationInvariant.exit {n : ℤ} {p q r v mb : ℕ} (h : q = mb ∧ ValuationInvariant n p false (q, r, v)) (hr : ¬(r == 0) = true) : ValuationInvariant n p true (q, r, v)

theorem Ratpoints.Setup.ValuationInvariant.exists_eq {n : ℤ} {p q r v : ℕ} (h : ValuationInvariant n p true (q, r, v)) : ∃ (m : ℕ), n.natAbs = p ^ v * m ∧ m % p = r ∧ r ≠ 0

theorem Ratpoints.Setup.valuation_spec (n : ℤ) (p : ℕ) : ⦃ 1 < p ⦄ valuation n p ⦃ fun (r : ℕ × ℕ) => n = 0 ∧ r = (veryBig, 0) ∨ n ≠ 0 ∧ ∃ (m : ℕ), n.natAbs = p ^ r.1 * m ∧ m % p = r.2 ∧ r.2 ≠ 0 ⦄

The loop ends, since the quotient drops with every pass while the remainder is 0, |n| being p ^ v times a positive multiple of p; for p = 1 and n ≠ 0 it would not.

theorem Ratpoints.Setup.valuation_value (n : ℤ) (p : ℕ) : ⦃ True ⦄ valuation n p ⦃ fun (r : ℕ × ℕ) => r = (valuation n p).run ⦄

The result of Ratpoints.Setup.valuation as its own value, for the contracts of the loops that bind it and read it through Ratpoints.Setup.exists_eq_run_valuation and its corollaries.

theorem Ratpoints.Setup.exists_eq_run_valuation {n : ℤ} (hn : n ≠ 0) {p : ℕ} (hp : 1 < p) : ∃ (m : ℕ), n.natAbs = p ^ (valuation n p).run.1 * m ∧ m % p = (valuation n p).run.2 ∧ ¬p ∣ m

Ratpoints.Setup.valuation_spec for n ≠ 0 as a plain statement, which the proofs use without the program logic, with p ∤ m for the remainder ≠ 0.

theorem Ratpoints.Setup.fst_run_valuation {n : ℤ} (hn : n ≠ 0) {p : ℕ} (hp : 1 < p) : (valuation n p).run.1 = padicValNat p n.natAbs

theorem Ratpoints.Setup.exists_eq_of_eq_run_valuation {w v r p : ℕ} (hw : w ≠ 0) (hp : 1 < p) (hv : (v, r) = (valuation (↑w) p).run) : ∃ (m : ℕ), w = p ^ v * m ∧ ¬p ∣ m

The valuation of a natural number w ≠ 0 at p > 1 by Ratpoints.Setup.valuation, in the form in which a loop that binds its result reads it: w = p ^ v m with p ∤ m.