eq_iff_modeq_int

Stream: Is there code for X?

[Kevin Buzzard]

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?

[Chris Hughes]

It's about characteristic n now

[Kevin Buzzard]

I need to learn about char_p?

[Patrick Massot]

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

[Kevin Buzzard]

But n isn't prime!

[Kevin Buzzard]

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]

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Mario Carneiro]

@Johan Commelin you deleted a lemma? shame on you

[Johan Commelin]

Did I? Where? When?

[Mario Carneiro]

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

[Johan Commelin]

Oops

[Kevin Buzzard]

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.

[Johan Commelin]

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

[Johan Commelin]

My apologies

[Kevin Buzzard]

Johan is saying that we have a better lemma somewhere now

[Johan Commelin]

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

[Johan Commelin]

I think I messed up

[Johan Commelin]

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

[Reid Barton]

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

[Kevin Buzzard]

exactly

[Kevin Buzzard]

/me deletes all of his Lean repos other than mathlib

[Patrick Massot]

Noooo!

[Patrick Massot]

Fortunately git is decentralized

[Johan Commelin]

The perfectoid repo is on the community account

[Kevin Buzzard]

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.

[Johan Commelin]

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?

[Kevin Buzzard]

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

[Johan Commelin]

Ok, I'll do it.

[Kevin Buzzard]

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

[Johan Commelin]

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...

[Kenny Lau]

have we fixed wlog?

[Johan Commelin]

No, I don't think so.

[Johan Commelin]

But that's not the hard part (-;

[Johan Commelin]

I can easily work aroun wlog, of course

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

Hmm... thanks for keeping me honest.

[Johan Commelin]

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