Priority of notation

Stream: general

[Antoine Chambert-Loir]

I have defined a notation

notation:25 α " →[" M:25 "] " β:0 => EquivariantMap (@id M) α β

which conflicts with the one for MulActionHom. Because of that ambiguity, Lean stops.
I tried to insert (priority := 1000) , without success…
How can I make mine to be chosen automatically?

[Eric Wieser]

I think 1000 is the default priority so providing that won't do anything

[Antoine Chambert-Loir]

By without success, I meant that I got an error message.
Where should I insert the priority attribute? I tried notation (priority := 1000) :25…

[Junyan Xu]

Many examples are found by searching the repo, for example this. M:25 β:0 don't feel right to me ... Oops it's used here.

[Eric Wieser]

:25 is precedence not priority

[Junyan Xu]

What does it mean to put a precedence on a variable?

[Kyle Miller]

@Antoine Chambert-Loir I believe the priority goes after the :25.

[Kyle Miller]

Just to confirm, here is the syntax definition for notation.

Here's what that means using simplified syntax-like notation:

(docComment)? (attributes)? attrKind
"notation" (precedence)? (namedName)? (namedPrio)? notationItem* "=>" term

The attrKind is ("scoped" <|> "local")?, the namedName is "(name :=" ident ")", and the namedPrio is "(priority :=" priority ")".

[Kyle Miller]

The priority parser has a number of named priority levels by the way. There's default, low, mid, and high, and you can write expressions involving +, -, and parentheses.

[Florent Schaffhauser]

I was looking for previous threads on notation and precedence and ended up here but I have not been able to use the explanations given above to solve the following problem (of which I am not sure that it is due to a precedence issue).

Here is an MWE:

import Mathlib.Tactic.Ring

def AddElem {R : Type} (P : Set R) (a : R) : Set R :=
P ∪ {a}

variable (S : Set ℚ)
#check AddElem S (0 : ℚ)  -- AddElem S 0 : Set ℚ
#check AddElem S 0  -- AddElem S 0 : Set ℚ

notation:max P"["a"]" => AddElem P a
#check S[(0 : ℚ)] -- S[0] : Set ℚ
#check S[0]  -- ambiguous, possible interpretations ⏎ S[0] : Set ℚ ⏎ ⏎ S[0] : ?m.8100

The issue is that S[0] is not recognized if I do not write S[(0 : ℚ)], while AddElem S 0 works just fine without specifying (0 : ℚ). I'm stuck!

[Eric Wieser]

If you hover over the error message, you can see the second one is getElem (aka list indexing notation)

[Kyle Miller]

You could set the priority. I think it's notation:max (priority := high) P"["a"]" => AddElem P a

You might need to stick noWs (capitalization might be wrong) between P and "[" to force no whitespace.

[Florent Schaffhauser]

