ZMod lemma

Stream: Is there code for X?

[Patrick Massot]

Another one before I go to bed:

import Mathlib.Data.ZMod.Basic

example (n : ℕ) (r : ℤ) : ∃ k : ℤ, ((r : ZMod n) : ℤ) = r + k*n := sorry

[Timo Carlin-Burns]

import Mathlib.Data.ZMod.Basic

lemma Int.mod_eq (n m : ℤ) : n % m = n - (n / m) * m := by
  rw [eq_sub_iff_add_eq, add_comm, Int.ediv_add_emod']

example (n : ℕ) (r : ℤ) : ∃ k : ℤ, ((r : ZMod n) : ℤ) = r + k*n := by
  use -(r / n)
  rw [ZMod.coe_int_cast, Int.mod_eq, sub_eq_add_neg, neg_mul]

[Yaël Dillies]

This statement looks evil given that you're using the very non-canonical coercion ZMod n → ℤ.

[Kevin Buzzard]

Is ((r : ZMod n) : \Z) equal to r % n (at least in the application)? If so then this could be broken into two smaller steps.

[Patrick Massot]

Thanks Timo!

[Patrick Massot]

Is there a non-evil spelling of this ZMod n → ℤ map?

[Eric Rodriguez]

zmod.val?

[Eric Wieser]

I think the claim is that the map itself is evil

[Jireh Loreaux]

I don't see what is so evil about this map. Although I guess another version which is similar in spirit but avoids this coercion is (r : ZMod n) = (r % n : ZMod n).

[Kevin Buzzard]

The map is evil because it doesn't preserve addition, multiplication, or 1. I would maintain that the map from Fin n to the naturals was not evil but that if you're using ZMod n then you're announcing that you care about the ring structure and so you shouldn't be using maps that don't.

[Jireh Loreaux]

Well, sure, but just because a function is a morphism in that category doesn't mean it's evil. ℝ is a ring too, and sin : ℝ → ℝ doesn't preserve addition, multiplication or 1 either. The fact that a particular function isn't a morphism only means that the API surrounding it's use doesn't come for free and we need to write it separately.

[Kyle Miller]

The function ZMod n → ℤ seems fine (it's giving a minimal non-negative representative), but it doesn't seem right to have it be a coercion.

[Kevin Buzzard]

Right, like sin isn't a coercion

[Jireh Loreaux]

Aha, evil because it's a coercion, which is what Yaël said, but different from Eric's claim that the map itself is evil. I can get on board with the coercion being evil, not least because it means there are coercions in both directions. I think that's arguably the most evil part of it.

[Jireh Loreaux]

Returning to this to mention: it's a shame we lost @Anne Baanen's work in Lean 3 allowing for coercions to possess morphism properties. It would be nice if there were a way to recover this in some form.

[Jireh Loreaux]

I understand that it's very different because we don't have an actual coe function anymore. I'm just dreaming / hoping that someone smarter than me comes up with a new idea.

[Eric Wieser]

it would be pretty easy for us to reintroduce a new coe function

[Eric Wieser]

Though it would probably not be liked by Leo

[Eric Wieser]

(we effectively already did this for coeFn and coeSort)

[Jireh Loreaux]

I'm not arguing for that in general. I think it was necessary for Fun like, but the auto-unfold in Lean 4 is very nice.

[Eric Wieser]

I think probably what we should actually visit is arbitrary functions possessing morphism properties