Overloading Lean's notation

Stream: computer science

[Fabrizio Montesi]

(Triggered by the discussion in https://github.com/cs-lean/cslib/pull/17#discussion_r2228569513 with @Chris Henson )
In logic, semantics, and type systems (at least!), we encounter often the situation where we'd like to use important Lean symbols for notation. Examples: T → T for arrow types (functions) in an embedded type system, A → B for implication in an embedded logic, M → N for a reduction, x : T for x has type T, etc.

I can see that:

1. Some formalisation projects, especially in Rocq, do overload the core notation for their embedded systems.
2. Some projects figure out alternative notation.

Is option 1 even feasible in Lean in the long run?
If we instead follow option 2, we should probably agree on some standard 'translation' of the normal pen-and-paper symbol and document it, so that we use it coherently. (Ideally even in code, with type classes.)

[Eric Wieser]

Here you could consider some t(_ → _) elaborator where within the () you're not using regular lean syntax at all

[Fabrizio Montesi]

Is there a convention for how these elaborators should be called? I see a lot of

`(Name| ...)

in docs.

[Eric Wieser]

That's not really the same thing; I'm thinking of things in the style of q(_) and congr(_) and ofNat(_) that are currently in mathlib (though these don't really invent new notation inside the ()s)

[Aaron Liu]

the

`(name| ...)

is a syntax quotation

[Fabrizio Montesi]

Whoops, yes, sorry for the conflation.

[Fabrizio Montesi]

Mmh, so perhaps we could make an appropriately-namespaced term elaborator whenever we wanted this kind of syntax, and then people who wanted to use it easily could just open to get it. Term elaborators might actually also solve some problems we had with taking parameters when we use notation.

[Fabrizio Montesi]

Trying to imagine how this will look in nontrivial places. Here's the reduction of a typing judgement (a concept used in plenty of works):

red(ty(Γ ⊢ M : T) → ty(Γ ⊢ M' : T))

[Kyle Miller]

Here's an example in LeanLTL (short paper). The LLTL[t] macro expands the Lean term t to an LTL interpretation.

LLTL[p → q] expands to p ⇨ q, where ⇨ is the Heyting algebra arrow. There's also a pretty printer that turns Heyting algebra arrows back into LLTL syntax if it's for LTL types.

[Kyle Miller]

This uses macros, but a future version probably will use more hands-on elaboration to control expansion better.

[Fabrizio Montesi]

A sequents in classical linear logic instantiated with the type MyAtom of atomic propositions: cll MyAtom(?a & !b)

[Shreyas Srinivas]

Check the notation file of Iris : https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Notation.lean

[Fabrizio Montesi]

Shreyas Srinivas said:

Check the notation file of Iris

Like this one?

https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Notation.lean

(Crossed over, thx for the link.)

[Fabrizio Montesi]

Iris sells it pretty well, looks nice.
Thanks for the input, everyone. :)

@Chris Henson What do you think of the approach?

[Chris Henson]

Fabrizio Montesi said:

Trying to imagine how this will look in nontrivial places. Here's the reduction of a typing judgement (a concept used in plenty of works):

red(ty(Γ ⊢ M : T) → ty(Γ ⊢ M' : T))

There is no need to nest red(...) and ty(...), this can be done as part of the elab.

In general yes, this was on my radar and seems correct. I have written some simple term elaborators. As I mentioned in a previous PR I'd also like a pretty printer, the examples posted above are helpful for learning how to write one.

I will reply to your comment on the PR regarding some details I believe would need to be worked out.

[Malvin Gattinger]

I don't have much to contribute, but I am curious about such overloaded notation too for other model logics. And @Andrés Goens a while ago wrote these examples, including pretty printing, in the pdl project: https://github.com/m4lvin/lean4-pdl/compare/main...pretty

[Fabrizio Montesi]

Created a related issue: https://github.com/cs-lean/cslib/issues/23

[Andrés Goens]

Malvin Gattinger said:

I don't have much to contribute, but I am curious about such overloaded notation too for other model logics. And Andrés Goens a while ago wrote these examples, including pretty printing, in the pdl project: https://github.com/m4lvin/lean4-pdl/compare/main...pretty

right, that approach is essentially the same as above, just using a different syntactic convention [f|...] instead of f(...)

[Andrés Goens]

the cool think I think is when building these unexpanders that it also shows up on the proof goals

[Fabrizio Montesi]

Term conversion is η-conversion's cool grandchild.