Weird notation conflict handling

Stream: lean4

[Patrick Massot]

The following code works

--import Mathlib.Logic.Relator

notation:25 (priority := high) a:26 " ⇒ " b:25 => a → b

variable (P Q : Prop)

#check  P ⇒ Q
#check  ¬ P ⇒ Q

Uncommenting the first line brings the cursed global notation from https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Logic/Relator.lean#L35 and the second check fails. The thing I don’t understand is why the high priority is enough the avoid the cursed notation in the first check but not in the second one.

[Patrick Massot]

@Sebastian Ullrich this is one more example where being able to simply kill an upstream notation would be a life saver.

[Vlad Tsyrklevich]

I believe your use of :25/:26 are overriding priority := high. Changing them to :50/:51, or getting rid of them and letting priority := high take control both work for me.

[Kevin Buzzard]

If core won't let us kill an upstream notation then I guess here at least we can fix it in mathlib by scoping the infixr:40 " ⇒ " => LiftFun notation in Mathlib.Logic.Relator. It does seem a bit weird that a symbol which all mathematicians know the meaning of is globally stolen to mean something completely different.

[Sebastian Ullrich]

Patrick Massot said:

Sebastian Ullrich this is one more example where being able to simply kill an upstream notation would be a life saver.

Would something like attribute [-term_parser] term_⇒_ be acceptable, under the extra limitation that the tokens stay registered (i.e. you can use them in a new notation, but you cannot undo notation "pi" removing that identifier)? If yes, then that is a bit more feasible, could you open an issue?

[Eric Wieser]

Vlad Tsyrklevich said:

I believe your use of :25/:26 are overriding priority := high. Changing them to :50/:51, or getting rid of them and letting priority := high take control both work for me.

I would guess this is because you can't override the same notation with different precedence?

[Patrick Massot]

Kevin Buzzard said:

If core won't let us kill an upstream notation then I guess here at least we can fix it in mathlib by scoping the infixr:40 " ⇒ " => LiftFun notation in Mathlib.Logic.Relator. It does seem a bit weird that a symbol which all mathematicians know the meaning of is globally stolen to mean something completely different.

Sure, I will also PR a fix to Mathlib. But for teaching I’m stuck with an old Mathlib until next year.

[Patrick Massot]

Sebastian Ullrich said:

Patrick Massot said:

Sebastian Ullrich this is one more example where being able to simply kill an upstream notation would be a life saver.

Would something like attribute [-term_parser] term_⇒_ be acceptable, under the extra limitation that the tokens stay registered (i.e. you can use them in a new notation, but you cannot undo notation "pi" removing that identifier)? If yes, then that is a bit more feasible, could you open an issue?

Yes, that would already be much better.

[Patrick Massot]

Vlad Tsyrklevich said:

I believe your use of :25/:26 are overriding priority := high. Changing them to :50/:51, or getting rid of them and letting priority := high take control both work for me.

Thanks, I’ll try those. But I am a bit worried this will break other things. And it doesn’t really explain the mystery.

[Vlad Tsyrklevich]

I am also curious to understand why it fails. I tried to look through Elab traces and read through the language reference manual, but I didn't figure it out

[Sebastian Ullrich]

Because with the Relator notation, it is parsed as ¬ (P ⇒ Q) while without it, it is parsed as (¬ P) ⇒ Q, so priority does not come into play as there is no choice between the two notations at a single location. The former parse is preferred by the "local longest parse" rule: once we're parsing inside the Not, we prefer parsing there as much as possible before ascending.

[Kim Morrison]

chore: scope ⇒ notation to Relator #22419