Guide for writing notations

Stream: new members

[Ricardo Prado Cunha]

Are there any in-depth guides on writing notations for lean3? All I've found are https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#notation and https://leanprover-community.github.io/mathlib_docs/data/buffer/parser.html; the former doesn't really cover anything complicated like folding and the latter is just definitions without much explanation of how to effectively use them.

[Mauricio Collares]

I know you mentioned lean 3 specifically, but is migrating to lean 4 an option? It has a great macro system (https://arxiv.org/pdf/2001.10490.pdf), and a lot of people will test the "migration flow" now that mathlib3 is less than a month away from being frozen.

[Kyle Miller]

For Lean 3, I'm not sure if the notation command is documented, but if you search through the mathlib source for examples you might be able to hack something together. Note that that second link has nothing to do with the Lean 3 notation parsing. The parser is all written in C++.

[Ricardo Prado Cunha]

Mauricio Collares said:

I know you mentioned lean 3 specifically, but is migrating to lean 4 an option? It has a great macro system (https://arxiv.org/pdf/2001.10490.pdf), and a lot of people will test the "migration flow" now that mathlib3 is less than a month away from being frozen.

We're already using lean3 and migrating to lean4 isn't really an option currently, although it's good to hear that mathlib3 is close to being frozen (which I assume means lean4 is close to having a proper full release rather than just milestone releases? Once that's properly done I might bite the bullet and try to migrate everything over).

[Ricardo Prado Cunha]

Kyle Miller said:

For Lean 3, I'm not sure if the notation command is documented, but if you search through the mathlib source for examples you might be able to hack something together. Note that that second link has nothing to do with the Lean 3 notation parsing. The parser is all written in C++.

Yeah I've been trying to emulate the mathlib source but that's been difficult. Also good to know that data.buffer.parser isn't actually what's used (in hindsight that makes sense since it's not even in core).

[Patrick Massot]

Ricardo Prado Cunha said:

Mauricio Collares said:
it's good to hear that mathlib3 is close to being frozen (which I assume means lean4 is close to having a proper full release rather than just milestone releases?).

Those are completely independent events.

[Jireh Loreaux]

From what I understand, I don't think they are completely independent because mathlib3 frozen means mathlib4 (almost) ported which means Lean 4 will consider a stable release. So I think the former is essentially a prerequisite for the latter.

[Ricardo Prado Cunha]

Patrick Massot said:

Ricardo Prado Cunha said:

Mauricio Collares said:
it's good to hear that mathlib3 is close to being frozen (which I assume means lean4 is close to having a proper full release rather than just milestone releases?).

Those are completely independent events.

I think I misunderstood what freezing means. I interpreted it as meaning that development on mathlib3 will stop, and presumably people will migrate to using mathlib4, which to my knowledge only works with lean4; and I also presume that many people wouldn't want to switch to lean4 if it's far from release.

[Ruben Van de Velde]

I think your last clause is incorrect, at least for people involved in mathlib

[Kyle Miller]

Ricardo Prado Cunha said:

Yeah I've been trying to emulate the mathlib source but that's been difficult.

The next best thing is explaining what sort of syntax you want to have and someone here might help you write a notation to support it.

[Ricardo Prado Cunha]

Kyle Miller said:

The next best thing is explaining what sort of syntax you want to have and someone here might help you write a notation to support it.

There's this syntax I've been able to get to sort of work. Basically I want α ^ n = tuple α n, α ^ n × m = tuple (tuple α n) m, α ^ n × m × j = tuple (tuple (tuple α n) m) j, etc. (where tuple (α : Type u) : ℕ → Type u is a custom inductive type I've made).
I've gotten it to work with parentheses (i.e., (α ^ n × m)) using notation:min `(` t:79 ` ^ `:79 d:(foldl:34 ` × `:34 (n x, tuple x n) t `)` ) := d, but ideally it'd be possible to use without parentheses. Not sure if that's even possible since that might lead to ambiguity in parsing.
As a bit of a workaround I'm also using instance : has_pow (Type u) ℕ := ⟨tuple⟩ since that allows it to work without parentheses for rank 1 (i.e., α ^ n but not α ^ n × m).

[Kyle Miller]

Yeah, I think you either need parentheses, or, better, you could choose new symbols for ^ and × so that they don't conflict with pre-existing notation. I'm not sure whether it's OK to use ( in your notation like that (and definitely this notation will affect how (2 ^ 3) would be parsed).

The notation line looks right given your description, but I can't say for certain whether or not you got the precedences right, I always needed to experiment.

[Kyle Miller]

You might consider avoiding notation and instead using a function where mkTuple [m,n] α = tuple (tuple α n) m

Or you could define a new arrow with right associativity, where say m --> n --> α is tuple (tuple α n) m

[Ricardo Prado Cunha]

Kyle Miller said:

Yeah, I think you either need parentheses, or, better, you could choose new symbols for ^ and × so that they don't conflict with pre-existing notation. I'm not sure whether it's OK to use ( in your notation like that (and definitely this notation will affect how (2 ^ 3) would be parsed).

Yeah I wasn't too confident I could omit the parentheses. Although this doesn't seem to affect things like (2 ^ 3) (doing an #eval on that still gives me 8), probably due to me setting it to precedence :min.
I did use to have it with ^^ and ××, which I don't think have any other definitions, but I still wasn't able to get it to work without parentheses. Removing the open parenthesis says "invalid notation declaration, symbol expected" and removing the closing parenthesis causes it to say invalid expression, `)` expected when I try to actually use it. Removing both makes Lean even more confused.