Zulip Chat Archive

Stream: Is there code for X?

Topic: zmod


view this post on Zulip 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?

view this post on Zulip Scott Morrison (May 23 2020 at 10:28):

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

view this post on Zulip Kevin Buzzard (May 23 2020 at 10:28):

You want to look at modeq

view this post on Zulip Kevin Buzzard (May 23 2020 at 10:28):

That's the language the lemmas are proved in

view this post on Zulip Patrick Massot (May 23 2020 at 10:29):

(deleted)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 23 2020 at 10:32):

I posted a proof of one of these the other day

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 23 2020 at 10:34):

Okay, that lemma does look good.

view this post on Zulip Scott Morrison (May 23 2020 at 10:34):

It never made it into mathlib?

view this post on Zulip 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

view this post on Zulip Scott Morrison (May 23 2020 at 10:35):

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

view this post on Zulip Scott Morrison (May 23 2020 at 10:35):

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

view this post on Zulip Kevin Buzzard (May 23 2020 at 10:36):

Unfortunately I use subtraction

view this post on Zulip Kevin Buzzard (May 23 2020 at 10:36):

Maybe you can start with WLOG

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: May 17 2021 at 16:26 UTC