big ops

Stream: general

[Johan Commelin]

What do people think of

@[to_additive]
abbreviation fintype.prod (f : α → γ) := finset.univ.prod f

localized "notation `∑` binders `, ` r:(scoped f, fintype.sum f) := r" in big_operators
localized "notation `∏` binders `, ` r:(scoped f, fintype.prod f) := r" in big_operators

localized "notation `∑` binders ` in ` s `, ` r:(scoped f, finset.sum s f) := r" in big_operators
localized "notation `∏` binders ` in ` s `, ` r:(scoped f, finset.prod s f) := r" in big_operators

@Patrick Massot I know that this is a very meagre substitute for the big ops library in coq. But I think it's better to wait for Lean 4 before we start a big refactor. In the mean time, this notation seems like a cheap way to improve readability.

[Patrick Massot]

Does this actually work? I mean both the fintype and finset version at the same time.

[Patrick Massot]

Oh I see, the notation is subtly different

[Patrick Massot]

The question still stands, but I'm more optimistic

[Johan Commelin]

@Patrick Massot See https://github.com/leanprover-community/mathlib/pull/1564/files/88a5f988abd92ea699824d72dd8c0fcdd5cd4ac0..60f01102933198521d31c2d58ad07651a23dccec#diff-c5bb8de7cb26ae773e9bcb3fa594be6fL57-R230 for a short proof of concept

[Patrick Massot]

Yes, I saw, that's wonderful. My question is specifically about coexistence of the two variations. Do you use both in that file?

[Johan Commelin]

Yes, I do.

[Johan Commelin]

@Patrick Massot The first calc in the proof mixes them, for example.

[Patrick Massot]

amazing

[Sebastien Gouezel]

Would that conflict with

notation `∑` binders `, ` r:(scoped f, tsum f) := r

in topology/algebra/infinite_sum? (If necessary, we could also localize this one).

[Patrick Massot]

People will probably want to use both when discussing partial sums.

[Sebastien Gouezel]

I would be ok with ∑' for the infinite sum, and the other notations introduced by Johan.

[Johan Commelin]

Yes, I also thought about that, and I think the ' version would be best.

[Johan Commelin]

To what extent could this refactor be done with a regex? Because I fear it will be a lot of work if everything has to be done manually...

[Johan Commelin]

One thing I noticed with my experiment is that rw [finset.sum_lemma] doesn't play very well with abbreviation fintype.sum f := finset.sum univ f

[Sebastien Gouezel]

Just using search and replace in all files in vscode, replacing ∑ with ∑', should do it, hopefully.

[Johan Commelin]

But I wouldn't like restating a whole bunch of lemmas to fintype.sum. At the same time, I think ∑ x in univ, f x is ugly.

[Johan Commelin]

Sebastien Gouezel said:

Just using search and replace in all files in vscode, replacing ∑ with ∑', should do it, hopefully.

No, I meant the other refactor.

[Johan Commelin]

Replacing all finset.sum s f with ∑ x in s, f x

[Sebastien Gouezel]

You don't even need to introduce the abbreviation, just the notation ∑ should be enough.

[Sebastien Gouezel]

Ah, yes, the other refactor. Time for regexps, yes.

[Johan Commelin]

Or do we just introduce the notation, but not use it in the file...

[Johan Commelin]

#2571

[Johan Commelin]

If I change the notation to

localized "notation `∑` binders ` in ` s `, ` r:(scoped f, finset.sum s f) := r" in big_operators
localized "notation `∏` binders ` in ` s `, ` r:(scoped f, finset.prod s f) := r" in big_operators

localized "notation `∑` binders `, ` r:(scoped f, finset.univ.sum f) := r" in big_operators
localized "notation `∏` binders `, ` r:(scoped f, finset.univ.prod f) := r" in big_operators

then the second set of notation is not used in the tactic state. That's unfortunate. Is there some incantation that can move Lean to do a better job?

[Johan Commelin]

I've never really understood how priorities work for notation. Can that be used here?

[Johan Commelin]

