Notation and term elaborators

[fmontesi]

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.

We will also need to combine notations in nontrivial ways. For example, this is the shape of reductions between typing judgements used in plenty of papers: (Γ ⊢ M : T) → (Γ ⊢ M' : T).

In a Zulip discussion (#computer science > Overloading Lean's notation), we discussed the possibility of using term elaborators. This is an example from Iris: https://github.com/leanprover-community/iris-lean/blob/master/src/Iris/BI/Notation.lean.
Thus we could write things like red(ty(Γ ⊢ M : T) → ty(Γ ⊢ M' : T)) (the nested ty might be unnecessary).

The design of these elaborators will need some thinking, so I'm opening this issue to keep record.

[chenson2018]

I'd like to start with something small to kick this off. Occasionally when applying a lemma or constructor, a ReductionSystem is exposed in the infoview e.g. a term like rs.Red M N instead of the notation we have defined. I think this is a use case for a pretty printer?

Again though, it would need to be a family of pretty printers. I think this is exactly what is happening in this example Kyle provided:

https://github.com/UCSCFormalMethods/LeanLTL/blob/ef8d4c9dd94d3ae85e76328549b70e35551891f2/LeanLTL/TraceSet/Notation.lean#L268-L290

[chenson2018]

In light of #25 (comment) about relying on notation3, I thought I should leave a link to this Zulip thread. If at some later point we want/need to remove this dependency, that thread has the information on how to do something similar ourselves.

[chenson2018]

While my last PR was helpful, I still am seeing some cases where notation3 does not pick up printing I would expect it to. As an example, I am still getting goals like foo.R bar, where R is the relation that should be using a notation. I think I will try adding our own delab/unexpander to catch these. While this may seem like a lot for just reduction arrows, I think it is important to get something that works exactly as intended before we tackle more complicated situations like your example of typing derivations you gave above.