diamond for monoid instance on ideals

Stream: general

[Kevin Buzzard]

@María Inés de Frutos Fernández seems to have found a diamond in recent mathlib; she bumped her adeles project and some of her code stopped working; mathlib is finding two instances of a monoid structure on ideals of the integers of a number field.

import number_theory.number_field
import ring_theory.dedekind_domain

variables (K : Type) [field K] [number_field K]

open number_field

-- X and Y both have type `monoid (ideal ↥(ring_of_integers K))`

def X := @monoid_with_zero.to_monoid
    (@ideal ↥(@ring_of_integers K _inst_1)
       (@ring.to_semiring ↥(@ring_of_integers K _inst_1)
          (@comm_ring.to_ring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_ring)))
    (@semiring.to_monoid_with_zero
       (@ideal ↥(@ring_of_integers K _inst_1)
          (@ring.to_semiring ↥(@ring_of_integers K _inst_1)
             (@comm_ring.to_ring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_ring)))
       (@submodule.semiring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_semiring
          ↥(@ring_of_integers K _inst_1)
          (@ring_of_integers K _inst_1).to_semiring
          (@number_field.ring_of_integers_algebra K K _inst_1 _inst_1
             (@algebra.id K
                (@comm_ring.to_comm_semiring K
                   (@euclidean_domain.to_comm_ring K (@field.to_euclidean_domain K _inst_1)))))))

-- depends on `ideal.cancel_comm_monoid_with_zero` so noncomputable
noncomputable def Y := @monoid_with_zero.to_monoid
    (@ideal ↥(@ring_of_integers K _inst_1)
       (@ring.to_semiring ↥(@ring_of_integers K _inst_1)
          (@comm_ring.to_ring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_ring)))
    (@comm_monoid_with_zero.to_monoid_with_zero
       (@ideal ↥(@ring_of_integers K _inst_1)
          (@ring.to_semiring ↥(@ring_of_integers K _inst_1)
             (@comm_ring.to_ring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_ring)))
       (@cancel_comm_monoid_with_zero.to_comm_monoid_with_zero
          (@ideal ↥(@ring_of_integers K _inst_1)
             (@ring.to_semiring ↥(@ring_of_integers K _inst_1)
                (@comm_ring.to_ring ↥(@ring_of_integers K _inst_1) (@ring_of_integers K _inst_1).to_comm_ring)))
          (@ideal.cancel_comm_monoid_with_zero ↥(@ring_of_integers K _inst_1)
             (@ring_of_integers K _inst_1).to_comm_ring
             _
             _)))

example : X = Y := rfl -- fails

One is computable, the other isn't. She's worked around the issue with some cunning priority-setting but because the code used to work this is probably a consequence of a relatively recent commit.
The fix was

local attribute [instance, priority 10000] comm_monoid_with_zero.to_monoid_with_zero

[Eric Rodriguez]

I wonder if this is due to my ring of integers algebra instance? (docs#number_field.ring_of_integers_algebra). what happens if she turns it off?

[Eric Rodriguez]

(also, it seems the pretty-printing bug from the widget has spread to the docs website :()

[María Inés de Frutos Fernández]

Thanks, @Eric Rodriguez . Yes, it seems it was caused by the ring_of_integers_algebra instance; I commented it out and the error went away (Is this what you meant by "turning it off"?).

[Alex J. Best]

You can also do local attribute [-instance] ring_of_integers_algebra within a file or section to turn an instance of locally but still have it availiable elsewhere

[Eric Rodriguez]

you should able to just do attribute [-instance] ring_of_integers_algebra. I added it for a reason I later realised was mathematically wrong, so if it's causing diamonds I think we should definitely consider either fully removing it or just making a def.

[Eric Wieser]

How exactly is the diamond related to that algebra instance?

[Eric Rodriguez]

algebra K K inducing algebra O K O K, it seems

[María Inés de Frutos Fernández]

Eric Rodriguez said:

you should able to just do attribute [-instance] ring_of_integers_algebra.

Thanks! I didn't know about this.

[Eric Wieser]

I think this diamond with docs#subalgebra.algebra' is fundamentally the same problem:

import algebra.algebra.subalgebra

example {R A} [comm_semiring R] [comm_semiring A] [algebra R A] (S : subalgebra A A) :
  (algebra.id S) = subalgebra.algebra' _ :=
begin
  change algebra.mk _ _ _ = algebra.mk _ _ _,
  congr' 1,
  ext : 1,
  change x = subtype.mk x _,
  refl, -- fails
end

which is the fact that docs#subtype.coe_eta is not true definitionally (until Lean 4).

[Eric Rodriguez]

can we hack definitional eta into Lean3 whilst we wait for mathport? or is this just ridiculous?

[Eric Wieser]

This seems to be caused by a diamond in subtypes withalgebra.id (moved out of this thread)