Different behavior in norm_num and #eval

Stream: mathlib4

[Thomas Zhu]

This works instantly:

import Mathlib.Tactic.NormNum.LegendreSymbol

open NumberTheorySymbols

example : J(21234 | 2512349331023485) = 1 := by norm_num

but this takes forever:

#eval J(21234 | 2512349331023485)

Why isn't jacobiSym evaluation like in Mathlib.Tactic.NormNum.LegendreSymbol defined as also a csimp rule? I am writing some primality tests and do need a fast computation for jacobiSym. Is there a way to do that currently, using what we have in Mathlib.Tactic.NormNum.LegendreSymbol?

[Michael Stoll]

Because nobody did it so far.

[Michael Stoll]

It should be quite possible to use the algorithm behind the norm_num extension for Jacobi symbols for implementing a reasonably fast function that computes it (it is more or less the euclidean algorithm with some minor twists to deal with powers of two, and one has to keep track of the sign). But so far, nobody has expressed a need for it.

[Thomas Zhu]

Thank you, I just wanted to check I'm not missing something existing in mathlib.

[Michael Stoll]

(The definition is based on factorization and Legendre symbols, so it is perhaps not surprising that #eval is slow.)

[Kyle Miller]

You can use #norm_num by the way rather than #eval

[Kyle Miller]

but that doesn't help needing to do the computations at runtime inside another program, unless you set up some things.