Strange coercions with ZMod

Stream: general

[David Loeffler]

This threw me completely:

#eval (8 : ℤ) = (0 : ZMod 4) -- result: "false"
#eval (0 : ZMod 4) = (8 : ℤ) -- result: "true"

The problem seems to be that the map ZMod.cast sending ZMod N to ℤ, which sends a residue class to its least non-negative representative, is registered as a coercion; but the map Int.cast mapping ℤ to an arbitrary ring is also a coercion, and it seems Lean's rules for which coercion it picks depend on which way round the equality is written.

Personally I find it deeply disturbing that ZMod.cast : ZMod 4 → ℤ is a coercion; in first-year algebra lectures we spend a great deal of effort trying to train students not to think of ℤ / N as "{0, ..., N-1} with funny arithmetic operations". It looks like mathlib does exactly that internally (ZMod N is an alias for Fin N); but shouldn't that be a guilty secret of the implementation, to be concealed as much as possible in the API?

[Mario Carneiro]

seems the least we could do is make it a scoped instance

[Kevin Buzzard]

This is another issue of ZMod and Fin being semantically different. ZMod.cast is a horrible function, it doesn't have good mathematical properties, it's a great idea to scope it. I am now worried that someone who knows what a bitvec is will start arguing that it should definitely be there because computer scientists love it for some reason.

[Mario Carneiro]

We've had discussions about it before. I think one argument for it was that although it isn't generally sensible, there are cases where it makes sense, like the map from Z/6 to Z/3 composing this function with the quotient map

[Mario Carneiro]

so you can rationalize it on the grounds of "garbage in garbage out"

[Mario Carneiro]

But I think it's a sufficiently niche usage that scoping it should suffice

[Kyle Miller]

David Loeffler said:

Personally I find it deeply disturbing that ZMod.cast : ZMod 4 → ℤ is a coercion

I agree with this (here's a previous thread; I can't find the one where I wrote down the same sort of example as yours).

This coercion also breaks the assumption of the expression tree elaborator, which is responsible for arithmetic and inequalities, that there are no nontrivial loops when you compose coercions.

[Kevin Buzzard]

Oh there are not supposed to be nontrivial loops? Then scoping it is a done deal!

[Kyle Miller]

Yep, definitely not! The elaborator tries to find some type among all the leaf terms in an arithmetic expression that all the leaves can be coerced to, and if there's a nontrivial loop of coercions that includes all the types, then who knows what the resulting type will be.

With David's examples, the first one is an equality of Int and the second is an equality of ZMod, for no good reason other than whatever order the elaboration algorithm happens to visit the leaf terms. (A "leaf" is anything that sits inside a tree of operators and (in)equalities; in a + f b * (c : Int) = d, then the leaves are a, f b, (c : Int), and d.)

[Kyle Miller]

Found my previous example:

Kyle Miller said:

import Mathlib.Tactic

def n : Nat := 100
def m : Fin 100 := 50
#eval m ≤ n -- false
#eval n ≤ m -- false

[Johan Commelin]

I'm creating a PR that removes the coercion.

[Floris van Doorn]

I hope that we can also remove one of the Fin coercions, where we have very similar behavior that is also very confusing. (In this case, I think we should remove the coercion Nat -> Fin n.)

import Mathlib.Data.Fin.Basic
#eval (8 : ℕ) = (0 : Fin 4) -- false
#eval (0 : Fin 4) = (8 : ℕ) -- true
#eval (0 : Fin 4) = (8 : ℤ) -- false
#eval (((5 : Fin 8) : Fin 4) : Fin 8) = 1 -- true

[Johan Commelin]

refactor(ZMod): remove coe out of ZMod #9839

[Eric Wieser]

Would it be reasonable to keep around the coercion in the case where [Fact (m ∣ n)] [CharP R m]? Or is that still harmful?

[Eric Wieser]

Floris van Doorn said:

I hope that we can also remove one of the Fin coercions, where we have very similar behavior that is also very confusing. (In this case, I think we should remove the coercion Nat -> Fin n.)

I don't think we can easily remove that coercion without also removing n : R for any ring

[Eric Wieser]

Though putting the ring instance on Fin in a scope would solve it

[Floris van Doorn]

Oh, that's where the coercion comes from. That's fair. I think scoping the ring instance is reasonable.

[Yaël Dillies]

If we really want to go in that direction, should we replace Fin n by ZMod n wherever it is used as a ring?

[Eric Wieser]

No, because that has the wrong behavior for Fin 0 and bitvectors. I think the Fin ring behavior is correct for the people who want it, but it's totally fine to make them ask for it with open scoped

[Michael Stoll]

Eric Wieser said:

Would it be reasonable to keep around the coercion in the case where [Fact (m ∣ n)] [CharP R m]? Or is that still harmful?

There is a ring homomorphism from ZMod n to ZMod m(and thence to R) when m divides n, so this definitely makes sense from a mathematical point of view, and I would think we really want to have it.

[Floris van Doorn]

Does it have to be a coercion though? I think it's fine to just write ZMod.cast a (or something similar for a bundle homomorphism)?

[Kevin Buzzard]

We have docs#ZMod.castHom

[Johan Commelin]

Yes, I imagine that in most cases we will want the bundled hom instead of the coe.

[Johan Commelin]

Eric Wieser said:

Would it be reasonable to keep around the coercion in the case where [Fact (m ∣ n)] [CharP R m]? Or is that still harmful?

Arguably we could even have an Algebra instance under those assumptions. Of course there will be a diamond for R = Zmod n. But this diamond issue also exists for your proposed coe.