Why "scoped notation" for Euler's totient function?

Stream: lean4

[Siddhartha Gadgil]

For some reason in Mathlib the symbol φ for the Euler totient function is notation scoped to Nat. This has the unpleasant effect that using this for a function variable name (as is common) gives an error. Just wanted to know why this choice, rather than say an abbrev.

[Siddhartha Gadgil]

A related question: open scode Nat hiding ... does not seem to be a valid command. Can one choose not to import notation?

[Patrick Massot]

An easy fix would be to have a more specific scope.

[Patrick Massot]

Although I very much agree that having a way to remove notation would be great.

[Kenny Lau]

I think we don't want the ability to remove stuff because it puts a burden on maintenance

[Siddhartha Gadgil]

Why is it different from allowing "open blah hiding ..."

[Chris Henson]

This is also a pain point for CSlib, this exact case and other notations.

[Kenny Lau]

what notations do you have in cslib

[Yury G. Kudryashov]

Another pain point is that we can't conveniently use notation for Real.pi if we also open Nat because of the notation for the prime counting function.

[Kenny Lau]

we should have a version of open that doesn't do open scope

[Chris Henson]

Kenny Lau said:

what notations do you have in cslib

IIRC the conflicts are with ZMOD and Finsupp notation. We have just added testing that makes it required to transitively import Mathlib.Init which discourages future conflicts, but it would still be nice to have control over removing notations in downstream projects.

[Kenny Lau]

import Lean

namespace Lean.Elab.Command

def Scope.justOpen (ns : Name) (oldScope : Scope) : Scope :=
  { oldScope with openDecls := .simple ns [] :: oldScope.openDecls }

elab "open " "noscope " ns:ident : command => do
  modifyScope <| Scope.justOpen ns.getId

end Lean.Elab.Command

namespace Nat

def pi : Nat := 3
scoped notation "π" => pi

end Nat

section Test1

open noscope Nat
#check pi
#check π -- error

end Test1

section Test2

open Nat
#check pi
#check π

end Test2

section Test3

open scoped Nat
#check pi -- error
#check π

end Test3

[Kenny Lau]

I've gone and done it

[Kenny Lau]

(the existing open automatically triggers activateScoped)

[Kenny Lau]

@Kim Morrison do you think this is a good idea?

[Kim Morrison]

Yes, the functionality is desirable, but I'm sceptical about the syntax, it's adding yet more to the learnable surface area...

[Kenny Lau]

@Kim Morrison what syntax would you suggest?

[Chris Henson]

I don't think the particular syntax is an issue (though maybe unscoped is better for consistency?). I believe Kim's is commenting on adding more syntax at all to something fundamental like open. I empathize with that argument, but feel maybe that ship has sailed to an extent.

[Kenny Lau]

@Chris Henson what syntax would you suggest?

[Chris Henson]

Again, I am not objecting to your syntax specifically, past slightly preferring open unscoped .... This would be an additional branch in elabOpenDecl that you linked above, yes?

[Kenny Lau]

if it goes to lean4, yes it would have to modify elabOpenDecl

[Kenny Lau]

or else we can just put my code somewhere in mathlib separately

[Chris Henson]

My only suggestion is that even if it is downstream, I would still try to match the syntax that is used in that elab for the scoped case.

[Kenny Lau]

@Chris Henson sorry, I don't understand what you mean by this.

[Kenny Lau]

surely unscoped already matches scoped

[Chris Henson]

Your syntax above is different in that it takes a single ident, while in the elab there is

