Localized instances

Stream: general

[Yaël Dillies]

How hard would it be to have an attribute localized_instance which

• protects the declaration
• nolints it for docstrings
• declares it as an instance in the specified local

[Yaël Dillies]

Working on file#data/set/pointwise, file#data/finset/pointwise, file#order/filter/pointwise is a pain because one must write useless docstrings to the new instances, protect them and add them manually to the nearest pile of localized ... in pointwise. I wish I could just do

@[localized_instance pointwise, to_additive]
instance mul_one_class [mul_one_class α] : mul_one_class (set α) :=

instead of

/-- `set α` is a `mul_one_class` under pointwise operations if `α` is. -/
@[to_additive "`set α` is an `add_zero_class` under pointwise operations if `α` is."]
protected def mul_one_class [mul_one_class α] : mul_one_class (set α) := sorry

localized "attribute [instance] set.mul_one_class set.add_zero_class" in pointwise

It would maybe even be better if we could extend the instance attribute instead of creating a new one.

[Yaël Dillies]

And one neat bonus would to make check_reducibility not throw errors when such localized instances are used in global ones. For example, the pointwise filter instances currently do not use the set ones, but I want to tweak them to improve the definitional unfolding and I find myself needing to localize them all as well to appease the linter.

[Kyle Miller]

Is this different from your previous proposal? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Automatic.20attribute.20localization/near/275732727

[Yaël Dillies]

Thanks I couldn't find it anymore :sweat_smile: It's the same underlying idea but I refined it to make sure it really behaves like instance.

[Kyle Miller]

I think this is still subsumed by Lean 4's scoped instances feature

[Yaël Dillies]

So is the answer "Wait for Lean 4"?

[Yaël Dillies]

Also, I don't think scoped _root_.pointwise.set.mul_one_class is much more user-friendly than what we already have. I once again despair at the new scoping mechanism.

[Yaël Dillies]

Putting stuff in namespaces set.pointwise, finset.pointwise, filter.pointwise is not an option because you don't want to open three different pointwise namespaces every time you work on something.

[Kyle Miller]

Potentially you can export set.pointwise to pointwise, but I haven't checked.

[Yaël Dillies]

Well anyway if I can't change your mind so as to why scoped is bad, we might as well backport it so that I can change mine.