Converting Between ℕ and ℤ in Modular Arithmetic

Stream: general

[Kajani Kaunda]

@[deprecated Int.natCast_modEq_iff]
theorem Int.coe_nat_modEq_iff{a : ℕ} {b : ℕ} {n : ℕ} :
↑a ≡ ↑b [ZMOD ↑n] ↔ a ≡ b [MOD n]

The above theorem may be used to move between modular equivalences in natural numbers (MOD n) and integers (ZMOD ↑n), ensuring that the results are consistent across both domains. But then i see that it has been deprecated. So what is the new preferred way of handling this situation?

My specific use case is where I coerced a variable p defined as type N to type Z in order to prove some result, which worked:

have hpp' (h00 : (↑p : ℤ) ≡ 2 [PMOD 6]) : (↑p - 2 : ℤ) ≡ 0 [PMOD 6] := AddCommGroup.sub_modEq_zero.mpr h00

But now this subsequent line of code does not work:

obtain ⟨k, hk⟩ := Nat.dvd_of_mod_eq_zero hpp'

It only works if hpp' is defined like this:

have hpp' : p - 2 ≡ 0 [MOD 6] := by sorry

That's why I was thinking or reversing the coercion of p. But my reasoning feels very painful and convoluted - and wrong! I think working exclusively with either Z or N types is the cleaner and preferred approach. Any help please!

My minimum working example is as follows:

import Mathlib
import Mathlib.Algebra.Group.Defs
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Int.ModEq

lemma lemma_4_2 (p : ℕ) (hprime : Nat.Prime p) (hpg3 : p > 3)  :
    ∃ n, p = 6 * n + 1 ∨ p = 6 * n - 1 := by
  by_contra! hneg
  mod_cases hp : p % 6
  {
    -- Case p % 6 = 0: p is divisible by 6
    obtain ⟨k, hk⟩ := Nat.dvd_of_mod_eq_zero hp
    have hp : 3 * (2*k) = p := by
      rw [←mul_assoc]
      exact hk.symm
    apply Nat.not_prime_mul' hp
    · norm_num
    · omega
    · exact hprime
  }
  {
    -- Case p % 6 = 1: this will lead to a contradiction in the next steps
    sorry
  }
  {
    have hpp' (h00 : (↑p : ℤ) ≡ 2 [PMOD 6]) : (↑p - 2 : ℤ) ≡ 0 [PMOD 6] :=
      AddCommGroup.sub_modEq_zero.mpr h00

    --TEST
    have hph : p - 2 ≡ 0 [MOD 6] := by sorry
    --TEST

    -- Convert the result back to natural numbers (if p is a natural number)
    -- have hpp_nat : (p - 2) ≡ 0 [MOD 6] := by exact SOME_MAGIC_TACTIC hpp'

    obtain ⟨k, hk⟩ := Nat.dvd_of_mod_eq_zero hpp' -- OK hph
    have hkp : 2 * (3*k + 1) = p := by
      rw [mul_add, ←mul_assoc, mul_one]
      convert hk.symm using 0
      omega
    apply Nat.not_prime_mul' hkp
    · norm_num
    · omega
    · exact hprime

  }
  {
    -- Case p % 6 = 3
    have hp' : p - 3 ≡ 0 [MOD 6] := by
      sorry
    obtain ⟨k, hk⟩ := Nat.dvd_of_mod_eq_zero hp'
    have hkp : 3 * (2*k + 1) = p := by
      rw [mul_add, ←mul_assoc, mul_one]
      convert hk.symm using 0
      omega
    apply Nat.not_prime_mul' hkp
    · norm_num
    · omega
    · exact hprime
  }
  {
    -- Case p % 6 = 4: to be handled next
    sorry
  }
  {
    -- Case p % 6 = 5: to be handled next
    sorry
  }

[Kevin Buzzard]

docs#Int.coe_nat_modEq_iff

[Kevin Buzzard]

It's now called Int.natCast_modEq_iff.

[Kajani Kaunda]

Kevin Buzzard said:

It's now called Int.natCast_modEq_iff.

Ah! Ok Thank you so much for that!