Thank you both! The following options work, so it seems that [ is more difficult to handle than (.

import Mathlib.Tactic.Ring

def AddElem {R : Type} (P : Set R) (a : R) : Set R := P ∪ {a}

variable (S : Set ℚ)
#check AddElem S (0 : ℚ)  -- AddElem S 0 : Set ℚ
#check AddElem S 0  -- AddElem S 0 : Set ℚ

notation:max P"("a")" => AddElem P a
#check S((0 : ℚ))  -- S(0) : Set ℚ
#check S(0)  -- S(0) : Set ℚ

notation:max (priority := high) P"["a"]" => AddElem P a
#check S[(0 : ℚ)]  -- S[0] : Set ℚ
#check S[0]  -- S[0] : Set ℚ

[Kyle Miller]

I think we might want to set the priority like this in parts of mathlib -- [ and ] are used in probability theory for things like expectations, and that also runs into this issue.

By the way, there are two other ways to disambiguate this. The first is to give an expected type, like (S[0] : Set ℚ), since that causes the elaborator to disambiguate. The second is to write S [0] since the GetElem notation requires there to be no space.

[Patrick Massot]

Speaking of precedence and priorities, does anyone know how to put precedence so that notation (priority := high) a " ⇒ " b => a → b works as expected? I did not manage to find where the arrow notation is defined in core.

[Patrick Massot]

Is notation:25 (priority := high) a " ⇒ " b:0 => a → b the correct incantation?

[Patrick Massot]

It works on my sample of one example that failed without precedence info and is lifted from our linear maps notation.

[Patrick Massot]

And for extra credit, I'm interested in having a delaborator that triggers only when it should. Using notation3 does create a delaborator but it triggers to much and I see ℕ ⇒ n ≥ N ⇒ |u n - l| ≤ ε / 2

[Patrick Massot]

The core Lean Lean.PrettyPrinter.Delaborator.delabForall is full of call to private function whose code doesn't work when copy pasted in a project :sad:

[Mario Carneiro]

Patrick Massot said:

Speaking of precedence and priorities, does anyone know how to put precedence so that notation (priority := high) a " ⇒ " b => a → b works as expected? I did not manage to find where the arrow notation is defined in core.

I think it would be notation:25 (priority := high) a:26 " ⇒ " b:25 => a → b

[Patrick Massot]

This also works on my sample.

[Patrick Massot]

Any idea about how to delaborate it?

[Kyle Miller]

@Patrick Massot What does "when it should" mean? If you use notation3 instead it'll be used for arrow functions in general. Do you want it to work just for propositions?

[Patrick Massot]

Yes.

[Patrick Massot]

I simply want to use normal notations for teaching.

[Patrick Massot]

So ⇒ means implies and nothing else, and nothing else means implies.

[Kyle Miller]

I tested this with three whole examples:

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

open Lean PrettyPrinter Delaborator SubExpr in
@[delab forallE]
def delabDoubleArrow : Delab := do
  let e ← getExpr
  unless e.isArrow do failure
  unless ← (Meta.isProp e.bindingDomain! <&&> Meta.isProp e.bindingBody!) do failure
  let p ← withBindingDomain delab
  let q ← withBindingBody `a delab
  `($p ⇒ $q)

[Patrick Massot]

This is very promising but breaks bounded quantifiers.

[Patrick Massot]

I see ∀ (ε : ℝ), ε > 0 ⇒ ∃ N, ∀ (n : ℕ), n ≥ N ⇒ |u n - l| < ε

[Patrick Massot]

It needs to collaborate with https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Util/Delaborators.lean#L48

[Kyle Miller]

I guess there's this then:

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

open Lean PrettyPrinter Delaborator SubExpr

def delabDoubleArrow : Delab := do
  let e ← getExpr
  unless e.isArrow do failure
  unless ← (Meta.isProp e.bindingDomain! <&&> Meta.isProp e.bindingBody!) do failure
  let p ← withBindingDomain delab
  let q ← withBindingBody `a delab
  `($p ⇒ $q)

@[delab forallE]
def delabPi : Delab := whenPPOption Lean.getPPNotation do
  let stx ← delabDoubleArrow <|> delabForall
  match stx with
  | `(∀ ($i:ident : $_), $j:ident ∈ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ∈ $s, $body) else pure stx
  | `(∀ ($x:ident : $_), $y:ident > $z ⇒ $body) =>
    if x == y then `(∀ $x:ident > $z, $body) else pure stx
  | `(∀ ($x:ident : $_), $y:ident < $z ⇒ $body) =>
    if x == y then `(∀ $x:ident < $z, $body) else pure stx
  | `(∀ ($x:ident : $_), $y:ident ≥ $z ⇒ $body) =>
    if x == y then `(∀ $x:ident ≥ $z, $body) else pure stx
  | `(∀ ($x:ident : $_), $y:ident ≤ $z ⇒ $body) =>
    if x == y then `(∀ $x:ident ≤ $z, $body) else pure stx
  | `(Π ($i:ident : $_), $j:ident ∈ $s ⇒ $body) =>
    if i == j then `(Π $i:ident ∈ $s, $body) else pure stx
  | `(∀ ($i:ident : $_), $j:ident ∉ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ∉ $s, $body) else pure stx
  | `(∀ ($i:ident : $_), $j:ident ⊆ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ⊆ $s, $body) else pure stx
  | `(∀ ($i:ident : $_), $j:ident ⊂ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ⊂ $s, $body) else pure stx
  | `(∀ ($i:ident : $_), $j:ident ⊇ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ⊇ $s, $body) else pure stx
  | `(∀ ($i:ident : $_), $j:ident ⊃ $s ⇒ $body) =>
    if i == j then `(∀ $i:ident ⊃ $s, $body) else pure stx
  | _ => pure stx

[Patrick Massot]

It seems to work, thanks!

[Patrick Massot]

It is almost frightening to see Lean code that looks so much like real math. I fear Lean will spend more and more time spying on my traditional math courses to see whether I'm cheating.

[Patrick Massot]

I really don't understand how we can end up with notations such as https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Order/SymmDiff.lean#L70-L76 unscoped. There is even a comment saying this is a bad idea!

[Patrick Massot]

And I am also curious to know why import Mathlib.Tactic pulls in that cursed file.

[Patrick Massot]

OMG, it is imported by Mathlib/Data/Set/Basic.lean!

[Patrick Massot]

Sanity is hopefully restored in #9844 but I didn't try to build locally since there 26 files all over mathlib that use those notations (in at most three declarations in almost every case...).

[Patrick Massot]

And it seems to build!

[Yaël Dillies]

Why do you it is that bad? You're not working on the Laplacian yet, are you?

[Kevin Buzzard]

Maybe this is the blocker! We'll need it for FLT!

[Patrick Massot]

The one that was in my way was infixl:100 " ⇔ " => bihimp. But having a single letter notation in global scope is bad independently of any other use.

[Eric Wieser]

Well, the symbols do mean the same thing! (docs#bihimp_iff_iff)

example (A B : Prop) : (A ⇔ B) = (A ↔ B) := by simp

[Eric Wieser]

(the same is true for example (A B : Prop) : (A ⇨ B) = (A → B) := rfl)

[Eric Wieser]

I wonder if bihimp should be adjusted so that the first one is also true by rfl

[Yaël Dillies]

Patrick Massot said:

The one that was in my way was infixl:100 " ⇔ " => bihimp. But having a single letter notation in global scope is bad independently of any other use.

That's not a letter! That's \inc.

[Yaël Dillies]

Eric Wieser said:

I wonder if bihimp should be adjusted so that the first one is also true by rfl

This is not possible without adding it as a field to docs#HeytingAlgebra since docs#Iff is a custom structure instead of being defined using docs#And

[Mario Carneiro]

Yaël Dillies said:

Patrick Massot said:

The one that was in my way was infixl:100 " ⇔ " => bihimp. But having a single letter notation in global scope is bad independently of any other use.

That's not a letter! That's \inc.

I'm pretty sure he's talking about ∆ just above it

[Yaël Dillies]

Yes, and that's not \D, that's \inc.

[Yaël Dillies]

It used to be \D, which caused trouble in category theory files which used \D to denote shapes (IIRC), so I changed it to \inc.

[Kyle Miller]

(And that was justified because we had found some sources where it said that in unicode, ∆ is for symmetric differences, among some other things.)

[Patrick Massot]

I am sorry about all this confusion. Again, the thing that triggered a bug in my code yesterday is infixl:100 " ⇔ " => bihimp. When I tracked it down I saw that the neighboring definition was explicitly flagged as problematic so I scoped both. But I didn't realize the delta-looking letter was not a unicode delta.

[Mauricio Collares]

Should \inc be unscoped notation, then?