mathlib3 documentation

number_theory.legendre_symbol.norm_num

A `norm_num` extension for Jacobi and Legendre symbols #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We extend the tactic.interactive.norm_num tactic so that it can be used to provably compute the value of the Jacobi symbol J(a | b) or the Legendre symbol legendre_sym p a when the arguments are numerals.

Implementation notes #

We use the Law of Quadratic Reciprocity for the Jacobi symbol to compute the value of J(a | b) efficiently, roughly comparable in effort with the euclidean algorithm for the computation of the gcd of a and b. More precisely, the computation is done in the following steps.

Use J(a | 0) = 1 (an artifact of the definition) and J(a | 1) = 1 to deal with corner cases.
Use J(a | b) = J(a % b | b) to reduce to the case that a is a natural number. We define a version of the Jacobi symbol restricted to natural numbers for use in the following steps; see norm_num.jacobi_sym_nat. (But we'll continue to write J(a | b) in this description.)
Remove powers of two from b. This is done via J(2a | 2b) = 0 and J(2a+1 | 2b) = J(2a+1 | b) (another artifact of the definition).
Now 0 ≤ a < b and b is odd. If b = 1, then the value is 1. If a = 0 (and b > 1), then the value is 0. Otherwise, we remove powers of two from a via J(4a | b) = J(a | b) and J(2a | b) = ±J(a | b), where the sign is determined by the residue class of b mod 8, to reduce to a odd.
Once a is odd, we use Quadratic Reciprocity (QR) in the form J(a | b) = ±J(b % a | a), where the sign is determined by the residue classes of a and b mod 4. We are then back in the previous case.

We provide customized versions of these results for the various reduction steps, where we encode the residue classes mod 2, mod 4, or mod 8 by using terms like bit1 (bit0 a). In this way, the only divisions we have to compute and prove are the ones occurring in the use of QR above.

def norm_num.jacobi_sym_nat (a b : ℕ) :

The Jacobi symbol restricted to natural numbers in both arguments.

Equations

norm_num.jacobi_sym_nat a b = jacobi_sym ↑a b

API Lemmas #

We repeat part of the API for jacobi_sym with norm_num.jacobi_sym_nat and without implicit arguments, in a form that is suitable for constructing proofs in norm_num.

theorem norm_num.jacobi_sym_nat.zero_right (a : ℕ) :

norm_num.jacobi_sym_nat a 0 = 1

Base cases: b = 0, b = 1, a = 0, a = 1.

theorem norm_num.jacobi_sym_nat.one_right (a : ℕ) :

norm_num.jacobi_sym_nat a 1 = 1

theorem norm_num.jacobi_sym_nat.zero_left_even (b : ℕ) (hb : b ≠ 0) :

norm_num.jacobi_sym_nat 0 (bit0 b) = 0

theorem norm_num.jacobi_sym_nat.zero_left_odd (b : ℕ) (hb : b ≠ 0) :

norm_num.jacobi_sym_nat 0 (bit1 b) = 0

theorem norm_num.jacobi_sym_nat.one_left_even (b : ℕ) :

norm_num.jacobi_sym_nat 1 (bit0 b) = 1

theorem norm_num.jacobi_sym_nat.one_left_odd (b : ℕ) :

norm_num.jacobi_sym_nat 1 (bit1 b) = 1

theorem norm_num.legendre_sym.to_jacobi_sym (p : ℕ) (pp : fact (nat.prime p)) (a r : ℤ) (hr : jacobi_sym a p = r) :

legendre_sym p a = r

Turn a Legendre symbol into a Jacobi symbol.

theorem norm_num.jacobi_sym.mod_left (a : ℤ) (b ab' : ℕ) (ab r b' : ℤ) (hb' : ↑b = b') (hab : a % b' = ab) (h : ↑ab' = ab) (hr : norm_num.jacobi_sym_nat ab' b = r) :

jacobi_sym a b = r

The value depends only on the residue class of a mod b.

theorem norm_num.jacobi_sym_nat.mod_left (a b ab : ℕ) (r : ℤ) (hab : a % b = ab) (hr : norm_num.jacobi_sym_nat ab b = r) :

norm_num.jacobi_sym_nat a b = r

theorem norm_num.jacobi_sym_nat.even_even (a b : ℕ) (hb₀ : b ≠ 0) :

norm_num.jacobi_sym_nat (bit0 a) (bit0 b) = 0

The symbol vanishes when both entries are even (and b ≠ 0).

theorem norm_num.jacobi_sym_nat.odd_even (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat (bit1 a) b = r) :

norm_num.jacobi_sym_nat (bit1 a) (bit0 b) = r

When a is odd and b is even, we can replace b by b / 2.

theorem norm_num.jacobi_sym_nat.double_even (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat a (bit1 b) = r) :

norm_num.jacobi_sym_nat (bit0 (bit0 a)) (bit1 b) = r

If a is divisible by 4 and b is odd, then we can remove the factor 4 from a.

theorem norm_num.jacobi_sym_nat.even_odd₁ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat a (bit1 (bit0 (bit0 b))) = r) :

norm_num.jacobi_sym_nat (bit0 a) (bit1 (bit0 (bit0 b))) = r

If a is even and b is odd, then we can remove a factor 2 from a, but we may have to change the sign, depending on b % 8. We give one version for each of the four odd residue classes mod 8.

theorem norm_num.jacobi_sym_nat.even_odd₇ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat a (bit1 (bit1 (bit1 b))) = r) :

