Zulip Chat Archive

Stream: Is there code for X?

Topic: zmod


Scott Morrison (May 23 2020 at 10:25):

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 (May 23 2020 at 10:28):

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

Kevin Buzzard (May 23 2020 at 10:28):

You want to look at modeq

Kevin Buzzard (May 23 2020 at 10:28):

That's the language the lemmas are proved in

Patrick Massot (May 23 2020 at 10:29):

(deleted)

Scott Morrison (May 23 2020 at 10:30):

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

Scott Morrison (May 23 2020 at 10:31):

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 (May 23 2020 at 10:32):

I posted a proof of one of these the other day

Kevin Buzzard (May 23 2020 at 10:33):

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 (May 23 2020 at 10:34):

Okay, that lemma does look good.

Scott Morrison (May 23 2020 at 10:34):

It never made it into mathlib?

Kevin Buzzard (May 23 2020 at 10:35):

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 (May 23 2020 at 10:35):

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

Scott Morrison (May 23 2020 at 10:35):

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

Kevin Buzzard (May 23 2020 at 10:36):

Unfortunately I use subtraction

Kevin Buzzard (May 23 2020 at 10:36):

Maybe you can start with WLOG

Scott Morrison (May 23 2020 at 10:48):

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 (May 23 2020 at 11:03):

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 (May 23 2020 at 11:12):

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 (May 23 2020 at 14:36):

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

Johan Commelin (May 23 2020 at 14:39):

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

Last updated: Dec 20 2023 at 11:08 UTC