zmod comm_ring field diamond

Stream: general

[Alex J. Best]

Does anyone know what the issue with the following is, or better yet how to fix it :):

import data.zmod.basic

variables {p : ℕ} [fact p.prime]
example :
  @euclidean_domain.to_comm_ring _ (@field.to_euclidean_domain _ (zmod.field p)) = zmod.comm_ring p :=
rfl

I'm completely stumped

[Junyan Xu]

Probably because docs#zmod.comm_ring is defined by cases (whether n = 0) and therefore not defeq to its eta-expanded form (i.e. with all fields in the structure expanded).

[Yaël Dillies]

Ah so it's a matter of f (nat.rec hzero hsucc) = nat.rec (f hzero) (λ n, f (hsucc n)) not being defeq?

[Alex J. Best]

Yeah that makes sense, I wonder if its even possible to get around this then, if field etc. were new structures that would help I guess?

[Junyan Xu]

If you replace p by p+1 it works

[Alex J. Best]

Or maybe we could redefine the comm_ring structure so each field was individually defined via cases, but that sounds horrible

[Eric Wieser]

Yes, that's how to fix the problem

[Junyan Xu]

In Lean 4 this doesn't need to be fixed, right? Because eta-expansion is defeq (lean4#777).

[Junyan Xu]

BTW to prove it in the original form:

import data.zmod.basic

variables {p : ℕ} [fact p.prime]
example :
  @euclidean_domain.to_comm_ring _ (@field.to_euclidean_domain _ (zmod.field p)) = zmod.comm_ring p :=
by { have := (fact.out p.prime).pos, unfreezingI {cases p}, {cases this}, {refl} }

[Eric Wieser]

This isn't just structure eta, this is more general inductive eta

[Junyan Xu]

But as soon you expand the RHS to {add := (zmod.comm_ring p).add, ...} I think it's then defeq to the LHS.

[Junyan Xu]

docs#zmod.field is defined with .. zmod.comm_ring p.

[Reid Barton]

Is there a reason zmod n isn't defined as, you know, Z mod (n)

[Riccardo Brasca]

Well, taking the quotient zmod 0 wouldn't be equal to Z.

[Yaël Dillies]

Sure, but is ℤ/0ℤ really equal to ℤ anyway?

[Kevin Buzzard]

Neither the current definition nor Reid's proposed refactor make zmod 0 definitionally equal to ℤ.

[Bryan Gin-ge Chen]

Certainly the docstring should include more information about the actual definition. Right now docs#zmod simply says:

The integers modulo n : ℕ.

[Junyan Xu]

Kevin Buzzard said:

Neither the current definition nor Reid's proposed refactor make zmod 0 definitionally equal to ℤ.

Sorry? docs#zmod says zmod 0 = ℤ

[Riccardo Brasca]

Currently it's propositionally equal at least

[Kevin Buzzard]

Oh no you're absolutely right, I had misremembered, I thought it was defined with if then else. It is indeed definitionally equal right now.

[Alex J. Best]

This is now #14712