How do you hide scoped notation

Stream: lean4

[Terence Tao]

In a forthcoming analytic number theory formalization project, we would like to use Nat.ArithmeticFunction as well as complex analysis. In analytic number theory it is traditional to write the complex variable as s = σ + I*t, which causes a conflict because Nat.ArithmeticFunction includes scoped notation (docs#Nat.ArithmeticFunction.termσ) that defines σ as Nat.ArithmeticFunction.sigma, thus for instance the following code fails unless ArithmeticFunction is not opened:

import Mathlib

open Complex Nat ArithmeticFunction

proof_wanted riemann_hypothesis (σ t:ℝ) (h: σ > 1/2) : riemannZeta (σ + I*t) ≠ 0

Is there a way to hide the scoped notation σ from the opening of ArithmeticFunction? I tried open ArithmeticFunction hiding termσ and open ArithmeticFunction hiding sigma but these did not work. One could of course rename the variable σ to something else like σ' but we don't plan on using Nat.ArithmeticFunction.sigma and it would be more elegant to somehow suppress the notation while retaining access to the arithmetic functions (such as Λ, the von Mangoldt function) that we do wish to use.

[Eric Rodriguez]

This is a ridiculously hacky workaround that is honestly a bug, but if you do open ArithmeticFunction renaming ... -> ... it should work. This is because the renaming elaborator forgets to run docs#activateScoped

[Eric Rodriguez]

(do that in the next line, and with the ... being some name in the ArithmeticFunction namespace - you can rename something to itself)

[Eric Rodriguez]

(https://github.com/leanprover/lean4/blob/b614ff1d12bc38f39077f9ce9f2d48b42c003ad0/src/Lean/Elab/Open.lean#L60-L97 if anyone wants to file a core bug)

[Terence Tao]

Could you provide a mwe of your hack? The ... does not compile, and replacing it with say σ doesn't seem to work either.

[Eric Rodriguez]

import Mathlib

open Complex Nat
open ArithmeticFunction renaming sigma → sigma

proof_wanted riemann_hypothesis (σ t:ℝ) (h: σ > 1/2) : riemannZeta (σ + I*t) ≠ 0

[Terence Tao]

Hmm. Unfortunately that also disables the notation that we did want to use from Nat.ArithmeticFunction, such as Λ, so now other parts of the code stop working (in this case, the second proof_wanted):

import Mathlib

open Complex Nat
open ArithmeticFunction renaming sigma -> sigma


proof_wanted riemann_hypothesis (σ t:ℝ) (h: σ > 1/2) : riemannZeta (σ + I*t) ≠ 0

@[coe] def ofReal (f : ArithmeticFunction ℝ) : ArithmeticFunction ℂ where
  toFun n := f n
  map_zero' := by simp only [Nat.ArithmeticFunction.map_zero, ofReal_zero]

instance realCoe : Coe (ArithmeticFunction ℝ) (ArithmeticFunction ℂ) := ⟨ofReal⟩

proof_wanted von_mangoldt_and_zeta (σ' t:ℝ) (h: σ' > 1) : LSeries Λ (σ' + I*t) = - deriv riemannZeta (σ' + I*t) / riemannZeta (σ' + I*t)

[Eric Rodriguez]

from reading the code, I don't think there's currently any way to do this, sadly. I think there's a good case for it, however

[Terence Tao]

Huh. Hopefully there will be a better fix in the future. I guess for now we just use σ' instead of σ.

[Michael Stoll]

Your second proof_wanted is available in my EulerProducts repository, BTW. (In terms of a complex variable s with real part > 1.)

[Terence Tao]

Guess my project is 50% complete then :joy:

[Kyle Miller]

I don't think there's a way to turn off notation after it's been added.

I think we should be more careful about which namespace notation goes in. In this case, perhaps it would be better in Nat.ArithmeticFunction.Notation

[Michael Stoll]

Off-topic: I think the "Nat." part in Nat.ArithmeticFunction is a bit redundant. Maybe we can just use ArithmeticFunction for the namespace?

[Eric Rodriguez]

Kyle Miller said:

I don't think there's a way to turn off notation after it's been added.

I think we should be more careful about which namespace notation goes in. In this case, perhaps it would be better in Nat.ArithmeticFunction.Notation

In the code above, Terry seems to want some of the notation in that namespace and not some of the others. Wasn't there going to be a change to force notations to be named?

[Michael Stoll]

So can one import only selected notations?

[Michael Stoll]

(instead of hiding some)

[Kyle Miller]

@Eric Rodriguez Oh, I see. Even if notations are named, right now it seems you can't turn any off (term_parser is one of those un-erasable attributes)

[Kyle Miller]

It seems to be possible to import individual notations, if you know the name of their parser:

import Mathlib

open Complex Nat

attribute [term_parser] ArithmeticFunction.termΛ

#check Λ

That doesn't enable the pretty printer however.

[Kyle Miller]

I suppose another solution then is to have a separate namespace per notation, so that way you can open scoped whatever you want to enable.

[Eric Rodriguez]

I think separately from this specific use-case it'd be nice to have some version of open that didn't open scoped, (well, without the current hacky workaround)

[Terence Tao]

Kyle Miller said:

I suppose another solution then is to have a separate namespace per notation, so that way you can open scoped whatever you want to enable.

Actually I imagine that would come with its own problems, for instance in this particular case the σ notation is used in the statement of several further lemmas in ArithmeticFunction and so it doesn't seem obvious to me how to select lemmas and notation "a la carte" without having to unfold any notation in a lemma that one opened without opening the supporting notation. For this particular use case we plan to use quite a few tools and notations from ArithmeticFunction, so selectively introducing a handful of targeted notations and lemmas isn't ideal here, but it's good to know that some option to partially introduce notation from a namespace exists.

[Kyle Miller]

It might be possible (using either current or potential future features) to have a la carte scoped notations that can be bundled up into a particular other namespace.

For example, we currently have export as an alternative to open to cause certain names to be available to those who open the namespace they were exported to. I don't know how scoped interacts with export at the moment.

I don't know if this would help you, but I'm interested in figuring out what would be helpful and am exploring the nearby design space.

[Terence Tao]

Kyle Miller said:

It might be possible (using either current or potential future features) to have a la carte scoped notations that can be bundled up into a particular other namespace.

For example, we currently have export as an alternative to open to cause certain names to be available to those who open the namespace they were exported to. I don't know how scoped interacts with export at the moment.

I don't know if this would help you, but I'm interested in figuring out what would be helpful and am exploring the nearby design space.

I could imagine an a la carte bundling option to be useful for educational purposes. For instance to create "natural number game" like environments where a select number of tools from a namespace (together with whatever notation was needed in order to state those tools) were made readily available without access to the entire namespace.

[Yaël Dillies]

open scoped SomeNamespace (nameOfSomeNotation nameOfSomeOtherNotation) is the syntax I would be expecting

[Michael Stoll]

For the time being, #10403 adds separate scopes for the notations for arithmetic functions (like ArithmeticFunction.sigma or ArithmeticFunction.vonMangoldt), so that it will be possible to make a selection of the notations one would like to import. (open scoped ArithmeticFunction will still give access to all of them.)

[Michael Stoll]

#10403 has just been merged.

[Yury G. Kudryashov]

Should we also move notation for docs#Nat.primeCounting to another scope? Currently open scoped Nat Real creates a conflict for π (I wanted to have notation for Real.pi and Nat.factorial in one file).