parsing question about `∥x∥`

Stream: general

[Kevin Buzzard]

I am surprised about the following:

import analysis.normed_space.basic

example (α : Type) [has_norm α] [has_add α] (x y : α) :
  ∥x + y∥ ≤ max ∥x∥ ∥y∥ := sorry -- doesn't compile :-(

The error is

type mismatch at application
  ∥x + y∥ ≤ max
term
  max
has type
  ?m_1 → ?m_1 → ?m_1 : Type ?
but is expected to have type
  ℝ : Type
-/

In analysis.normed_space.basic we have this:

class has_norm (α : Type*) := (norm : α → ℝ)

export has_norm (norm)

notation `∥`:1024 e:1 `∥`:1 := norm e

but yet if I #print notation \|| I get

`∥`:1 _:1 `∥`:1 := has_norm.norm #0

In fact even the following file doesn't make the binding power go above 1:

def norm : Type := sorry

notation `∥`:1024 e:1 `∥`:1 := norm e

#print notation ∥ -- `∥`:1 _:1 `∥`:1 := norm #0

What have I misunderstood here?

[Kevin Buzzard]

def norm : Type := sorry

notation `∥`:512 e:37 `∥`:999 := norm e

#print notation ∥ -- `∥`:999 _:37 `∥`:999 := norm #0

Is this to be expected? I can't have the first and second \|| with different binding power? This is clearly not what the authors of analysis.normed_space.basic were expecting.

[Eric Wieser]

I think binding power is global per-token?

[Kevin Buzzard]

But ∥x + y∥ ≤ max ∥x∥ ∥y∥ is a set phrase in nonarchimedean geometry! Can we not get it to parse? ∥x + y∥ ≤ (max ∥x∥ ∥y∥) is the current workaround.

[Eric Wieser]

How does parsing fail if you use 1024 for both priorities?

[Kevin Buzzard]

`⌊`:1024 _:1 `⌋`:1 := floor #0 is the correct choice, so it seems; it's just that we are bitten by both sides being the same token.

[Kevin Buzzard]

with 1024 on both I get two invalid expression errors, it's hard to tell what's going wrong.

[Kevin Buzzard]

one red squiggle under \le, the other under ||y||

[Mario Carneiro]

Yeah, bracketing operators that are the same on both sides are nasty to parse, for example |x+|+f|y|+z|+z|

[Mario Carneiro]

I think there are vertical bar tokens in unicode with little left/right ticks on them that are an okay compromise IMO

[Kevin Buzzard]

Mario Carneiro said:

Yeah, bracketing operators that are the same on both sides are nasty to parse, for example |x+|+f|y|+z|+z|

You just need good spacing :-)

[Kevin Buzzard]

@Patrick Massot @Heather Macbeth @Sebastien Gouezel @Yury G. Kudryashov did you never have problems with parsing and \||? If not then you are presumably not too interested in the idea of replacing it with some variant of lfloor and rfloor (or any other two different tokens). What you have here in analysis.normed_space.basic is being ignored by the parser -- the 1024 is apparently overruled by the 1, which is quite a big difference! I'm surprised this issue didn't show up sooner. Or maybe it did and you know about it...

[Eric Wieser]

How about the "new" tokens (∥x + y∥) - I hear parts of mathlib already use those /s

[Mario Carneiro]

that also works here, if you write ∥x + y∥ ≤ max (∥x∥) (∥y∥)

[Mario Carneiro]

Suggestion: ⸡x⸠

[Mario Carneiro]

Note that unicode calls ⸠ the left and ⸡ the right, but I think it makes more sense with the quills pointing out rather than in

[Eric Wieser]

That's "⸡x⸠" for android users

[Yury G. Kudryashov]

You've pasted the same symbol, so we see the same symbol.

[Yury G. Kudryashov]

@Kevin Buzzard Sometimes I see parsing errors and add parentheses.

[Alex J. Best]

How about a subscript?

import data.real.basic
class has_norm (α : Type*) := (norm : α → ℝ)

export has_norm (norm)

notation `∥`:1024 e:1 `∥ₙ`:1 := norm e

example (α : Type) [has_norm α] [has_add α] (x y : α) :
  ∥x + y∥ₙ ≤ max ∥x∥ₙ ∥y∥ₙ := sorry

seems to work fine and looks way more mathematically reasonable than ⸡x⸠

