Recommended way to create Finsets over ZMod

Stream: general

[Adam Kurkiewicz]

I'd like to work with Finsets with elements in ZMod p. But I'm struggling to create them in the first place.

For example, the first two statements typecheck, but the third one doesn't due to lack of Preorder (which is fair).

Is there some clever syntax like python's list comprehension or something similar that would first allow me to create a Finset in Nat and then lift it to ZMod?

import Mathlib.Tactic

#check (Finset.Icc (1 : ℕ) 4)

#eval (Finset.Icc (1 : ℕ) 4).prod (λ x => (x : (ZMod 5)))

#check (Finset.Icc (1 : (ZMod 5)) (4 : (ZMod 5)))

[Ruben Van de Velde]

#eval Finset.Icc 1 3 |>.image ((↑) : ℕ → ZMod 5) -- {1, 2, 3}

[Adam Kurkiewicz]

Perfect, image is the function I've been searching for. Thank you Ruben!

[Adam Kurkiewicz]

And how can I prove the following? Neither norm_num nor reduce_mod_char make any progress:

import Mathlib.Tactic

lemma ZMod_cast_sub (a : ℕ) (p : ℕ) (a_lt_p : a < p) (pprime: p.Prime) : - @Nat.cast (ZMod p) Semiring.toNatCast (p - a) = a := by
  norm_num
  reduce_mod_char
  sorry

[Kevin Buzzard]

My first thought is: how did you get into that mess in the first place?

[Adam Kurkiewicz]

lemma upper_half_factorial_is_lower_half_factorial (p : ℕ) (pprime: p.Prime) (p_mod_4 : ((p : (ZMod 4)) = 1)):
  (Finset.Icc 1 ((p - 1)/2)).image (λ (x : ℕ) => (x : (ZMod p)))
      = (Finset.Icc ((p + 1)/2) (p - 1)).image (λ (x : ℕ) => (-x : (ZMod p))) := by
  have term_equality : ∀ k, (((p - k) : ZMod p) * (2⁻¹ : ZMod p)) = -((p + k : ZMod p) * (2⁻¹ : ZMod p)) := by
      norm_num
  ext x
  constructor
  intro left
  simp_all only [CharP.cast_eq_zero, zero_sub, neg_mul, zero_add, implies_true, Finset.mem_image, Finset.mem_Icc]
  obtain ⟨a, ⟨H1, H2⟩⟩ := left
  use (p - a)
  constructor
  omega
  rw [← H2]
  have : (a < p) := by sorry
  sorry
  intro left
  simp_all
  obtain ⟨a, ⟨⟨H1, H2⟩, H3⟩⟩ := left
  use (p - a)
  constructor
  constructor
  sorry
  sorry
  have := ZMod_cast_sub

  sorry

[Adam Kurkiewicz]

I know that a < p is not always true, but I can always pick a k large enough that a < k * p

[Adam Kurkiewicz]

I think it's a common trick in elementary number theory, to use the fact that (p - 1)/2 factorial squared is equal to -1 mod p when p - 1 is divisible by 4.

[Adam Kurkiewicz]

I need it specifically for IMO 2008 N6 shortlist problem, which gives a weak bound on largest prime divisors of $n^2 + 1$:

https://www.imo-official.org/problems/IMO2008SL.pdf

[Daniel Weber]

You can use docs#Nat.cast_sub

import Mathlib.Tactic

lemma ZMod_cast_sub (a : ℕ) (p : ℕ) (a_lt_p : a < p) : - @Nat.cast (ZMod p) Semiring.toNatCast (p - a) = a := by
  simp [Nat.cast_sub a_lt_p.le]

[Adam Kurkiewicz]

Fantastic, thank you Daniel!