notation3

Stream: mathlib4

[Jireh Loreaux]

How do I convert mathport's notation3 into valid Lean 4 notation? e.g.,

notation3 "Σₗ "(...)", "r:(scoped p => Lex Sigma p) => r

[Eric Wieser]

I would guess that you can find where the notation for Sigma is defined, and basically write the same thing

[Eric Wieser]

Surely that should say Lex (Sigma p)... Is this a mathport bug?

[Jireh Loreaux]

it definitely should be Lex (Sigma p). Copying and pasting the mathlib3 version and making modifications gave me:

notation  `Σₗ` binders `, ` r:(scoped p => _root_.Lex (Sigma p)) => r

which still doesn't work, it complains at Σ that it expected => and it complains at p: `expected '[', 'binder_predicate', 'elab', 'elab_rules', 'infix', 'infixl', 'infixr', 'instance', 'macro', 'macro_rules', 'notation', 'postfix', 'prefix', 'syntax' or 'unif_hint'

[Eric Wieser]

I meant find the mathlib4 notation for Sigma, and then replace Sigma p there with Lex (Sigma p)

[Eric Wieser]

Although the Sigma notation comes from here, and the generalization isn't so obvious: https://github.com/leanprover/lean4/blob/1b5029222859a52ad1afcd23f5fbfd64b047e17a/src/Init/NotationExtra.lean#LL84C52-L84C73

[Eric Wieser]

https://github.com/leanprover/lean4/blob/1b5029222859a52ad1afcd23f5fbfd64b047e17a/src/Init/NotationExtra.lean#L179-L181also looks relevant

[Jireh Loreaux]

Yea, I was just looking that.

[Jireh Loreaux]

yeah, but I don't see how to make it work.

[Mario Carneiro]

I think we should just use notation3 for the port

[Mario Carneiro]

We will want to do something to make it easy to declare binders anyway

[Jireh Loreaux]

notation3 wasn't working either.

[Mario Carneiro]

not working how?

[Jakob von Raumer]

Just porting Data.PSigma.Order (mathlib4#815), so I'm running into the same thing. Keeping notation3 for now seems okay, small problem is that it does not accept docstrings.

[Jakob von Raumer]

I'll try to fix it

[Jakob von Raumer]

Fixed

[Yaël Dillies]

Please please please port data.sigma.order and data.psigma.order simultaneously.

[Yaël Dillies]

There's a reason why I cross-ref both files.

[Ruben Van de Velde]

That's a bit late, since mathlib4#815 already landed

[Jireh Loreaux]

Sorry, I've been out for a few days with strep throat, otherwise I would have taken your advice Yaël.

[Patrick Massot]

What is the current status of notation3. Should I keep

notation3 "⨆ "(...)", "r:(scoped f => supᵢ f) => r

or should I use

open Std.ExtendedBinder in
syntax "⨆ " extBinder ", " term:51 : term

macro_rules
  | `(⨆ $x:ident, $p) => `(supᵢ fun $x:ident ↦ $p)
  | `(⨆ $x:ident : $t, $p) => `(supᵢ fun $x:ident : $t ↦ $p)
  | `(⨆ $x:ident $b:binderPred, $p) =>
    `(supᵢ fun $x:ident ↦ satisfiesBinderPred% $x $b ∧ $p)

[Patrick Massot]

Note for future readers: it took me a long time to understand that mathport adds those notation3 command but does not add the relevant imports

import Mathlib.Mathport.Notation
import Init.NotationExtra

[Patrick Massot]

And then am I right to think that whatever the answer to my first question above, it should be followed by

@[app_unexpander supᵢ]
def supᵢ.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $x:ident ↦ $p) => `(⨆ $x:ident, $p)
  | `($_ fun $x:ident : $ty:term ↦ $p) => `(⨆ $x:ident : $ty:term, $p)
  | _ => throw ()

[Mario Carneiro]

Patrick Massot said:

Note for future readers: it took me a long time to understand that mathport adds those notation3 command but does not add the relevant imports

import Mathlib.Mathport.Notation
import Init.NotationExtra

You don't need the second import. As in lean 3, any import starting with Init.* is imported by default in every lean file

[Mario Carneiro]

I think you should use notation3 with the import for now. I think we need something in this space, not sure if the notation3 syntax is exactly the way we want to spell it, but clearly those unexpanders are just a bunch of boilerplate and this is what macros are for

[Patrick Massot]

Sorry about the spurious import, I copy-pasted from somewhere without thinking.

[Patrick Massot]

The unexpander is needed in any case, right?

[Patrick Massot]

I mean notation3 does not do it.

[Patrick Massot]

How do we put doc on a notation3? The doc blame linter complains, and the inherit_doc attribute doesn't seem to work.

[Patrick Massot]

Actually a regular docstring seems to work.

[Mario Carneiro]

mathlib4#1090