`(Parser.Command.openDecl| scoped $nss*)

for the scoped case.

[Kenny Lau]

right, i've fixed that locally

[Kenny Lau]

#31086

[Kenny Lau]

the current code looks like:

import Lean

namespace Lean.Elab.Command

def Scope.addOpenDecl (o : OpenDecl) (oldScope : Scope) : Scope :=
  { oldScope with openDecls := o :: oldScope.openDecls }

elab "open " "unscoped " nss:ident* : command => do
  for ns in nss do
    for ns in (← resolveNamespace ns) do
      modifyScope <| Scope.addOpenDecl <| .simple ns []

end Lean.Elab.Command

[Bhavik Mehta]

Patrick Massot said:

An easy fix would be to have a more specific scope.

Some related functions are in the Nat.ArithmeticFunction scope, which could make sense here too

[Siddhartha Gadgil]

Independent of the solution, for my understanding why is notation preferred here to abbrev. I understand for reals for example because of typeclass inference.

[Kenny Lau]

abbrev is just bad, it's pretending to be notation but it's not good enough, i just don't like abbrev in general (personally)

[Kenny Lau]

when people say abbrev they mean notation

[Siddhartha Gadgil]

What here is "just bad". I mean what actually goes wrong. When I say/use abbrev that is what I mean.

[Kenny Lau]

abbrev is another declaration with more eager definitional equality, at the level of expressions they produce different results, so it's harder to use, whereas with notation they elaborate to the same notation so everything still works fine

[Kenny Lau]

if you define Nat.totient and then define Nat.φ then you now have two separate functions that have the same value

[Siddhartha Gadgil]

I know what the difference is internally. I was asking what difference it makes in practice if we have a reducible definition. For types this blocks typeclass inference. Where does it affect functions? I realise rewrite is blocked if some theorems use one and some the other, but what if consistency is enforced.

[Kenny Lau]

consistency to which function

[Siddhartha Gadgil]

Nat.φ

[Kenny Lau]

it's exactly what we now have with le and ge, ge is now entirely unusable

[Kenny Lau]

Siddhartha Gadgil said:

Nat.φ

yeah that's just not mathlib style, mathlib prefers names

[Kenny Lau]

we should have made / make ge a notation

[Siddhartha Gadgil]

To ask again, there is a clear cost to notation - it breaks parsing. This means that if I want to use factorial say, I simply cannot use φ as a variable name. The symbol φ has been elevated to the status (within the scope, but a broad scope) of a reserved word.

This goes against the spirit as I understand of modern programming languages, where reserved words are introduced with great hesitation. It especially goes against the spirit of Lean which wants to be extensible. It is also very nasty from my point of view, since computer generated code will need to know that if I have the factorial symbol (which I would generally want) I lose the use of a variable that is extremely commonly used as a function name.

Of course one has to balance gains and losses. Perhaps there are strong reasons the other way which make it worthwhile. That is why I asked, to understand the issues. Can someone please give reasons with examples, for instance (rather than strong adjectives).

[Kenny Lau]

why would you want to use φ as a variable name in your scenario where you have Nat.φ as an abbrev?

[Siddhartha Gadgil]

Because I want "open scoped Nat" as default and when autoformalizing sources humans often use φ as notation for functions.

[Siddhartha Gadgil]

I mean this happened, hence my raising the issue.

[Siddhartha Gadgil]

There are of course workarounds. I can programatically read the error message, note that this is the cause and then replace φ by another function.

[Siddhartha Gadgil]

But I do think the principle that one should not create reserved words/symbols lightly is reasonable, and should only be violated for strong counter reasons.

[Kenny Lau]

I'm saying that making φ an abbrev has nothing to do with having it as a variable name, sure it parses syntactically when it's an abbrev, but that's still undesirable, and in my opinion adding bad smell to gas so that we can smell it when it's leaking is way better than not having the bad smell just because it smells bad

[Siddhartha Gadgil]

I don't know if you undestood the issue - making it a notation blocks one from using it as a variable name, essentially making it a reserved word.

[Kenny Lau]

i'm saying you shouldn't use it as a variable name in any case, not just in the case where the compiler complains

[Siddhartha Gadgil]

I know what you are saying. But in mathematics we use it all the time, and a lot of work has been done in Lean so that we can write things the same way as we do in human mathematics.

[Kenny Lau]

but you don't need to open Nat all the time

[Siddhartha Gadgil]

Siddhartha Gadgil said:

Because I want "open scoped Nat" as default and when autoformalizing sources humans often use φ as notation for functions.

@Kenny Lau This is getting ridiculous. I asked for an explanation from someone. I am not learning anything.

[Kenny Lau]

I apologise, I'll let someone else address your concerns

[Eric Wieser]

Siddhartha Gadgil said:

Because I want "open scoped Nat" as default

Is this because you want factorial notation? If so, it sounds like the problem is that we have too many notations in the same namespaces?

[Eric Wieser]

Yury G. Kudryashov said:

Another pain point is that we can't conveniently use notation for Real.pi if we also open Nat because of the notation for the prime counting function.

I thought we moved the prime counting function to a different scope namespace? src#Nat.primeCounting says it's in open scoped Nat.Prime as of #15519

[Eric Wieser]

As you can probably guess, this was also motivated by some AI workflow, though as usual this can be translated into an issue that a human learning Lean would also be tripped up by

[Siddhartha Gadgil]

Eric Wieser said:

Siddhartha Gadgil said:

Because I want "open scoped Nat" as default

Is this because you want factorial notation? If so, it sounds like the problem is that we have too many notations in the same namespaces?

Yes, it is for the factorial notation. I agree that using refined scopes is the best solution.

[Yury G. Kudryashov]

Eric Wieser said:

Yury G. Kudryashov said:

Another pain point is that we can't conveniently use notation for Real.pi if we also open Nat because of the notation for the prime counting function.

I thought we moved the prime counting function to a different scope namespace? src#Nat.primeCounting says it's in open scoped Nat.Prime as of #15519

:face_palm: I remember that I had this issue, then I didn't need this for a long time, and now I forgot to check if it's still an issue.