Local notations : issue and workaround

Stream: lean4

[Julien Marquet]

I'm interested in defining local notations, to have for instance fancy group laws, custom symbols for orders, etc.

It looks like I'm not the only one interested in this (there are already issues #435 and #358 that are close to my point), so I'll write here

• A minimal example of the problem
• A (not fully satisfying) workaround
• The tracks that I've found to solve this issue (and that I couldn't follow on my own :/)

[ This is a lengthy post because I just summarize what I have found. I would have loved to have simply fixed the issue, PR'd Lean 4 and just announced the feature without making too much noise but this is out of my reach :/ ]

---

The problem arises in scenarios like this one :

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel : O → O → Prop)
infixl:50 " ◃ " => rel

theorem foo : ∀ x y : O, x ◃ y :=
by /- Goal is `∀ (x y : O), rel x y` :'( -/ admit

So here's a workaround if you want fancy notation and pretty printing !

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel : O → O → Prop)
infixl:50 " ◃ " => id rel
@[appUnexpander id] def unexpandAppRel : Lean.PrettyPrinter.Unexpander
  | `(id rel $x $y) => `($x ◃ $y)
  | _ => throw ()

theorem foo : ∀ x y : O, x ◃ y :=
by /- Goal is `∀ (x y : O), x ◃ y` !! -/ admit

The Unexpander just finds all the instances of app rel x y and displays them as x ◃ y.
This pattern works well in more compex cases. Here is an example that demonstrates this, and by the way I give examples of what does _not_ work :

set_option quotPrecheck.allowSectionVars true

variable (O : Type) (rel rel' : O → O → O)

infixl:70 " ◃ " => id rel -- Notice we can directly use `infixl`
@[appUnexpander id] def unexpandAppRel : Lean.PrettyPrinter.Unexpander
  | `(id rel $x $y) => `($x ◃ $y)
  | _ => throw ()

-- This one does _not_ work (explained just after)
@[appUnexpander rel] def unexpandRel : Lean.PrettyPrinter.Unexpander
  | `(rel $x $y) => `($x ◃ $y)
  | _ => throw ()

theorem foo : ∀ x y z : O, x ◃ y ◃ z = rel x y :=
by
  -- Goal is : ∀ (x y z : O), x ◃ y ◃ z = rel x y
  admit

#print foo -- Prints correctly "x ◃ y ◃ z" but still prints "rel" on the right

Up to my understanding, the original problem arises from mkSimpleDelab :

• It only accepts right hand side expressions that are just a function (no function applications, because functions and function applications are _not_ the same syntactically), which rules out the app rel rhs;
• And the function that is given must be global, which makes having rel in the rhs impossible because rel was introduced by variable.

And apparently it isn't possible to use a local name as a parameter to appUnexpander (or I didn't understand how to do that).

[Mac]

actually, this is something I find quite useful myself and have been playing around with a lot

[Mac]

first thing to note is that you could use the builtin id instead of having to use define your own app

[Mac]

also, the idea of using app/id this way in order to able to write an appUnexpander is genius! I never would have thought of that!

[Julien Marquet]

Mac said:

first thing to note is that you could use the builtin id instead of having to use define your own app

This is indeed better with id, thanks ! I updated my original message.

[Julien Marquet]

I opened an issue on lean4 : #465

[Mac]

Fyi, I had a related discussion a while back: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Custom.20identifiers.3F/near/234451179 and @Sebastian Ullrich (a Lean 4 developer) suggested some ways local notation may be addressed in the future