A norm_num extension for Jacobi and Legendre symbols #
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.
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.