Finset sum notation

Stream: mathlib4

[Kenny Lau]

This might be a less used feature (at least to me), but the summtation (and also product) notations actually support more kinds of syntax:

import Mathlib

variable {s : Finset ℕ}

#check ∑ i ∈ s with i + 3 = 5, i * i
-- ∑ i ∈ s with i + 3 = 5, i * i : ℕ

set_option pp.notation false in
#check ∑ i ∈ s with i + 3 = 5, i * i
-- (Finset.filter (fun i => Eq (HAdd.hAdd i 3) 5) s).sum fun i => HMul.hMul i i : Nat

#check ∑ i ∈ s with h : i + 3 = 5, i * i
-- ∑ i ∈ s, if h : i + 3 = 5 then i * i else 0 : ℕ

Are these behaviours good enough? I personally have the following concerns:

1. with and with h : produce very different results syntactically, the former uses Finset.filter and the latter is dite.
2. The with h : fails the pretty-printer round-trip (but on the other hand if we just print every sum-dite epxression using with h : then it might also produce some false-positives

[Kenny Lau]

cc @Damiano Testa

[Ruben Van de Velde]

I think this is @Yaël Dillies's baby

[Kenny Lau]

aha, the with h : is #11563 which was merged last month

[Kenny Lau]

delab for with is #22048

[Bhavik Mehta]

Yeah, the first issue is something I mentioned a few times in #11563, I'd very much like to see that changed.

[Bhavik Mehta]

Perhaps that's easy enough to just change though?

[Bhavik Mehta]

There's also a bug with the delaborator for with, it doesn't give the correct spacing, I think this is still an issue?

[Kenny Lau]

Bhavik Mehta said:

There's also a bug with the delaborator for with, it doesn't give the correct spacing, I think this is still an issue?

I just fixed this in #30194 (merged)

[Bhavik Mehta]

Just spotted that too, thanks!!

[Kenny Lau]

Bhavik Mehta said:

the first issue

but then one question is also whether that's actually fine, since filter seems preferrable, and then h : is impossible without dite

[Bhavik Mehta]

Oh no, I think we should use ite in the first case. As well as being consistent, I think this is actually the more convenient thing to expand to. For instance, when commuting sums, it's usually easier to push everything into an ite and into the inner-most point in a sum

[Kenny Lau]

well one issue with ite is the "else 0" that it produces, maybe

[Bhavik Mehta]

I don't think that's an issue. In fact I think that's a good thing :)

[Kenny Lau]

well if you add two of them you might get 0 + 0

[Bhavik Mehta]

Sure, that just means we need to change a lemma's proof slightly, that's not really an issue. Essentially my proposed change is to make docs#Finset.sum_filter use notation on the rhs not lhs. And as I say, I think this is more convenient in practice as a choice.

[Yaël Dillies]

The big issue with Bhavik's idea, ie the reason it is taking so long to implement, is that it makes docs#Finset.sum_ite useless as a simp lemma (even locally)

[Yaël Dillies]

I still don't know how to solve the problem of splitting up a sum according to a property. Would a simproc checking whether the right side of the ite is zero not loop still?

[Yaël Dillies]

The matter is further complicated by the fact that docs#ite_not is a simp lemma, and one can also note that the new with h : notation is unsuited for use in docs#Finset.expect

[Yury G. Kudryashov]

Why not use a sum over (s.filter p).attach?

[Yury G. Kudryashov]

(I didn't think a lot about this, so probably it's a bad idea for an obvious reason)

[Yaël Dillies]

This is precisely what I had originally in #11563 before Bhavik got his way with the if h : ... then ... else ... spelling

[Yaël Dillies]

The main issue with the attach spelling is that it is quite weird to obtain the h from it

[Bhavik Mehta]

The attach versions are almost always far more annoying than useful, in part because obtaining h is awkward, but also because it leads very easily to DTT hell, particularly when modifying s or p as part of a rewrite sequence (which is a very common operation to do). I think we should have the lemmas saying that the ite sum is equal to the attach sum, but I think it's fairly clear that the ite version is by far the most useful in practice.

[Bhavik Mehta]

Yaël Dillies said:

The big issue with Bhavik's idea, ie the reason it is taking so long to implement, is that it makes docs#Finset.sum_ite useless as a simp lemma (even locally)

This isn't a simp lemma already, and throughout mathlib it's only used in simp twice, so I don't think this is a big issue.

[Bhavik Mehta]

Yaël Dillies said:

I still don't know how to solve the problem of splitting up a sum according to a property. Would a simproc checking whether the right side of the ite is zero not loop still?

What exactly is "the problem" here? The choice of notation has no impact here, we can rewrite in exactly the same way before or after these changes.

[Kenny Lau]

the problem is "loop"ing i think

[Kenny Lau]

if you have the wrong lemma to split a sum

[Bhavik Mehta]

That's already an issue! Again, the lemma statements aren't changing, we're just having more convenient and consistent notation for it

[Kenny Lau]

well we're debating here about the correct simp-NF forms, and that has an impact on what the statements look like

[Bhavik Mehta]

Why do you think the simp-NF forms are changing?

[Kenny Lau]

actually I would like to retract some of my statements, I don't think "splitting a sum on cases" should be a simp lemma, mainly because there's no way to infer the condition

[Kenny Lau]

so I assume we're talking about a statement of the form:

• sum of f(x) = sum of f(x) for P(x) + sum of f(x) for not P(x)

[Kenny Lau]

if our chosen representation for "sum of f(x) for P(x)" changes, then the statement also changes

[Kenny Lau]

by representation I mean something like:

• sum over filter
• sum over attached
• sum ite

[Yaël Dillies]

Kenny Lau said:

so I assume we're talking about a statement of the form:

• sum of f(x) = sum of f(x) for P(x) + sum of f(x) for not P(x)

No, that's not what I am talking about. I am instead thinking of the statement ∑ i ∈ s, if p i then f i else g i = ∑ i ∈ s with p i, f i + ∑ i ∈ s with ¬ p i, g i

[Kenny Lau]

aha

[Kenny Lau]

yeah that also applies, we also need to stop it from looping

[Yaël Dillies]

There are two things going on here:

• Under Bhavik's proposal, this lemma would loop.
• Under Bhavik's proposal, the simp normal form of ∑ i ∈ s with ¬ p i, g i is ∑ i ∈ s, if p i then 0 else g i, ie simp would remove notation

[Bhavik Mehta]

I think this just shouldn't be a simp-lemma! It's already barely used as such: it's not tagged simp currently, and it's used locally as a simp lemma only twice in mathlib.

[Yaël Dillies]

I never said that! It's clearly a sort of distributivity lemma. But equally I don't think it should be banned from being used in simp

[Bhavik Mehta]

Perhaps, but I think the concern of "this particular lemma makes notation go away if I put it in simp" is quite a bit smaller than the consistency and convenience of the notation here.

[Kenny Lau]

well, we can just have without...

[Yaël Dillies]

That's actually not such a bad idea!