[Alex J. Best]

(ₙ for norm :smile: )

[Mario Carneiro]

What's mathematically unreasonable about it? I think the quills are almost invisible, just barely big enough that you can tell which is which. Just look at them as vertical bars with an orientation

[Mario Carneiro]

FYI I got the idea from mathematica, which uses characters that look essentially like this when you use the absolute value notation

[Mario Carneiro]

https://reference.wolfram.com/language/ref/character/LeftBracketingBar.html

[Mario Carneiro]

Drawn in monospaced fonts with a small left‐pointing tee to indicate direction.

I guess they draw it as a plain vertical bar in "presentation mode"

[Alex J. Best]

Mario Carneiro said:

What's mathematically unreasonable about it? I think the quills are almost invisible, just barely big enough that you can tell which is which. Just look at them as vertical bars with an orientation

Well I've never seen that character used in a math paper and if I saw it out of context I would have less idea what it meant than ∥y∥ₙ, and I assume most mathematicians would feel the same. A big strength of lean for me is that I can show mathematicians who don't know lean formalized statements and quite often they can understand them, I think using less "weird" symbols helps with this psychologically.

[Alex J. Best]

Alex J. Best said:

(ₙ for norm :smile: )

Actually I guess one issue with n is that it might be interpreted as "some natural number"

[Mario Carneiro]

I would hope that the context makes it clear:

example (α : Type) [has_norm α] [has_add α] (x y : α) : ⸡x + y⸠ ≤ max ⸡x⸠ ⸡y⸠ := sorry

Frankly I think there are much worse offenders when it comes to the set of unicode characters we use, like all the arrow variations. This is a vertical bar variation, and it's maybe not obvious what the variation means but that's going to be true for any notation - at some point you have to actually look it up or guess based on the names of theorems about it. I don't like a subscript n because then it looks parameterized, like a p-norm or something

[Mario Carneiro]

I think being able to visually see the difference between the left and right delimiters is also useful for human consumers. I think the mathematica design is telling: they use the plain bars for presentation but make the left/right thing visible in the monospace font so that authors don't confuse the two

[Heather Macbeth]

Personally, I'd rather keep the current notation, and just add parentheses when Lean can't figure it out . . . I really value that Lean code is semi-readable to outsiders, I think any step away from standard math notation should be very carefully weighed.

[Heather Macbeth]

@Alex J. Best's suggestion just shows up to me as blank boxes ... maybe I don't have the right fonts installed, but again, half our newcomer readers also won't?

[Alex J. Best]

That's very strange, they show as boxes for me too on Android (as does Mario's suggestion) but apart from the subscript I just copy pasted the usual norm bars from Kevin's post which do show on my phone. So I have no idea how those characters could have ended up different

[Johan Commelin]

will Lean4's parser be able to deal with the problem better? I got the impression that it's quite a bit more powerful. If so, I wouldn't refactor the notation just to switch back in half a year.

[Sebastien Gouezel]

I'm on the same line as Heather and Yury here. We know that the current notation works fine if we are ready to add parentheses when it doesn't :-) And it has the very valuable advantage of being self-explanatory. So I wouldn't change it.

[Eric Wieser]

As less offensive notation, could a subscript go on the closing ||?

[Kevin Buzzard]

Yes I also very much value the fact that right now it's readable and any change will make it less so. This is very much an area where the CS people don't seem to understand the value of this, I had some Twitter spat recently with a few people who argued that all unicode notation was bad because it just added an extra layer of unnecessary noise. Ok if it doesn't cause too many problems I think we should leave it. I'm still very much interested in the question about whether this issue can be fixed in lean 4

[Eric Wieser]

Like, perhaps $\|x\|_r$ with r standing for $\mathbb{R}$

[Kevin Buzzard]

This is the other option but we've just heard from the people who use this notation a lot that it doesn't seem to be a problem in practice

[Sebastian Ullrich]

Johan Commelin said:

will Lean4's parser be able to deal with the problem better? I got the impression that it's quite a bit more powerful. If so, I wouldn't refactor the notation just to switch back in half a year.

It turns out that this works out of the box in Lean 4.

axiom max {α} : α → α → α
axiom norm {α} : α → α
notation "∥" e "∥" => norm e

#check fun (x y : Nat) => ∥x + y∥ ≤ max ∥x∥ ∥y∥