Now that the tsum notation has been changed to ∑', I'm ready to start building a PR that introduces the notation above. Except that this notation doesn't really work yet. So what should I do? Introduce fintype.sum and fintype.prod?

[Anne Baanen]

From looking at the source code, the reverse lookups for notation head_map<notation_entry> notation_state::m_inv_map are stored without priority, since head_map<V> derives from head_map_prio<V, constant_priority_fn<V>>

[Anne Baanen]

In fact, according to the debugger the only notation returned for finset.sum is Σ _ in _, _

[Johan Commelin]

Hmm, but the other does seem to work :confused:

[Anne Baanen]

Aha: Σ := finset.univ.sum gets added as notation for the symbol (const lean::head_index &) @0x7ffff49083b8: {m_kind = lean::expr_kind::Macro, m_name = }, and Σ := finset.sum for (const lean::head_index &) @0x7fffdfffd3b8: {m_kind = lean::expr_kind::Constant, m_name = 'finset'.'sum'} (and the second thing is what we probably want)

[Johan Commelin]

Hmm... I have a hard time parsing this

[Gabriel Ebner]

I think Anne tells you to avoid the dot notation.

[Johan Commelin]

Aha.. you mean in the definition of the notation?

[Gabriel Ebner]

:+1:

[Johan Commelin]

Let me try that.

[Anne Baanen]

I think you want to change finset.univ.sum to finset.sum finset.univ and put the line defining finset.sum finset.univ first

[Johan Commelin]

Awesome

localized "notation `∑` binders `, ` r:(scoped f, finset.sum finset.univ f) := r" in big_operators
localized "notation `∏` binders `, ` r:(scoped f, finset.prod finset.univ f) := r" in big_operators

localized "notation `∑` binders ` in ` s `, ` r:(scoped f, finset.sum s f) := r" in big_operators
localized "notation `∏` binders ` in ` s `, ` r:(scoped f, finset.prod s f) := r" in big_operators

works. And the order is important.

[Johan Commelin]

This is great! I just fixed this in the chev-warn branch. Now I have some work to do to explain all of this to mathlib (-;

[Anne Baanen]

The explanation, as far as I understand it: when deciding how to pretty-print an expression, Lean looks up the notations associated to the head of the expression (e.g. finset.sum). It tries them one by one, until it finds a notation that matches the expression, then uses that to pretty-print. The order in which they are tried is the order in which they are stored in the environment structure, which in this case is the order in which they are defined. Apparently the priority information is thrown away (typically it would be highest-priority first, then by order of definition). This is why the order matters.

A notation definition is associated to the head of the expression it expands to, so notation ∑ binders , r:(scoped f, finset.sum finset.univ f) := r is associated to the head of the expansion of r, which is the head of finset.sum finset.univ f, which is finset.sum. But finset.univ.sum doesn't get expanded to finset.sum finset.univ at that point (maybe because it won't know if there is also a namespace finset.univ floating around somewhere?), so you have to write finset.sum finset.univ instead of finset.univ.sum.

[Johan Commelin]

Thanks a lot for explaining this!

[Patrick Massot]

Homework for Johan: write that long overdue docs/extras/notations.md

[Mario Carneiro]

notations don't go through name resolution until they are used, I think

[Johan Commelin]

/me has lots of homework

[Johan Commelin]

But we could start by just dumping Anne's explanation in that file. At least that would be a canonical place to find it again.

[Johan Commelin]

And then we can slowly improve that file.

[Patrick Massot]

Your sum notations also make great examples.

[Johan Commelin]

#2581

[Johan Commelin]

This is not ready for merging. And I welcome everyone to contribute.

[Anne Baanen]

I think there is some lookup of names going on at the point of definition though, if you define a notation before a name:

noncomputable theory

structure foo : Type

notation `☹` := foo.munge

def foo.munge : ℕ := nat.zero

notation `☺` := foo.munge

def bar1 := ☹ -- unknown identifier `foo.munge`
def bar2 := ☺

[Reid Barton]

Anne Baanen said:

