Writing an unexpander for InitialSeg

Stream: new members

[Matt Diamond]

It would be nice if initial segments could appear in the info view as α ≤i β notation (and likewise for the <i notation for principal segments). How would one write an unexpander to enable this? I assume it would be pretty simple but I have no idea what I'm doing when it comes to metaprogramming in Lean.

[Aaron Liu]

does using notation3 to define the notation work?

[Matt Diamond]

oh hmm, I don't know... the notation itself is already defined in mathlib using notation

[Matt Diamond]

but I suppose I could try redefining it using notation3

[Matt Diamond]

it does seem to work (though I had to write a slightly different syntax to avoid overlap with the existing notation)

[Matt Diamond]

I don't know about the differences here but it seems kind of funny that the lean-3 style notation works "better" than the lean 4 version (in the sense that it gives me the info view formatting for free)

[Aaron Liu]

I just copy-pasted the file#Order/InitialSeg into the web editor and changed notation to notation3 on line 67 and the infoview changes from (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2 to α ≤i β

[Matt Diamond]

yeah it definitely works... idk if that's something we want to change in mathlib (edit: probably not)

[Matt Diamond]

I tried to do this in the web editor but it complained about ambiguous syntax, understandably:

import Mathlib.Order.InitialSeg

notation3:25 α:24 " ≤i " β:25 => @InitialSeg α β (· < ·) (· < ·)

example (α β : Type*) [LT α] [LT β] (h : α ≤i β) : α ≤i β :=
by
  exact h

[Matt Diamond]

the doc for notation3 says that it was created primarily for backward compatibility, so I'm curious if there's a more forward-looking approach

[Matt Diamond]

(this isn't that important though, was mostly just wondering if it was something easy to do)

[Aaron Liu]

Matt Diamond said:

yeah it definitely works... idk if that's something we want to change in mathlib (edit: probably not)

why not?

[Matt Diamond]

oh just going off the doc for notation3... it says it has an "uncertain future"

[Ruben Van de Velde]

I think that's no longer accurate, or at least that there's no active plans to remove it

[Matt Diamond]

thanks for the info... I'm still curious why notation3 seems to work better here than notation

is this one of those things where the Lean4 version is more powerful but doesn't give you as much "out of the box", so to speak?

[Aaron Liu]

notation3 creates an delaborator

[Eric Paul]

I asked about it here before #mathlib4 > InitialSeg notation3, it seems like the hope is that notation would do it eventually

[Matt Diamond]

in the section on Notations, the Lean manual says:

When the expansion consists of the application of a function defined in the global environment and each term in the notation occurs exactly once, an unexpander is generated. The new notation will be displayed in proof states, error messages, and other output from Lean when matching function application terms otherwise would have been displayed.

so I'm wondering if the problem is that the notation for InitialSeg doesn't meet the requirements here, or if an unexpander by itself is insufficient

[Aaron Liu]

doesn't meet the requirements

[Aaron Liu]

@InitialSeg α β (fun (x1 : α) (x2 : α) => @LT.lt α inst_1 x1 x2) (fun (x1 : β) (x2 : β) => @LT.lt β inst x1 x2)

[Aaron Liu]

then it becomes obvious that α and β are used multiple times

[Matt Diamond]

ah, that would do it, yeah