porting `localized`

Stream: mathlib4

[Mario Carneiro]

Currently, Mathlib.Mathport.Syntax has an implementation of the localized command, and mathport does in fact produce localized applications when translating localized commands: example. However, Mathlib.Mathport.Syntax is not intended to be imported by mathlib4, and in most cases we want to rewrite it to use something else. So what should we do about this command? Options:

1. Move localized into its own file and start importing it in mathlib4. This amounts to making it an official bit of syntax.
2. Change mathport to produce the code that localized expands to, i.e. using with_weak_namespace around a scoped syntax. This is what we should do if we are deprecating it.
3. Change mathport to just use scoped syntax without the namespace. This is closest to the code we would like people to write instead, but it is sometimes wrong if we are not in the right namespace.
4. Refactor mathlib3 to use the current namespace as the "locale" instead of taking it as an argument. This will make option (3) a more correct course of action.

[Gabriel Ebner]

I think (2) is worse than what we have right now. with_weak_namespace is a mathlib extension as well btw.

[Mario Carneiro]

using mathlib extensions is fine, mathport is full of mathlib extensions like all the tactics we're porting

[Mario Carneiro]

but I grant that with_weak_namespace isn't a nice thing to ask people to write directly post-port

[Gabriel Ebner]

It's also a big step backwards, we now have macros so that we don't have to write useless boilerplate. Let's use them.

[Mario Carneiro]

okay, but is localized the right abstraction here?

[Mario Carneiro]

since then we have to teach people when to use localized vs local vs scoped

[Gabriel Ebner]

Maybe we should rename localized to scoped. Then it would be a natural generalization:

scoped notation "foo" => 42 -- scoped in current namespace
scoped[Foo] notation "foo" => 42 -- scoped in Foo namespace

[Mario Carneiro]

that makes sense to me. Is that Foo or current namespace + Foo?

[Gabriel Ebner]

It's _root_.Foo, which is more useful than current namespace + Foo. But I could also live with prepending the current namespace.

[Mario Carneiro]

is it possible to "resolve" a namespace? Like if you have open Lean Meta then Meta refers to namespace Lean.Meta even though you might be in namespace Std.DList or something

[Gabriel Ebner]

I only put the localized command in the Mathport/Syntax.lean file because I didn't want to make a new 5-line file.. If I had known that the location of the command would have such huge consequences, I would have put it in its own file.

[Mario Carneiro]

well I was going to move the file myself but I took the positioning (and in particular the trivial implementation) as an indicator that we hadn't yet fully settled on a course of action here

[Mario Carneiro]

are there circumstances where mathport should not produce a use of localized?

[Gabriel Ebner]

I think if scoped notation "foo" has the same effect as scoped[NS] notation "foo" then we should probably drop the unnecessary namespace attribute.

[Mario Carneiro]

should this scoped[NS] thing be part of attrKind in core, or a separate mathlib extension?

[Mario Carneiro]

the mathlib localized has a rather different syntax from attrKind, since it wraps a command rather than going inside attribute lists and such

[Gabriel Ebner]

It would be nicer in core. But it's certainly easier to put it in mathlib for now.

[Gabriel Ebner]

I have no idea if we can monkeypatch attribute [scoped[Foo] simp] bar.

[Mario Carneiro]

I doubt we can, without replacing half of lean 4 syntax, since attrKind is not extensible

[Gabriel Ebner]

Unfortunately syntax "scoped" "[" ident "]" attr : attr doesn't work either. :sad:

[Mario Carneiro]

Mario Carneiro said:

is it possible to "resolve" a namespace? Like if you have open Lean Meta then Meta refers to namespace Lean.Meta even though you might be in namespace Std.DList or something

Oh, it's already being resolved by the current version of with_weak_namespace Foo / localized [Foo]

[Mario Carneiro]

so you do have to use _root_.Foo if you want the root version

[Mario Carneiro]

and actually there are some mathlib examples where the locale name should really be prefixed, like this

[Gabriel Ebner]

Uhm, localized [Foo] expands to with_weak_namespace _root_.Foo so you don't need to write _root_ yourself.

[Mario Carneiro]

oh, missed that part

[Kyle Miller]

I think it would be nice if we port localized so that there is a special namespace for scoped notation. For example, put notation localized to Foo into Locale.Foo (or Foo.Locale). Then open_locale Foo becomes open Locale.Foo (or open Foo.Locale). This helps separate notation from other declarations in a given namespace.

[Kyle Miller]

There might be a better name for this than Locale. Mathlib3 uses locales for both local notation and local instances, and it might make sense to separate these into scoped notations and scoped instances with more specific names. Potential examples:

• open_locale big_operators --> open Notation.BigOperators
• open_locale pointwise --> open Instances.Pointwise

[Mario Carneiro]

Note that you can open scoped Foo to just get the notations of Foo without the declarations

[Mario Carneiro]

and while I don't think it currently exists, we could also have open Foo hiding scoped to do the opposite

[Kyle Miller]

Even with the open scoped feature, it would be good to think about logical namespaces to put notation extensions, since we have generally been careful in mathlib3 to make these be opt-in.

[Mario Carneiro]

I am reminded of the old eq.ops namespace from lean 2 which held some funny symbols for eq.symm, eq.trans and congr_arg

[Mario Carneiro]

@Floris van Doorn can probably say more about how scoped notations were organized in lean 2

[Floris van Doorn]

I am in favor of mixing declarations and scoped notation in the same namespace. So open TopologicalSpace gives you both the declarations in that namespace, and all the scoped notation in that namespace. Of course, we might have a few "notation namespaces" that happen to have only scoped notation and no declarations in them (like BigOperators and Pointwise), but other than that I think we can mix them.

In Lean 2 it also worked like that. We indeed had the weird eq.ops namespace with some (scoped) notation, but (at least in the HoTT library) we generally mixed notation and declarations.

[Yaël Dillies]

Another one would be FinsetFamily.

[Mario Carneiro]

I implemented most of the stuff mentioned in this thread in mathport. With that I have a refactor request: mathport now handles the case where a localized command uses the same name as the namespace you happen to be in specially, so it would be good to make sure mathlib is using this style wherever possible.

localized "notation `foo` := bar" in boo   -- bad
namespace boo
...

namespace boo
localized "notation `foo` := bar" in boo   -- good
...

[Yaël Dillies]

Wait, what do you mean? that now everything must be localized in the namespace we're in?

[Floris van Doorn]

I expect that both work, but the ported command is simpler if you're already in the namespace.

[Yaël Dillies]

Does that mean

localized ... in pointwise

should become

namespace pointwise
localized ... in pointwise
end pointwise

[Gabriel Ebner]

must be localized in the namespace we're in?

No, it's completely optional and both variants will translate just fine. Don't add extra namespaces!

[Gabriel Ebner]

It's just that if you already have a namespace block, consider moving the localized commands there.

[Gabriel Ebner]

Think of it like def boo.foo := 42 vs namespace boo def foo := 42 end.