Stream: maths

Topic: legendre symbols

Johan Commelin (Apr 25 2020 at 17:26):

lemma legendre_sym_mul (a b p : ℕ) [fact p.prime] :
legendre_sym (a * b) p = legendre_sym a p * legendre_sym b p :=
by simp only [← legendre_sym_hom_apply, nat.cast_mul, (legendre_sym_hom p).map_mul]


Johan Commelin (Apr 25 2020 at 17:26):

example : legendre_sym 43 29 = -1 :=
begin
haveI : fact (nat.prime 29) := by norm_num,
haveI : fact (nat.prime  7) := by norm_num,
haveI : fact (29 % 2 = 1)   := by norm_num,
haveI : fact ( 7 % 2 = 1)   := by norm_num,
calc legendre_sym 43 29 = legendre_sym 14 29 :
by { rw [legendre_sym_mod, show 43 % 29 = 14, by norm_num] }
... = legendre_sym (2 * 7) 29 :
by { rw [show 14 = 2 * 7, by norm_num] }
... = legendre_sym 2 29 * legendre_sym 7 29 :
by { rw [legendre_sym_mul] }
... = -legendre_sym 7 29 :
by { rw [legendre_sym_two, show (-1:ℤ)^(29/4 + 29/2) = -1, by norm_num],
rw [neg_one_mul] }
... = -legendre_sym 29 7 :
by { rw [legendre_sym_swap 7 29 dec_trivial],
rw [show (-1:ℤ) ^ (7 / 2 * (29 / 2)) = 1, by norm_num, mul_one] }
... = -legendre_sym 1 7 :
by { rw [legendre_sym_mod, show 29 % 7 = 1, by norm_num] }
... = -1 :
by { rw [legendre_sym_one] }
end


Johan Commelin (Apr 25 2020 at 17:27):

But I think that we might want to refactor this a bit. Because currently we cannot talk about the Legendre symbol of x : Z_[p] with respect to p.

Alex J. Best (Apr 25 2020 at 17:57):

I was thinking exactly the same thing last week! Legendre needs a little love, but it would be cool to generalize to kronecker symbols too

Kevin Buzzard (Apr 25 2020 at 18:00):

One of the codewars questions would be a whole lot easier if we had Kronecker symbols.

Johan Commelin (Apr 25 2020 at 18:04):

variables (p : ℕ) [nat.prime p]

open polynomial

lemma foo (hp : p ≠ 2) (n : ℕ) (h : legendre_sym n p = 1) : ∃ (x : ℤ_[p]), x^2 = n :=
begin
letI _hp : fact p.prime := ‹p.prime›,
by_cases hn : (n : zmod p) = 0,
{ rw ← legendre_sym_eq_zero_iff at hn,
rw hn at h,
exact absurd h zero_ne_one },
rw [legendre_sym_eq_one_iff p hn] at h,
rcases h with ⟨x, hx⟩,
rcases zmod.nat_cast_surjective x with ⟨k, rfl⟩,
let f : polynomial ℤ_[p] := X^2 - C n,
rcases @hensels_lemma p _ f k _ with ⟨x, hx, H⟩,
{ refine ⟨x, _⟩,
simpa only [sub_eq_zero, eval_C, eval_X, eval_pow, eval_sub] using hx, },
simp only [f],
simp only [eval_C, eval_X, eval_pow, eval_sub],
sorry
end


Kevin Buzzard (Apr 25 2020 at 18:04):

When I took over teaching Imperial's basic number theory course just after I was employed there, the lecture notes handed to me contained this glorious fact that (2/p)=(-1)^{(p^2-1)/8}; I see Chris has found some simpler trick involving p/4+p/2 but I was convinced that the students would rather be told that (2/p) is +1 if p=1 or 7 mod 8, and -1 if it's 3 or 5 mod 8. Similarly for this (p/q)(q/p)=(-1)^{p/2*q/2} result. Isn't it better to just reduce things mod 4 than to be working out 7/2*29/2? Unfortunately I can't make a PR because I already have a very complicated one about de Morgan's laws on the pile.

Johan Commelin (Apr 25 2020 at 18:04):

Unfortunately the final sorry is out of reach for the time being

Kevin Buzzard (Apr 25 2020 at 18:05):

Johan Commelin said:

Unfortunately the final sorry is out of reach for the time being

Are you kidding??

Johan Commelin (Apr 25 2020 at 18:05):

padic_norm has no connection with zmod p at the moment

Johan Commelin (Apr 25 2020 at 18:05):

Hensels lemma doesn't mention finite fields in Lean

Johan Commelin (Apr 25 2020 at 18:06):

We really need Henselian rings, and 7 different versions of Hensel's lemma

Kevin Buzzard (Apr 25 2020 at 18:06):

Ashwin started on DVR's, at least.

Alex J. Best (Apr 26 2020 at 01:47):

@Johan Commelin I was inspired by your legendre calculation and the idea of having a legendre tactic to run through and calculate a symbol automatically (and then a ternary quadratic form tatic or something lol), so I made a PR to do one line of your proof automatically :upside_down: rewriting 14=2*7 without thinking. #2536.