The explanation, as far as I understand it: when deciding how to pretty-print an expression, Lean looks up the notations associated to the head of the expression (e.g. finset.sum). It tries them one by one, until it finds a notation that matches the expression, then uses that to pretty-print. The order in which they are tried is the order in which they are stored in the environment structure, which in this case is the order in which they are defined. Apparently the priority information is thrown away (typically it would be highest-priority first, then by order of definition). This is why the order matters.

This is very helpful, thanks. It explains why what I suggested at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Show.20the.20objects.20for.20an.20equality.20of.20morphisms/near/194957595 did not work.

[Reid Barton]

I guess I was mixing up the method for resolving an overloaded notation (two different meanings for a # b) with the method for choosing a notation for the pretty-printer to display (two different notations for nat.add a b).

[Johan Commelin]

We still need tikzcd integration into the Lean tactic state

[Reid Barton]

How hard do you think it would be to use priority or at least prefer local notation over global notation in the pretty printer?

[Anne Baanen]

I think it shouldn't be too hard, since we already have a priority and a priority map

[Anne Baanen]

Looks like the code was written before priorities were available, so it seems like not a deliberate decision to leave out priorities here

[Anne Baanen]

Small complication: looks like priority for notation_entry is always set to a #defined value of 1000

[Anne Baanen]

It turns out that @[priority] and set_option default_priority don't interact with notation, but notation [priority 1] works as expected. PR made: https://github.com/leanprover-community/lean/pull/207

[Johan Commelin]

Cool. Thanks!

[Johan Commelin]

@Anne Baanen Does this also fix the problem that I currently need to write

(∏ x in s, f x) = ...

because otherwise it gets parsed as

∏ x in s, (f x = ...)

[Reid Barton]

This use of in in notation hurts my brain. I noticed it in some filter stuff too.

[Reid Barton]

I always expect in to be a keyword...

[Johan Commelin]

Maybe I can use \mem. Let me try.

[Johan Commelin]

Nope... that doesn't work.

[Johan Commelin]

I guess binders has special support for \in and doesn't want you to mess around with it.

[Johan Commelin]

@Reid Barton Do you have another suggestion?

[Reid Barton]

I don't think binders has special support for \in per se

[Reid Barton]

Maybe I can just get used to in.

[Anne Baanen]

The change shouldn't affect the parser, (un)fortunately.

[Reid Barton]

Oh maybe it wasn't filters actually. There is in in the snippet from the perfectoid space project in Kevin's paper and I can't parse it.

[Patrick Massot]

They are also in filters

[Patrick Massot]

In the eventually and frequently notations

[Reid Barton]

BTW I think I saw let ... in is no longer the syntax in Lean 4 anyways

[Reid Barton]

I wonder why in lean-homotopy-theory I get nice ∘ notation for my morphism composition...

[Reid Barton]

I have local notation f ` ∘ `:80 g:80 := g ≫ f, and that is enough to make it work fine

[Johan Commelin]

#2582 introduces the notation and uses it everywhere in algebra/big_operators.

[Johan Commelin]

I haven't gone through all of mathlib. But I hope we can transition organically.

[Johan Commelin]

But let's first see whether CI likes this

[Johan Commelin]

We need to decide what the precendence of big ops should be. I've found some discussion over here: https://math.stackexchange.com/q/185538/30839
Also see https://github.com/leanprover-community/mathlib/pull/2582#discussion_r418569631 for the discussion that has been going on at github.
Does anyone have strong opinions on how formulas should be parsed?

[Johan Commelin]

@Gabriel Ebner suggests: I think we need to use 64 and 69 instead, then the following works as expected:

∑ x, x + x  =  ∑ x, (x + x)
∑ x, x - x  =  ∑ x, (x - x)
∏ x, x * x  =  ∏ x, (x * x)
∏ x, x + x  =  (∏ x, x) + x

What do others think? Personally I dislike the last example.

[Kevin Buzzard]

I think the question is not "how would a mathematician interpret these" (for which the answer is known to be "different mathematicians will interpret them in different ways") but "what is the convention we should use in order to minimise the number of brackets in mathlib", so that those who want to golf can golf.

[Johan Commelin]

The math.sx page linked to above gives the following example

$\sum_{k\in K}\left(a_k+b_k\right) = \sum_{k\in K}a_k+\sum_{k\in K}b_k \longleftrightarrow \prod_{k\in K}a_kb_k = \left(\prod_{k\in K}a_k\right)\left(\prod_{k\in K}b_k\right).$

which is quoted from Knuth's Concrete mathematics.

[Johan Commelin]

That examples shows a lot of "assymetry".

[Kevin Buzzard]

The Lean conventions for \forall being super-greedy don't correspond with the way I use it in my undergraduate lectures, but I am happy to put extra brackets in. I don't even know which binds more out of \or and \and, I am just happy to put the brackets in to make my intentions clear. In short I'm arguing that this is not a question about the "correct" mathematical convention, it's about which convention will minimise the total number of brackets in mathlib.

[Gabriel Ebner]

It reminds me very much of the question whether ∀ x, p x → q should be (∀ x, p x) → q or ∀ x, (p x → q). I agree with Kevin, there are probably many right answers to this question.

[Johan Commelin]

Ok, I've reverted to 64/69

[Reid Barton]

The example you showed seems to suggest they should both be 69.

[Reid Barton]

More importantly, do they bind tighter than =?

[Johan Commelin]

Reid Barton said:

More importantly, do they bind tighter than =?

Yup. That's fixed (-;
Initially they didn't, which was really annoying.

[Reid Barton]

All example usages I can find suggest that both ∑ and ∏ bind more loosely than * but tighter than +, although I didn't find many relevant examples of products.

[Johan Commelin]

Well... we can still change it (-;
I'm fine with giving both 67 or 68.

[Johan Commelin]

What do people think of making both operators have level 67? If you like that idea, vote on this message with :thumbs_up:
If you want to keep it the way it is (which means 64/69), vote with :stop:

[Kevin Buzzard]

Can you try both, count the total number of necessary brackets in mathlib for each choice, and report back?

[Kevin Buzzard]

Hint: write a bracket linter first

[Johan Commelin]

Kevin Buzzard said:

Can you try both, count the total number of necessary brackets in mathlib for each choice, and report back?

Lol... I would rather not do that. It's already time consuming enough (-;

[Kevin Buzzard]

You posted what 64,69 did -- what does 67,67 do?

[Johan Commelin]

It should accomplish something like

$\sum_{k\in K}\left(a_k+b_k\right) = \sum_{k\in K}a_k+\sum_{k\in K}b_k \longleftrightarrow \prod_{k\in K}a_kb_k = \left(\prod_{k\in K}a_k\right)\left(\prod_{k\in K}b_k\right).$

which is quoted from Knuth's Concrete mathematics.

[Kevin Buzzard]

Well the mathematician in me votes for this one, but the computer scientist is abstaining

[Reid Barton]

I voted for 67,67 but I don't actually know what the numbers mean.

[Reid Barton]

Oh, now I see the end of the stackexchange post you linked to says the same thing I said, I think.

[Johan Commelin]

+ : 65, * : 70. And you wanted something in between... Unfortunately, rat is not defined in core, so we can't go for the actual (65 + 70)/2 : rat as precedence. Hence I suggested the nat version of that fraction :oops:

[Reid Barton]

and -, / are the same as +, * respectively?

[Johan Commelin]

As far as I know, yes

[Reid Barton]

I think they have to be actually.

[Yury G. Kudryashov]

reserve infixl ` + `:65
reserve infixl ` - `:65
reserve infixl ` * `:70
reserve infixl ` / `:70
reserve infixl ` % `:70
reserve prefix `-`:100
reserve infixr ` ^ `:80

[Yury G. Kudryashov]

Sorry for offtopic: what is the precedence of notation f^[n] := iterate f n? It eats = on the left.

[Johan Commelin]

@Yury G. Kudryashov It probably defaults to 0. Seems like we need to change core to fix that...

[Johan Commelin]

I have now changed to 67/67 and added a bit of explanation about it (plus an example of how to parenthesise...)

[Johan Commelin]

And... the linter is happy.