forgot how to do basic modular arithmetic

Stream: new members

[rzeta0]

It's been at least a year since I last looked at Lean and I've forgotten how to do simple modular arithmetic.

(It may be that when I last looked vanilla Lean didn't do it, and the Mechanics of Proof course had its own locally defined tactics?)

The following is the minimal code I'm trying to get working:

import Mathlib.Tactic

-- minimal example
example : 5 % 3 = 2 := by norm_num

-- minimal example
example : 5 ≡ 2 [ZMOD 3] := by norm_num

-- problematic example
example (n : ℤ): n + 1 ≡ 2 [ZMOD n - 1] := by
  calc
    n + 1 ≡ n + 1 - (n - 1) [ZMOD n-1] := by ?
    _ ≡ 2 [ZMOD n-1] := by ring

-- problematic example
example (n : ℤ): n + 1 ≡ 2 [ZMOD n - 1] := by
  dsimp [Int.ModEq] at *
  calc
    n + 1 % (n - 1) = n + 1 - (n - 1) % (n - 1) := by ring ??
    _ = 2 % (n - 1) := by ring ??

The dsimp appears to unfold the ZMOD into % notation, but even then I can't find the right tactics to justify similar proof steps.

[Snir Broshi]

The 2nd example is missing parentheses in the first calc step

[Aaron Liu]

@loogle _ ≡ (_ - _) [ZMOD _]

[loogle]

:search: Int.modEq_sub_modulus_iff, Int.ModEq.sub_left, and 3 more

[Aaron Liu]

@loogle (_ - _ : Int) % _

[loogle]

:search: Int.sub_emod, Int.sub_emod_right, and 18 more

[Aaron Liu]

import Mathlib.Tactic

-- minimal example
example : 5 % 3 = 2 := by norm_num

-- minimal example
example : 5 ≡ 2 [ZMOD 3] := by norm_num

-- problematic example
example (n : ℤ): n + 1 ≡ 2 [ZMOD n - 1] := by
  calc
    n + 1 ≡ n + 1 - (n - 1) [ZMOD n-1] := by rw [Int.modEq_sub_modulus_iff]
    _ ≡ 2 [ZMOD n-1] := by simp

-- problematic example
example (n : ℤ): n + 1 ≡ 2 [ZMOD n - 1] := by
  dsimp [Int.ModEq] at *
  calc
    (n + 1) % (n - 1) = (n + 1 - (n - 1)) % (n - 1) := by rw [Int.sub_emod]; simp
    _ = 2 % (n - 1) := congr($(by ring) % (n - 1))

[Snir Broshi]

I got

example (n : ℤ): n + 1 ≡ 2 [ZMOD n - 1] := by
  rw [show n + 1 = (n - 1) + 2 by lia]
  exact Int.modEq_modulus_add_iff.mpr rfl |>.symm

[rzeta0]

thanks everyone who replied - that's very helpful.