Johan Commelin (Apr 26 2020 at 03:37):

Nice! I had recently been thinking about how to hook up more general computations. The vague idea that I had was:

• introduce a class compute foo
• add instances of compute fib and compute legendre_sym that "explain" how to compute these functions
• make the norm_num tactic aware of this class

Now the hard part is to figure out what "explain" means. @Mario Carneiro @Simon Hudon do you have any ideas on how this could work?

Yury G. Kudryashov (Apr 26 2020 at 03:44):

Probably it should return the answer and a proof of correctness.

Mario Carneiro (Apr 26 2020 at 03:44):

My plan has been to use a def_replacer for norm_num so that you can dynamically add more disjuncts to https://github.com/leanprover-community/mathlib/blob/master/src/tactic/norm_num.lean#L450-L451

Mario Carneiro (Apr 26 2020 at 03:46):

So for instance you could write something like eval_prime there in the file on primes instead of inside norm_num itself, and this tactic can do whatever trickery it needs to to efficiently compute the result

Mario Carneiro (Apr 26 2020 at 03:46):

It's not just constrained to being an evaluator, although for a lot of functions that's probably what you would do

Johan Commelin (Apr 26 2020 at 03:52):

Would there be a dumbed down API method for people who are not very good at tactic writing?

Mario Carneiro (Apr 26 2020 at 03:53):

I think the easy version is that you first match on the expr you are looking for (e.g. (prime %%e)), then use a quick tactic script to rewrite with the definition and call norm_num on what remains

Mario Carneiro (Apr 26 2020 at 03:53):

which will wind up calling this function again recursively if you aren't done yet

Mario Carneiro (Apr 26 2020 at 03:54):

Alternatively, you run the function externally (in the tactic/VM), then construct the result numeral and hope that rfl works as a proof

Mario Carneiro (Apr 26 2020 at 03:56):

But to really have the desired dumbed down API we need the cbv tactic

Mario Carneiro (Apr 26 2020 at 03:57):

and that probably has to be implemented in core

Bryan Gin-ge Chen (Apr 26 2020 at 04:00):

What would we need to make cbv happen? Could you write a roadmap?

Mario Carneiro (Apr 26 2020 at 04:01):

Basically it is a tactic that performs the same operation as #reduce but with proofs

Mario Carneiro (Apr 26 2020 at 04:01):

I think it needs to be implemented in C++ for efficiency

Mario Carneiro (Apr 26 2020 at 04:02):

It is more or less simp [all equation lemmas]

Mario Carneiro (Apr 26 2020 at 04:04):

The name comes from a tactic with this behavior in Coq, but admittedly I don't know that much about how it works, what kinds of things cause it to stop and so on

Mario Carneiro (Apr 26 2020 at 04:04):

You don't want to completely reduce the term to normal form because it will get unreadable long before then

Bryan Gin-ge Chen (Apr 26 2020 at 04:19):

I found the doc page on the Coq tactic. Is it like dsimp but with more control?

Markus Himmel (Apr 26 2020 at 07:31):

Regarding computing legendre symbols: Maybe it would be easier to teach norm_num how to evaluate 29^14 in zmod p` and use Euler's criterion? This should certainly be much more computationally efficient for computing large legendre symbols.

David Wärn (Apr 26 2020 at 08:20):

I don't know if this helps, but there's also a simple & efficient algorithm to compute large Legendre symbols using QR: https://en.wikipedia.org/wiki/Jacobi_symbol#Calculating_the_Jacobi_symbol

Alex J. Best (Apr 26 2020 at 08:30):

Right the quadratic reciprocity one is what I had in mind, it's what I would do by hand. I don't know what the runtime of exponentiating and using eulers criterion is but it seems like it should be harder to take exponentials, even if you do it in a smart way (but it is easiest to implement).

David Wärn (Apr 26 2020 at 08:49):

Both should be polynomial in the number of digits, but exponentiation needs lots of expensive multiplications / remainders

Mario Carneiro (Apr 26 2020 at 08:58):

keep in mind that the asymptotic analysis in the books isn't quite correct for theorem provers. Division / modulus are exactly as expensive as multiplication + addition, because it's the same proof

Mario Carneiro (Apr 26 2020 at 08:59):

Unfortunately the literature is much sparser on what the best bounds are for nondeterministic TMs

Kevin Buzzard (Apr 26 2020 at 09:23):

The standard algorithm using QR will be super-fast in practice as long as there's an efficient division with remainder algorithm, and will also compute Jacobi symbols (note that it needs no factoring either, just casting out powers of 2). The p^(q-1)/2 approach leaves you having to do multiplications mod q which might really hurt if q has 100 digits, and doesn't work for Jacobi symbols because it relies on the units being cyclic

what's qt?

did you mean qr?

Kevin Buzzard (Apr 26 2020 at 09:25):

Sorry, phone autocorrect

Last updated: May 18 2021 at 07:19 UTC