local semireducible

Stream: mathlib4

[Jireh Loreaux]

how do I adjust the transparency of a definition locally? In mathlib4#922 mathport outputs:

attribute [local semireducible] WithOne WithZero

But Lean complains invalid attribute 'semireducible', must be global. However, if I also remove the local (and wrap this in a section) then it complains invalid attribute 'semireducible', declaration is in an imported module

How do I deal with this?

[Jireh Loreaux]

@Mario Carneiro: I know during the meeting we discussed just making WithOne semireducible. However, when I went to do so, I realized that it was already semireducible because it had never been marked irreducible in mathlib4#841. It turns out that the reason for this is that mathport just entirely ignored the attribute [irreducible] with_one line from mathlib3. This seems like a bug in mathport, right? Or am I missing something?

[Mario Carneiro]

Like I said in the meeting, attribute [irreducible] is just plain not supported in lean 4

[Mario Carneiro]

I suppose it could print the line commented out and make a porting note of its own

[Jireh Loreaux]

Ummm... I'm confused. I thought what wasn't supported was locally changing the transparency of a definition. But I thought that the transparency could still be adjusted (globally and permanently) within the module in which it was declared. Indeed, adding attribute [irreducible] WithOne into Algebra.Group.WithOne.Defs does not yield an error and it seems to have the effect that makes it irreducible.

[Jireh Loreaux]

@Mario Carneiro pinging just to make sure you see this again, because I definitely don't understand.

[Mario Carneiro]

I could be wrong, but my understanding was that this causes problem for caching various things. Maybe it was fixed by just clearing all the caches, in which case it is possible to do but expensive

[Jireh Loreaux]

Okay, I see. Thanks.

[Kevin Buzzard]

Surely the autoporter should be flagging that it's ignoring various mathlib3 declarations?

[Scott Morrison]

I made a mathlib3 PR #17874 removing a small number of local attribute [semireducible]s.

[Scott Morrison]

I think it would be a good idea if we start getting rid of all of these.

[Scott Morrison]

grep -r 'local attribute \[semireducible\]' * | grep -v ^meta | grep -v ^tactic

says:

algebra/order/monoid/to_mul_bot.lean:local attribute [semireducible] with_zero
algebra/order/monoid/with_zero/defs.lean:local attribute [semireducible] with_zero
algebra/group/with_one/basic.lean:local attribute [semireducible] with_one with_zero
algebraic_geometry/Gamma_Spec_adjunction.lean:local attribute [semireducible] Spec.to_LocallyRingedSpace
algebraic_geometry/Gamma_Spec_adjunction.lean:local attribute [semireducible] LocallyRingedSpace_adjunction Γ_Spec.adjunction
algebraic_topology/simplex_category.lean:local attribute [semireducible] simplex_category
algebraic_topology/simplex_category.lean:local attribute [semireducible] simplex_category.hom
category_theory/triangulated/rotate.lean:local attribute [semireducible] shift_shift_neg shift_neg_shift
data/fin/basic.lean:local attribute [semireducible] reflected
data/zmod/basic.lean:local attribute [semireducible] int.nonneg
data/zmod/quotient.lean:local attribute [semireducible] mul_opposite
data/rat/meta_defs.lean:local attribute [semireducible] reflected
data/int/basic.lean:local attribute [semireducible] reflected
group_theory/monoid_localization.lean:local attribute [semireducible] localization.mul localization.one localization.npow
group_theory/monoid_localization.lean:local attribute [semireducible] localization
group_theory/monoid_localization.lean:local attribute [semireducible] localization.zero localization.mul
ring_theory/fractional_ideal.lean:local attribute [semireducible] mul
ring_theory/fractional_ideal.lean:local attribute [semireducible] span_singleton
ring_theory/class_group.lean:local attribute [semireducible] to_principal_ideal
ring_theory/dedekind_domain/selmer_group.lean:local attribute [semireducible] mul_opposite
ring_theory/localization/fraction_ring.lean:local attribute [semireducible] is_fraction_ring.inv
topology/algebra/group/basic.lean:local attribute [semireducible] mul_opposite