Casting from N to ZMod q

Stream: new members

[Christoph Spiegel]

Hi everyone,

I am running into some weird casting behavior when handling numbers in ZMod q. This is the MWE that showcases the issue:

import Mathlib.Data.ZMod.Basic

example (p q : ℕ) [Fact (Nat.Prime p)] (h : 2 ^ p ≡ 1 [MOD q]) : 0 = 0 := by
  have two_pow_p_eq_one := (@Nat.cast_pow (ZMod q) _ 2 p) ▸ ((ZMod.eq_iff_modEq_nat q).mpr h)
  have two_pow_p_eq_one' := Eq.mp (congrArg (Eq (2 ^ p)) Nat.cast_one) two_pow_p_eq_one

  have := orderOf_eq_prime two_pow_p_eq_one' (sorry) -- this one works
  have := orderOf_eq_prime two_pow_p_eq_one (sorry) -- this one doesn't

I am also not quite sure when the casting arrow ↑ appears and when it does not, because there are elements 1 and 2 in ZMod q in the infoview that should be casted from Nat but appear without the arrow.

[Ruben Van de Velde]

A #mwe should have the necessary import statements

[Christoph Spiegel]

Ruben Van de Velde said:

A #mwe should have the necessary import statements

Sorry, import Mathlib.Data.ZMod.Basic seems to be the only thing necessary .

[Jireh Loreaux]

Note that 12345 : ZMod q makes sense for any q (without a cast from ℕ) due to the docs#OfNat instance. So that's probably why there's no ↑.

If you actually want it to be casted from ℕ, you can write something like ((2 : ℕ) : ZMod q).

[Jireh Loreaux]

That being said, I think you probably don't want the Nat.cast to appear in the statements here.

[Christoph Spiegel]

So checking out the two versions of two_pow_p_eq_one in the infoview I get

two_pow_p_eq_one: ↑2 ^ p = ↑1
two_pow_p_eq_one': 2 ^ p = 1

The entities with casting arrows are @Nat.cast (ZMod q) and the other ones are @OfNat.ofNat (ZMod q) 2 .

What exactly do you mean by not wanting to use Nat.cast? The following would suggest that these three casting approaches should be interchangeable (and I would expect that preferably only the first is needed):

def a := (2 : ZMod 5)  -- ZMod 5 := 2
def b := @Nat.cast (ZMod 5) _ 2  -- ZMod 5 := ↑2
def c := @OfNat.ofNat (ZMod 5) 2 _  -- ZMod 5 := OfNat.ofNat 2

example : a = b := rfl
example : b = c := rfl
example : a = c := rfl

But orderOf_eq_prime is not able to accept the output of eq_iff_modEq_nat without first using the congrArg trick (which I don't even exactly recall how I came up with).

[Jireh Loreaux]

Yes, they're provably equal (even definitionally equal), but in statements you'll want to prefer (2 : ZMod 5) in general, even if in the proof you need to convert it to a Nat.cast.

[Jireh Loreaux]

Also, note that a and c are really the same thing:

example : (2 : ZMod 5) = @OfNat.ofNat (ZMod 5) 2 _ := by with_reducible rfl

The same doesn't work for b.

[Jireh Loreaux]

The theorem docs#Nat.cast_eq_ofNat should help you convert between the two with rw.

[Christoph Spiegel]

Nat.cast_eq_ofNat does take care of the conversion, but if I #print the proof terms, it's just the same congrArgproof in the background using Nat.cast_one (probably how I found that explicit coercion in the first place).

I guess the following two things don't make sense to me:

1. Why does eq_iff_modEq_nat return the 'undesirable' @Nat.cast, in particular since the Prop statement is (a : ZMod n) = b ↔ a ≡ b [MOD n], indicating that it should return @OfNat.ofNat?
2. If they are definitionally equal, why isn't orderOf_eq_prime able to coerce the input into the right form, in particular since even the following more modest variant of two_pow_p_eq_one that only replaces ↑1 with 1 works: have := orderOf_eq_prime (@Nat.cast_one (ZMod q) _ ▸ two_pow_p_eq_one) (sorry).

[Eric Rodriguez]

There's two different things going on here, and I agree that it's somewhat confusing.

Nat.cast is just the general function that takes any element of Nat to some semiring (or weaker). This works for any natural number, no matter how you write it.

OfNat is for the specific case when you write an _explicit_ natural number, such as 23 or 37 or 12386902 or 1. This mechanism allows classes to define specifically what stuff that is parsed as a natural number can be parsed "natively" by the class. You can imagine, for example, a class like TheNumbersFromThreeToFive could only want to implement OfNat for 3, 4, 5, and not have a general Nat.cast instance.

However, where it gets tricky is that for (iirc) everything (if not, then most things) that have a Nat.cast defined, we also define OfNat R t to just be equal to Nat.cast t. Therefore, these two are equal definitionally; we like this in general! There could be some argument that this is not always the best option (for example, you can write 7 : Fin 5); however, what this means is that with numerals you can get these two things, that are @OfNat (ZMod q) k, and @Nat.cast (ZMod q) (@OfNat Nat k).

[Christoph Spiegel]

That makes some sense, thanks for the explanation!

I re-read the error message from orderOf_eq_prime and realized that it never complained about the2, the issue is that it wants the identity element 1 in the Monoid, not the casted ↑1. So I would say that replacing the ↑1 through Nat.cast_one is the 'correct' way of handling this, rather than just blanket rewriting everything withNat.cast_eq_ofNat.

What I still don't quite understand is why Lean seemingly can coerce 2 ^ p = 1 into ↑2 ^ p = 1 (that's what happens when too aggressively rewriting not just the 1 but also the 2with Nat.cast_eq_ofNat or just through simp), but it cannot coerce ↑2 ^ p =↑ 1 into ↑2 ^ p = 1?

[Jireh Loreaux]

Nat.cast_eq_ofNat requires a docs#Nat.AtLeastTwo instance. I think that's the reason for the behavior you're seeing, but maybe I'm misunderstanding.

[Eric Wieser]

Jireh Loreaux said:

Also, note that a and c are really the same thing:

But they are not really really the same; c contains a second application of ofNat because it did not use nat_lit 2

[Jireh Loreaux]

Indeed, I had considered saying that, but thought better of it to avoid confusion.