legendre symbols

Stream: maths

[Johan Commelin]

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]

https://github.com/leanprover-community/mathlib/blob/legendre-sym-mul/src/number_theory/quadratic_reciprocity.lean#L562

[Johan Commelin]

Which leads to

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]

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]

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]

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

[Johan Commelin]

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],
  simp only [pow_two, sub_eq_add_neg],
  simp only [eval_X, add_assoc, derivative_X, mul_one, derivative_add, derivative_mul, one_mul, eval_add],
  sorry
end

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Johan Commelin said:

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

Are you kidding??

[Johan Commelin]

padic_norm has no connection with zmod p at the moment

[Johan Commelin]

Hensels lemma doesn't mention finite fields in Lean

[Johan Commelin]

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

[Kevin Buzzard]

Ashwin started on DVR's, at least.

[Alex J. Best]

@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]

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]

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

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

and that probably has to be implemented in core

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

It is more or less simp [all equation lemmas]

[Mario Carneiro]

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]

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

[Bryan Gin-ge Chen]

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

[Markus Himmel]

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]

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]

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]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

what's qt?

[Mario Carneiro]

did you mean qr?

[Kevin Buzzard]

Sorry, phone autocorrect