I was a bit surprised by that, but the secret is that function application in Lean 4 has to include whitespace. So y∥ is not confused as an incomplete application.

[Patrick Massot]

This is somehow an accident though. It doesn't answer the question: could we assign different binding power to the opening and closing ∥? Or is it no longer a meaningful question?

[Sebastian Ullrich]

Correct, it is no longer meaningful because precedences are now associated with parsers, i.e. e and the whole notation. Nor would an extended Lean 3 model help: You have to tell the parser that y∥ is not a valid start point of the notation, but max ∥ is. That cannot be solved with precedences alone. The parser (or any such parser) is not even thinking about the precedence of the closing ∥ at this point.

[Kevin Buzzard]

This is good news, presumably? Are you saying that this whole "|":a e:b "|":c thing with three numbers was a hack all along? Does Lean 4 use a Pratt parser? My understanding of binding is based on this.

[Sebastian Ullrich]

It does, I've written a bit about it at https://leanprover.github.io/lean4/doc/syntax.html. Do tell me if that's intelligible for non-CS audiences :) .

[Sebastian Ullrich]

Kevin Buzzard said:

This is good news, presumably? Are you saying that this whole "|":a e:b "|":c thing with three numbers was a hack all along?

Well, now it's two numbers (the expanded form is notation:max "∥" e:0 "∥" => norm e), but at least they're now local to the notation. I'm not sure right now if the third number ever mattered in Lean 3 either.

[Kevin Buzzard]

While introducing new notations is a relatively rare feature in programming languages and sometimes even frowned upon because of its potential to obscure code, it is an invaluable tool in formalization for expressing established conventions and notations of the respective field succinctly in code.

Did you see the Twitter conversation I had about this? Andrej Bauer asked a maths question in Coq and my initial reaction was "that is so ugly to read, here is how it looks in Lean, mathematicians can read my version" and then several people popped up saying "unicode is just a stupid gimmick, it makes people's lives worse" and I was just dumbfouded. I will say it again -- on several occasions mathematicians have said to me that they are attracted to Lean because it looks more readable to them than the other languages. I think it is marvellous that we are going in this direction. The CS people were arguing that it adds an extra layer of obfuscation. What they don't seem to realise is that for mathematicians it is serious unobfuscation. It is a translation which is bridging the gap between our two worlds.

[Eric Wieser]

Heather Macbeth said:

Alex J. Best's suggestion just shows up to me as blank boxes ... maybe I don't have the right fonts installed, but again, half our newcomer readers also won't?

Mathlib is full of notation that doesn't render properly in zulip on android - even linear maps often don't. I don't think we should consider zulip android monospace font bugs in mathlibs design. Discounting the blank box complaint, do you still prefer (∥x + y∥) over ∥x + y∥ₙ?

[Gabriel Ebner]

Is that a zulip bug though? It seems to be limited to certain android versions. (IIRC you mentioned that you couldn't see the characters on github either.)

[Kevin Buzzard]

This is fixed in Lean 4 so for me the matter of whether we should change notation is now closed.

[Sebastian Ullrich]

Kevin Buzzard said:

Did you see the Twitter conversation I had about this?

I did, and I agree with you (modulo choice of words :) ). I'm pretty sure though that this wasn't "CS people" but (mostly) "Coq people". No-one coming from Agda would challenge use of Unicode, while in Isabelle they're not even content with Unicode but use their own extended markup, font, and text rendering (so if you want an ITP that actually allows you to put \N in the subscript...).

[Mario Carneiro]

Sebastian Ullrich said:

the secret is that function application in Lean 4 has to include whitespace. So y∥ is not confused as an incomplete application.

Does this mean that folks can't pretend lean has C style function call syntax anymore, e.g. f(x, y, z) (which works as long as f : A x B x C -> D)?

[Mario Carneiro]

I'm not sure how common this is, but I routinely see people posting lean 3 proofs using things like P(sin(x))

[Sebastian Ullrich]

Mario Carneiro said:

Sebastian Ullrich said:

the secret is that function application in Lean 4 has to include whitespace. So y∥ is not confused as an incomplete application.

Does this mean that folks can't pretend lean has C style function call syntax anymore, e.g. f(x, y, z) (which works as long as f : A x B x C -> D)?

Even better, they can now implement that syntax properly without clashing with the internal application syntax, and then reevaluate their life choices.