norm_num.jacobi_sym_nat (bit0 a) (bit1 (bit1 (bit1 b))) = r

theorem norm_num.jacobi_sym_nat.even_odd₃ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat a (bit1 (bit1 (bit0 b))) = r) :

norm_num.jacobi_sym_nat (bit0 a) (bit1 (bit1 (bit0 b))) = -r

theorem norm_num.jacobi_sym_nat.even_odd₅ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat a (bit1 (bit0 (bit1 b))) = r) :

norm_num.jacobi_sym_nat (bit0 a) (bit1 (bit0 (bit1 b))) = -r

theorem norm_num.jacobi_sym_nat.qr₁ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat (bit1 b) (bit1 (bit0 a)) = r) :

norm_num.jacobi_sym_nat (bit1 (bit0 a)) (bit1 b) = r

Use quadratic reciproity to reduce to smaller b.

theorem norm_num.jacobi_sym_nat.qr₁_mod (a b ab : ℕ) (r : ℤ) (hab : bit1 b % bit1 (bit0 a) = ab) (hr : norm_num.jacobi_sym_nat ab (bit1 (bit0 a)) = r) :

norm_num.jacobi_sym_nat (bit1 (bit0 a)) (bit1 b) = r

theorem norm_num.jacobi_sym_nat.qr₁' (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat (bit1 (bit0 b)) (bit1 a) = r) :

norm_num.jacobi_sym_nat (bit1 a) (bit1 (bit0 b)) = r

theorem norm_num.jacobi_sym_nat.qr₁'_mod (a b ab : ℕ) (r : ℤ) (hab : bit1 (bit0 b) % bit1 a = ab) (hr : norm_num.jacobi_sym_nat ab (bit1 a) = r) :

norm_num.jacobi_sym_nat (bit1 a) (bit1 (bit0 b)) = r

theorem norm_num.jacobi_sym_nat.qr₃ (a b : ℕ) (r : ℤ) (hr : norm_num.jacobi_sym_nat (bit1 (bit1 b)) (bit1 (bit1 a)) = r) :

norm_num.jacobi_sym_nat (bit1 (bit1 a)) (bit1 (bit1 b)) = -r

theorem norm_num.jacobi_sym_nat.qr₃_mod (a b ab : ℕ) (r : ℤ) (hab : bit1 (bit1 b) % bit1 (bit1 a) = ab) (hr : norm_num.jacobi_sym_nat ab (bit1 (bit1 a)) = r) :

norm_num.jacobi_sym_nat (bit1 (bit1 a)) (bit1 (bit1 b)) = -r

Certified evaluation of the Jacobi symbol #

The following functions recursively evaluate a Jacobi symbol and construct the corresponding proof term.

meta def norm_num.prove_jacobi_sym_odd :

tactic.instance_cache → tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

This evaluates r := jacobi_sym_nat a b recursively using quadratic reciprocity and produces a proof term for the equality, assuming that a < b and b is odd.

meta def norm_num.prove_jacobi_sym_nat :

tactic.instance_cache → tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

This evaluates r := jacobi_sym_nat a b and produces a proof term for the equality by removing powers of 2 from b and then calling prove_jacobi_sym_odd.

meta def norm_num.prove_jacobi_sym :

tactic.instance_cache → tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × tactic.instance_cache × expr × expr)

This evaluates r := jacobi_sym a b and produces a proof term for the equality. This is done by reducing to r := jacobi_sym_nat (a % b) b.

The `norm_num` plug-in #

meta def tactic.norm_num.eval_jacobi_sym :

expr → tactic (expr × expr)

This is the norm_num plug-in that evaluates Jacobi and Legendre symbols.