Zulip Chat Archive

Stream: Is there code for X?

Topic: eq_iff_modeq_int


view this post on Zulip Kevin Buzzard (May 16 2020 at 16:48):

lemma eq_iff_modeq_int {n : ℕ+} {a b : } : (a : zmod n) = b  a  b [ZMOD (n : )] := ...

I'm fixing up some old codewars kata and I find that this has disappeared from the library, in #2511. I need (a : zmod n) = b -> a % n = b % n`. How am I supposed to get that now?

view this post on Zulip Chris Hughes (May 16 2020 at 17:08):

It's about characteristic n now

view this post on Zulip Kevin Buzzard (May 16 2020 at 17:14):

I need to learn about char_p?

view this post on Zulip Patrick Massot (May 16 2020 at 17:14):

No you don't, because you already learned it for the perfectoid project.

view this post on Zulip Kevin Buzzard (May 16 2020 at 17:22):

But n isn't prime!

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:07):

lemma eq_iff_modeq_int {n : } {a b : } : (a : zmod n) = b  a  b [ZMOD (n : )] :=
by rw [eq_comm, sub_eq_zero, int.cast_sub, char_p.int_cast_eq_zero_iff (zmod n) n, int.modeq.modeq_iff_dvd]

view this post on Zulip Johan Commelin (May 16 2020 at 19:08):

But this doesn't use zmod n in an essential way, right?

view this post on Zulip Johan Commelin (May 16 2020 at 19:09):

So it should be a lemma about arbitrary R with char_p R n

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:09):

All I care about is that my kata is compiling again right now

view this post on Zulip Mario Carneiro (May 16 2020 at 20:00):

@Johan Commelin you deleted a lemma? shame on you

view this post on Zulip Johan Commelin (May 16 2020 at 20:00):

Did I? Where? When?

view this post on Zulip Mario Carneiro (May 16 2020 at 20:01):

This was a lemma before the refactor, I can't find it now

view this post on Zulip Johan Commelin (May 16 2020 at 20:01):

Oops

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:02):

eq_zero_iff_dvd_int got renamed to char_p.int_cast_eq_zero_iff and a similar story for nat, but the lemma in question just seemed to vanish completely.

view this post on Zulip Johan Commelin (May 16 2020 at 20:02):

I see... I guess I messed up with porting some of the zmodp stuff to zmod p.

view this post on Zulip Johan Commelin (May 16 2020 at 20:02):

My apologies

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:03):

Johan is saying that we have a better lemma somewhere now

view this post on Zulip Johan Commelin (May 16 2020 at 20:03):

Hmm... except that maybe we don't have it...

view this post on Zulip Johan Commelin (May 16 2020 at 20:03):

I think I messed up

view this post on Zulip Johan Commelin (May 16 2020 at 20:06):

I will try to restore stuff next week... now I first need to rest.

view this post on Zulip Reid Barton (May 16 2020 at 20:07):

This is what you get for not PRing your katas to mathlib

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:08):

exactly

view this post on Zulip Kevin Buzzard (May 16 2020 at 20:08):

/me deletes all of his Lean repos other than mathlib

view this post on Zulip Patrick Massot (May 16 2020 at 20:09):

Noooo!

view this post on Zulip Patrick Massot (May 16 2020 at 20:09):

Fortunately git is decentralized

view this post on Zulip Johan Commelin (May 16 2020 at 20:09):

The perfectoid repo is on the community account

view this post on Zulip Kevin Buzzard (May 17 2020 at 10:53):

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 Johan Commelin (May 18 2020 at 12:09):

I think the trouble with my refactor PR was that I completely rewrote the API for zmod. Hence a lot of auxilliary lemmas no longer made sense, or weren't needed. I guess this lemma was collateral damage. My apologies.
@Kevin Buzzard Do you want to PR it, or shall I do it?

view this post on Zulip Kevin Buzzard (May 18 2020 at 12:37):

I don't want to PR it, my PR's usually have to go through a few iterations and I am not looking at the mathlib github site at all at the minute

view this post on Zulip Johan Commelin (May 18 2020 at 12:49):

Ok, I'll do it.

view this post on Zulip Kevin Buzzard (May 18 2020 at 12:49):

Thanks. I'm trying to get another Lean post-doc and time is tight :-)

view this post on Zulip Johan Commelin (May 18 2020 at 13:33):

Is there a slick way of proving

import algebra.char_p
import data.int.modeq

lemma eq_iff_modeq (R : Type*) [semiring R] (p : ) [char_p R p] (a b : ) :
  (a : R) = b  a  b [MOD p] :=
begin
  wlog h : a  b,
  obtain k, rfl := nat.exists_eq_add_of_le h,
  rw [nat.modeq.modeq_iff_dvd' h,  char_p.cast_eq_zero_iff R p,
    nat.add_sub_cancel_left, nat.cast_add],
end

Currently I can only think of going through zmod p...

view this post on Zulip Kenny Lau (May 18 2020 at 13:35):

have we fixed wlog?

view this post on Zulip Johan Commelin (May 18 2020 at 13:37):

No, I don't think so.

view this post on Zulip Johan Commelin (May 18 2020 at 13:37):

But that's not the hard part (-;

view this post on Zulip Johan Commelin (May 18 2020 at 13:37):

I can easily work aroun wlog, of course

view this post on Zulip Johan Commelin (May 18 2020 at 13:37):

Note that in this particular case it isn't slow (for a human)

view this post on Zulip Kenny Lau (May 18 2020 at 13:44):

import algebra.char_p
import data.int.modeq

set_option profiler true

-- elaboration of eq_iff_modeq took 1.41s
lemma eq_iff_modeq (R : Type*) [semiring R] (p : ) [char_p R p] (a b : ) :
  (a : R) = b  a  b [MOD p] :=
begin
  wlog h : a  b,
  obtain k, rfl := nat.exists_eq_add_of_le h,
  rw [nat.modeq.modeq_iff_dvd' h,  char_p.cast_eq_zero_iff R p,
    nat.add_sub_cancel_left, nat.cast_add],
end

-- elaboration of eq_iff_modeq' took 222ms
lemma eq_iff_modeq' (R : Type*) [semiring R] (p : ) [char_p R p] (a b : ) :
  (a : R) = b  a  b [MOD p] :=
begin
  wlog h : a  b := le_total a b using [a b, b a] tactic.skip,
  swap, { rwa [eq_comm, nat.modeq, @eq_comm _ (a % p)] },
  obtain k, rfl := nat.exists_eq_add_of_le h,
  rw [nat.modeq.modeq_iff_dvd' h,  char_p.cast_eq_zero_iff R p,
    nat.add_sub_cancel_left, nat.cast_add],
end

view this post on Zulip Johan Commelin (May 18 2020 at 14:03):

Hmm... thanks for keeping me honest.

view this post on Zulip Johan Commelin (May 18 2020 at 14:04):

It seems that my hardware is 3 times as fast... so I didn't really notice


Last updated: May 17 2021 at 15:13 UTC