match case by mod remainder

Stream: new members

[mdnestor]

I have the following proof that argues by cases on the remainder of n % 2. Is there a better way to do this? note I could also do if n%2 = 0 then () else () but I want it to work for divisors larger than 2 and avoid nested if statements.

example (n: Nat) (h: n^2 % 2 = 0): n % 2 = 0 := by
  match hm: n % 2 with
  | 0 => sorry
  | 1 => sorry
  | k + 2 =>
    have _ : ¬n % 2 < 2 := by simp [hm]
    have _ : n % 2 < 2 := by apply Nat.mod_lt; decide
    contradiction

[Michael Stoll]

You could try fin_cases (n : ZMod 2)...

[mdnestor]

That works. I wanted to avoid imports, but this is still pretty good:

import Mathlib.Data.ZMod.Defs

example (n: Nat) (h: n^2 % 2 = 0): n % 2 = 0 := by
  match hn: (n: ZMod 2) with
  | 0 => sorry
  | 1 => sorry

[Michael Stoll]

Usually, it is a good idea to work with ZMod k instead of with remainders n % k. For example,

import Mathlib.Data.ZMod.Basic

theorem foo : ∀ (n : ZMod 2), n ^ 2 = 0 → n = 0 := by decide

example (n : Nat) (h : n ^ 2 % 2 = 0): n % 2 = 0 := by
  rw [← Nat.dvd_iff_mod_eq_zero, ← ZMod.natCast_zmod_eq_zero_iff_dvd] at h ⊢
  push_cast at h
  exact foo (↑n) h

Note that statements about ZMod k with a concrete k can usually be proved by decide.

[mdnestor]

where is the equivalent of Nat.div_add_mod for ZMod?

[Michael Stoll]

docs#ZMod.natCast_mod ?