zmod

Stream: Is there code for X?

[Scott Morrison]

I'm failing to find two of the most basic facts about zmod:

example (a b c : ℕ) (h : (a : zmod c) = (b : zmod c)) : a % c = b % c :=
sorry

example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
sorry

and worse, I don't seem to be able to prove them... Any help?

[Scott Morrison]

Actually, I guess it's actually the other direction I want in any case.

[Kevin Buzzard]

You want to look at modeq

[Kevin Buzzard]

That's the language the lemmas are proved in

[Patrick Massot]

(deleted)

[Scott Morrison]

But I don't want to use modeq, because it is horrible. :-) I am working with (Z/NZ) + \sqrt{3} (Z/NZ).

[Scott Morrison]

It seems like the coercion from nat to zmod isn't particularly well described in the API, so it's hard to extract information from hypotheses about these coercions.

[Kevin Buzzard]

I posted a proof of one of these the other day

[Kevin Buzzard]

I'm on mobile and don't know how to send the link but search for

Whilst proving example : (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) : (a : R) = b ↔ a ≡ b [ZMOD p] I noticed the following thing:

theorem sub_eq_zero : a - b = 0 ↔ a = b

and

theorem modeq_iff_dvd : a ≡ b [ZMOD n] ↔ (n:ℤ) ∣ b - a

One a-b, one b-a. This meant that I had to add an eq_comm in the following proof:

import number_theory.quadratic_reciprocity
import data.int.modeq

lemma thing (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
  (a : R) = b ↔ a ≡ b [ZMOD p] :=
begin
  rw eq_comm,
  rw ←sub_eq_zero,
  rw ←int.cast_sub,
  rw char_p.int_cast_eq_zero_iff R p,
  rw int.modeq.modeq_iff_dvd,
end

I think the above lemma is the correct thing to PR to mathlib (with perhaps a better proof) but this experience did make me wonder whether there should be a "convention" for the order of the subtractands when proving lemmas of this form

[Scott Morrison]

Okay, that lemma does look good.

[Scott Morrison]

It never made it into mathlib?

[Kevin Buzzard]

I certainly didn't PR it. My life is too full right now, I would PR, get a comment, and then not notice for two weeks and this is a bit annoying

[Scott Morrison]

I guess I still need to adapt it for the nat version instead of int.

[Scott Morrison]

okay, I'll see if I can include something like it

[Kevin Buzzard]

Unfortunately I use subtraction

[Kevin Buzzard]

Maybe you can start with WLOG

[Scott Morrison]

Okay,

lemma char_p.int_coe_eq_int_coe_iff (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
  (a : R) = b ↔ a ≡ b [ZMOD p] :=
begin
  rw eq_comm,
  rw ←sub_eq_zero,
  rw ←int.cast_sub,
  rw char_p.int_cast_eq_zero_iff R p,
  rw int.modeq.modeq_iff_dvd,
end

lemma zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) : (a : zmod c) = (b : zmod c) ↔ a ≡ b [ZMOD c] :=
char_p.int_coe_eq_int_coe_iff (zmod c) c a b

lemma zmod.nat_coe_eq_nat_coe_iff (a b c : ℕ) : (a : zmod c) = (b : zmod c) ↔ a ≡ b [MOD c] :=
begin
  convert zmod.int_coe_eq_int_coe_iff a b c,
  simp [nat.modeq.modeq_iff_dvd, int.modeq.modeq_iff_dvd],
end

@[simp]
lemma coe_zmod_eq_zero_iff_dvd (a b : ℕ) : (a : zmod b) = 0 ↔ b ∣ a :=
begin
  change (a : zmod b) = ((0 : ℕ) : zmod b) ↔ b ∣ a,
  rw zmod.nat_coe_eq_nat_coe_iff,
  rw nat.modeq.modeq_zero_iff,
end

starts with Kevin's lemma and deduces what I needed. (No need for wlog!). I'll bundle it all into an upcoming PR.

[Shing Tak Lam]

Here's a direct proof of your original examples?

import data.zmod.basic

example (a b c : ℕ) (h : (a : zmod c) = (b : zmod c)) : a % c = b % c :=
by rw [←zmod.val_cast_nat, ←zmod.val_cast_nat, h]

example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
by rw [nat.dvd_iff_mod_eq_zero, ←zmod.val_cast_nat, h, zmod.val_zero]

[Patrick Massot]

Could you please try to use norm_cast in all those proofs? Each proof that requires adding a norm_cast attribute benefits to future users beyond its intended use.

[Johan Commelin]

@Scott Morrison mathlib knows char_p (zmod n) n, and your questions ought to be proven for a general such R.

[Johan Commelin]

The second one is (half of) the definition of char_p:

example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
(char_p.cast_eq_zero_iff (zmod b) b a).mp h