Zulip Chat Archive

Stream: mathlib4

Topic: local semireducible


Jireh Loreaux (Dec 08 2022 at 19:55):

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 (Dec 08 2022 at 21:17):

@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 (Dec 08 2022 at 21:18):

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

Mario Carneiro (Dec 08 2022 at 21:19):

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

Jireh Loreaux (Dec 08 2022 at 21:34):

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 (Dec 08 2022 at 22:11):

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

Mario Carneiro (Dec 08 2022 at 22:18):

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 (Dec 08 2022 at 22:20):

Okay, I see. Thanks.

Kevin Buzzard (Dec 08 2022 at 23:17):

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

Scott Morrison (Dec 09 2022 at 04:01):

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

Scott Morrison (Dec 09 2022 at 04:01):

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

Scott Morrison (Dec 09 2022 at 04:03):

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

Last updated: Dec 20 2023 at 11:08 UTC