finite sums

Stream: maths

[Kevin Buzzard]

The 1st years at Imperial are doing infinite sums in their analysis class. To do infinite sums, one has to be able to have a robust API for finite sums. Here are three possibilities:

import data.list.basic data.fintype

open nat

variables (R : Type*) [add_comm_monoid R]

definition my_sum_to_n (summand : ℕ → R) : ℕ → R
| 0 := 0
| (succ n) := my_sum_to_n n + summand n

definition my_sum_to_n' (summand : ℕ → R) : ℕ → R :=
λ n, ((list.range n).map summand).sum

definition my_sum_to_n'' (summand : ℕ → R) : ℕ → R :=
λ n, (finset.range n).sum summand

You can see them in action here:

https://github.com/kckennylau/Lean/blob/master/proofs_by_induction.lean

What is the "idiomatic" way to do this? @Chris Hughes have you worked with this stuff a lot? Note that first two (but not the third) work with add_monoid but I am only interested in R being the real or complex numbers right now.

[Chris Hughes]

I use (range n).sum but I don't like it. I think a better interface needs to be made. (range n).sum definitely gives you the best range of lemmas though.

[Kevin Buzzard]

Ooh, I also want to sum from a to b, not just from 0 to n-1. Did we have all this conversation once before, ages ago?

[Kevin Buzzard]

finset or list?

[Kevin Buzzard]

Are statements such as sum_to_n f N = sum_to_n (\lam x, f(N-1-x)) N in the library?

[Chris Hughes]

I don't think so. Scott's made a start on this though

[Kevin Buzzard]

Does "a better interface" mean "make a completely new file somewhere in mathlib called something like finite_sum.lean and define a new function sum_range f a b or something, and prove basic things about it?

[Kevin Buzzard]

Oh I remember Mario's suggestion that sum_range f a b should sum f(x) from x=a to x=a+b-1

[Kevin Buzzard]

But is this not yet implemented?

[Chris Hughes]

No. It means use finset.sum, but have a bunch of lemmas specific to sums over intervals as well, and maybe some nice notation.

[Kevin Buzzard]

Do we have the function sending a,b to the finset {a,a+1,...,a+b-1}?

[Chris Hughes]

I think so, it's got Ico in its name I think.

[Kevin Buzzard]

Many thanks. It's got nothing but Ico in its name, apparently.

[Kevin Buzzard]

Interval-closed-open

[Kevin Buzzard]

and there's list.Ico, multiset.Ico and finset.Ico

[Kevin Buzzard]

Apparently we opted for Ico n m = {n, n+1, ... , m-1}

[Kevin Buzzard]

Lines 1654 onwards in finset.lean contain a bunch of stuff. But where are the recursors?

[Kevin Buzzard]

How do I prove that | sum_{i=a}^b f(i) | <= sum_{i=a}^b |f(i)| ??

[Kevin Buzzard]

(triangle inequality for finite sums)

[Kevin Buzzard]

Oh -- this is a general finset thing, not a sum from a to b thing.

[Kevin Buzzard]

So I need to find the right recursor for finsets...

[Kevin Buzzard]

Why is finset.induction tagged @[recursor 6]?

[Chris Hughes]

I think it must already be there

[Kevin Buzzard]

I think all of M1P1 must already be there :-)

[Kevin Buzzard]

If I was summing from 0 to n-1 I could do induction on n and use the fact that finset (n +1) = finset n union {n}. But for a general finset I'm going to have to choose a random element. Maybe that's just life.

[Kevin Buzzard]

Oh I see, I just use finset.induction I think.

[Kenny Lau]

is finset a traversable monad?

[Kevin Buzzard]

I don't know what any of that means, but can you explain to me why I might care?

[Kevin Buzzard]

[I'm open to the idea that I might care]

[Patrick Massot]

We already had this discussion many times. All those problems have been solved in Coq, and I made a tiny start at porting the solution at https://github.com/PatrickMassot/bigop. But nobody is willing to help because people on this chat think they know better than people who have thought about this for 30 years and formalized the 4 color theorem and Feit-Thompson.

[Kenny Lau]

type mismatch at field 'bind'
  finset.bind
has type
  Π {α β : Type u} [_inst_1 : decidable_eq β], finset α → (α → finset β) → finset β
but is expected to have type
  Π {α β : Type u}, finset α → (α → finset β) → finset β

[Kenny Lau]

that's the answer to my question

[Kenny Lau]

I should build a "real" finset

[Kevin Buzzard]

We already had this discussion many times.

Aah yes that's right -- I somehow fail to unify these finite set questions with the big operators work, and I even have a copy the Coq paper lying around on my desk somewhere.

[Kenny Lau]

import data.list.basic

universes u v

def finset.setoid (α : Type u) : setoid (list α) :=
{ r := λ L₁ L₂, ∀ x, x ∈ L₁ ↔ x ∈ L₂,
  iseqv := ⟨λ L x, iff.rfl, λ L₁ L₂ H12 x, (H12 x).symm, λ L₁ L₂ L₃ H12 H23 x, (H12 x).trans (H23 x)⟩ }

local attribute [instance] finset.setoid

def finset (α : Type u) : Type u :=
quotient (finset.setoid α)

namespace finset

variables {α : Type u}

instance : has_mem α (finset α) :=
⟨λ x s, ∀ L : list α, ⟦L⟧ = s → x ∈ L⟩

@[simp] lemma mem_mk {x : α} {L : list α} : @has_mem.mem α (finset α) _ x ⟦L⟧ ↔ x ∈ L :=
⟨λ H, H L rfl, λ H L₂ H2, (quotient.exact H2 x).2 H⟩

@[extensionality] protected lemma ext {s t : finset α} (H : ∀ x, x ∈ s ↔ x ∈ t) : s = t :=
quotient.induction_on₂ s t (λ L₁ L₂ H, quotient.sound $ λ x, by rw [← mem_mk, H x, mem_mk]) H

lemma ext_iff {s t : finset α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
⟨λ H x, H ▸ iff.rfl, finset.ext⟩

def empty : finset α := ⟦[]⟧

@[simp] lemma not_mem_empty (x : α) : x ∉ (empty : finset α) :=
λ h, mem_mk.1 h

def singleton (x : α) : finset α := ⟦[x]⟧

def union (s t : finset α) : finset α :=
quotient.lift_on₂ s t (λ L₁ L₂, ⟦L₁ ++ L₂⟧) $ λ L₁ L₂ L₃ L₄ H13 H24,
quotient.sound $ λ x, by rw [list.mem_append, list.mem_append, H13 x, H24 x]

@[simp] lemma mem_union {s t : finset α} (x : α) : x ∈ union s t ↔ x ∈ s ∨ x ∈ t :=
quotient.induction_on₂ s t $ λ L₁ L₂, by change x ∈ ⟦_⟧ ↔ _; simp only [mem_mk, list.mem_append]

variables {β : Type v}

def prebind (f : α → finset β) (L : list α) : finset β :=
L.foldr (λ x, union (f x)) empty

@[simp] lemma prebind_cons (f : α → finset β) (hd : α) (tl : list α) :
  prebind f (hd :: tl) = union (f hd) (prebind f tl) := rfl

@[simp] lemma mem_prebind {L : list α} {f : α → finset β} {y : β} :
  y ∈ prebind f L ↔ ∃ x ∈ L, y ∈ f x :=
list.rec_on L (iff_of_false (not_mem_empty y) $ λ ⟨x, H, _⟩, H) $ λ hd tl ih,
by rw [prebind_cons, mem_union, ih];
simp only [exists_prop, list.mem_cons_iff, or_and_distrib_right, exists_or_distrib, exists_eq_left]

instance : monad finset.{u} :=
{ pure := λ α x, quotient.mk [x],
  bind := λ α β s f, quotient.lift_on s (prebind f) $ λ L₁ L₂ h,
    by ext x; simp only [mem_prebind, exists_prop, h _] }

end finset

[Kenny Lau]

done, the real finset is a monad

[Johan Commelin]

@Patrick Massot I agree that it is frustrating that we are having this discussion multiple times, and that we are reinventing the wheel. I haven't thought about this problem (finite sums) myself. I wouldn't mind if this could be turned into a student project; but I fear that there is not enough mathematical meat in it. At the moment I don't have much contact with the CS department here in Freiburg. It's something on my todo list. Maybe they would think that an bachelor thesis titled "Algorithms and data types for manipulating finite sums and proving identities between them" is interesting...

[Johan Commelin]

I would like to get better at recruiting people for library development.

[Kenny Lau]

import data.list.basic

universes u v

def finset.setoid (α : Type u) : setoid (list α) :=
{ r := λ L₁ L₂, ∀ x, x ∈ L₁ ↔ x ∈ L₂,
  iseqv := ⟨λ L x, iff.rfl, λ L₁ L₂ H12 x, (H12 x).symm, λ L₁ L₂ L₃ H12 H23 x, (H12 x).trans (H23 x)⟩ }

local attribute [instance] finset.setoid

def finset (α : Type u) : Type u :=
quotient (finset.setoid α)

namespace finset

run_cmd mk_simp_attr "finset"

variables {α : Type u}

instance : has_mem α (finset α) :=
⟨λ x s, ∀ L : list α, ⟦L⟧ = s → x ∈ L⟩

@[finset] lemma mem_mk {x : α} {L : list α} : @has_mem.mem α (finset α) _ x ⟦L⟧ ↔ x ∈ L :=
⟨λ H, H L rfl, λ H L₂ H2, (quotient.exact H2 x).2 H⟩

@[extensionality] protected lemma ext {s t : finset α} (H : ∀ x, x ∈ s ↔ x ∈ t) : s = t :=
quotient.induction_on₂ s t (λ L₁ L₂ H, quotient.sound $ λ x, by rw [← mem_mk, H x, mem_mk]) H

lemma ext_iff {s t : finset α} : s = t ↔ ∀ x, x ∈ s ↔ x ∈ t :=
⟨λ H x, H ▸ iff.rfl, finset.ext⟩

def empty : finset α := ⟦[]⟧

@[finset] lemma not_mem_empty (x : α) : x ∉ (empty : finset α) :=
λ h, mem_mk.1 h

def singleton (x : α) : finset α := ⟦[x]⟧

def union (s t : finset α) : finset α :=
quotient.lift_on₂ s t (λ L₁ L₂, ⟦L₁ ++ L₂⟧) $ λ L₁ L₂ L₃ L₄ H13 H24,
quotient.sound $ λ x, by rw [list.mem_append, list.mem_append, H13 x, H24 x]

@[finset] lemma mem_union {s t : finset α} (x : α) : x ∈ union s t ↔ x ∈ s ∨ x ∈ t :=
quotient.induction_on₂ s t $ λ L₁ L₂, by change x ∈ ⟦_⟧ ↔ _; simp only [list.mem_append] with finset

section prebind

variables {β : Type v}

def prebind (f : α → finset β) (L : list α) : finset β :=
L.foldr (λ x, union (f x)) empty

@[finset] lemma prebind_cons (f : α → finset β) (hd : α) (tl : list α) :
  prebind f (hd :: tl) = union (f hd) (prebind f tl) := rfl

@[finset] lemma mem_prebind {L : list α} {f : α → finset β} {y : β} :
  y ∈ prebind f L ↔ ∃ x ∈ L, y ∈ f x :=
list.rec_on L (iff_of_false (not_mem_empty y) $ λ ⟨x, H, _⟩, H) $ λ hd tl ih,
by rw [prebind_cons, mem_union, ih];
simp only [exists_prop, list.mem_cons_iff, or_and_distrib_right, exists_or_distrib, exists_eq_left]

end prebind

variables {β : Type u}

instance : monad finset.{u} :=
{ pure := λ α x, quotient.mk [x],
  bind := λ α β s f, quotient.lift_on s (prebind f) $ λ L₁ L₂ h,
    by ext x; simp only [exists_prop, h _] with finset }

@[finset] lemma mem_pure {x y : α} : x ∈ (pure y : finset α) ↔ x = y :=
mem_mk.trans list.mem_singleton

@[finset] lemma mem_bind {s : finset α} {f : α → finset β} {y : β} :
  y ∈ s >>= f ↔ ∃ x ∈ s, y ∈ f x :=
quotient.induction_on s $ λ L, show y ∈ prebind f L ↔ _,
by simp only [exists_prop] with finset

@[finset] lemma mem_map {f : α → β} {s : finset α} {y : β} :
  y ∈ f <$> s ↔ ∃ x ∈ s, y = f x :=
show y ∈ s >>= pure ∘ f ↔ _,
by simp only [function.comp_apply] with finset

@[finset] lemma mem_seq {f : finset (α → β)} {s : finset α} {y : β} :
  y ∈ f <*> s ↔ ∃ φ ∈ f, ∃ x ∈ s, y = (φ : α → β) x :=
show y ∈ f >>= (<$> s) ↔ _, by simp only with finset

instance : is_lawful_monad finset.{u} :=
{ pure_bind := λ α β x f, finset.ext $ λ y, by simp only [exists_prop, exists_eq_left] with finset,
  bind_assoc := λ α β γ s f g, finset.ext $ λ y, by simp only [exists_prop, exists_and_distrib_left.symm,
      exists_and_distrib_right.symm, and_assoc] with finset; rw exists_swap,
  id_map := λ α s, finset.ext $ λ x, by simp only [id, exists_prop, exists_eq_right'] with finset }

end finset

[Kenny Lau]

it's a lawful monad!

[Kevin Buzzard]

Yeah but who is going to rewrite the 1700-line file finset.lean? What advantage does your approach have over the one in mathlib? Do you understand @Mario Carneiro and @Jeremy Avigad and @Simon Hudon 's approach via qpf's? Is it the same as yours or something else again?

[Kenny Lau]

well I've been told that the current finset in mathlib is faster in terms of computation

[Kenny Lau]

so it'll probably stay

[Scott Morrison]

@Patrick Massot, I disagree with your characterisation

because people on this chat think they know better than people who have thought about this for 30 year

[Scott Morrison]

I wanted a quick an dirty solution for reindexing sums by shifting right and left, and had no where near the time available to properly do a big operators library, so I did just that. There are now usable lemmas specifically for using finset.sum with Ico, and of course this is not meant to be a replacement for a good general solution later.

[Scott Morrison]

Further, and I suspect Mario will agree here, I don't think it's obvious that Coq's bigop library should be ported verbatim. We started a discussion about this earlier, and one example that came up was not understanding why they wanted to carry around both a domain for the sum, and a predicate selecting out some subset of that domain. To my eye that seems unnecessarily painful, and we should just change the domain to a subset when we want to do so. I couldn't find any explanation of this design decision in their paper, and as far as I can remember no one either justified it here, or wanted to talk about comparing the alternatives. As it didn't seem like there was much enthusiasm for discussion, I moved on to other things.

[Mario Carneiro]

@Kevin Buzzard The QPF stuff isn't presenting a new way to do finsets, it's just providing a way to use finset inside other inductive types, which is something we currently can't do

[Mario Carneiro]

The difference between Kenny's finsets and mathlib finsets is that Kenny's is a quotient over the multiplicity of an element, while mathlib's is a restriction on multisets so that they have multiplicity 0 or 1 in each element. Computationally it's worse than mathlib's finsets, but mathlib's finsets are already completely impractical and not how you should store finite sets of things anyway for computational purposes. The ordset type was intended to be more computational, and provides O(log n) operations for most things rather than linear time for everything

[Kenny Lau]

and my finsets don't need decidable_eq to be a monad :P

[Mario Carneiro]

One thing that Kenny's finsets doesn't support that mathlib's finsets do is card

[Mario Carneiro]

but Kenny's finsets support insert and union without decidable_eq, which is nice

[Kenny Lau]

déjà vu

[Mario Carneiro]

inter can't be done without decidable eq though

[Kenny Lau]

what's the best™ way to do finsets?

[Kenny Lau]

I recall ZF having 5 inequivalent definitions of finite?

[Mario Carneiro]

metamath has 8 (http://us2.metamath.org/mpeuni/mmtheorems83.html#mm8285s)

[Kenny Lau]

also why isn't multiset a monad?

[Kenny Lau]

import data.multiset

instance : monad multiset :=
{ pure := λ α x, x :: 0,
  map := @multiset.map,
  bind := @multiset.bind }

[Mario Carneiro]

good question

[Mario Carneiro]

is it lawful? I think it is

[Kenny Lau]

'course it's lawful, it's even commutative!

[Kenny Lau]

it's the free commutative monoid over a type

[Patrick Massot]

Further, and I suspect Mario will agree here, I don't think it's obvious that Coq's bigop library should be ported verbatim.

Of course we cannot port it verbatim. For instance we lack proper support for custom induction principle. We also lack SSReflect's powerful apply tactic. So we need to either first code more powerful tactics (which probably needs Lean 4) or write longer proofs (as I started to do).

We started a discussion about this earlier, and one example that came up was not understanding why they wanted to carry around both a domain for the sum, and a predicate selecting out some subset of that domain. To my eye that seems unnecessarily painful, and we should just change the domain to a subset when we want to do so. I couldn't find any explanation of this design decision in their paper, and as far as I can remember no one either justified it here, or wanted to talk about comparing the alternatives. As it didn't seem like there was much enthusiasm for discussion, I moved on to other things.

I'm not sure I understand what you mean here. Of course we want to be able to sum on various stuff, including using a predicate. Are you denying this happens in maths? There are several examples in the Coq bigop paper. Of course you can put the burden on the user, but this is not my understanding of what is library building. Let's take the simplest example. Say we have a sum indexed by integers, and we want to separate this into two sums: the sum over even integers in the summation range and the sum over odd integers, because you'll then do different manipulation depending on parity of the index. How would you like the interface to look like? Should is look like maths, where you get $\sum_{1 \le i \le n } u_i = \sum_{1 \le i \le n ; i \text{ even}} u_i + \sum_{1 \le i \le n ;i \text{ odd} } u_i$ after writing something like rw [bigop.split_using_predicate is_even, bigop.predicate_iff odd_iff_not_even or do you want to first prove lemmas about lists until it looks like a concatenation of lists etc? I really think the work should go into the library, and then the user enjoys. Note that the user doesn't need to see anything complicated until needed: you can define notation that do not mention the predicate when you don't need it (this is what bigop is doing, and what I've done right from the beginning).

[Mario Carneiro]

If you are doing something with complicated sums like these, I think the best option is to use finsets. They are much more compositional

[Patrick Massot]

finsets are unordered, hence they cannot be used for a general library.

[Mario Carneiro]

huh? That equation you gave doesn't even hold unless you can reorder the elements

[Patrick Massot]

What is the part of "general" that you don't understand?

[Mario Carneiro]

The part where finsets are already pretty general

[Patrick Massot]

bigop is a a general library, it handles all use case in a unified way

[Patrick Massot]

Assuming commutativity is extremely restrictive, it's not "pretty general"

[Mario Carneiro]

I'm saying that if it's not commutative, you have other options but that partition theorem isn't true

[Mario Carneiro]

Can we assume associativity?

[Patrick Massot]

Of course there are lemmas with assumptions, is that what you are trying to teach here?

[Mario Carneiro]

At some point you are just folding over the free magma

[Patrick Massot]

We don't have to assume associativity for all lemmas, although many of them will

[Patrick Massot]

I honestly don't understand how you can promote both semi-rings and big operations indexed by finite sets

[Mario Carneiro]

We have list.sum already

[Mario Carneiro]

I'm not seeing what we are missing

[Mario Carneiro]

We have an extensive collection of lemmas about ordered lists - that's list

[Patrick Massot]

list.sum is tied to addition, right?

[Mario Carneiro]

or list.prod, or list.foldr

[Patrick Massot]

and list.prod is tied to multiplication, so you are still missing a general purpose library

[Patrick Massot]

Of course list.foldr will be used in the implementation, but it doesn't give you the lemmas

[Mario Carneiro]

Sure it does

[Mario Carneiro]

you can prove lemmas about list.foldr

[Mario Carneiro]

under appropriate assumptions about the function

[Patrick Massot]

And then you are finally writing a bigop library!

[Patrick Massot]

assuming you also setup good notations

[Mario Carneiro]

It's hard to make a notation for a function with four explicit parameters

[Patrick Massot]

And, in order to do that you can save time by having a look at what other did.

[Patrick Massot]

That's why you need several notations

[Patrick Massot]

as in https://github.com/PatrickMassot/bigop/blob/master/src/bigop.lean#L28-L69

[Mario Carneiro]

If I am specializing to +, that's already a function

[Mario Carneiro]

Using the same function for all of these doesn't make anything easier

[Patrick Massot]

The trick is that those notations are used by users, but all lemmas are proved once, in the most general setting

[Patrick Massot]

Of course it does make everything easier, that's what math is about: prove general results and gets many special cases for free

[Mario Carneiro]

Yeah but we've already done that

[Patrick Massot]

Where?

[Mario Carneiro]

Finset has loads of theorems, multiset has loads of theorems, list has loads of theorems, all in maximum generality for the statement

[Patrick Massot]

Seriously Mario, did you open that https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/bigop.v or are you waiting for the next time one of your papers will be rejected because you pay no attention to what the rest of the world is doing?

[Johan Commelin]

That is >200 lines of introducing notation. Wow!

[Patrick Massot]

Yes, those guys are pretty serious about building user interfaces

[Johan Commelin]

Patrick, do you know if that file was written by hand?

[Mario Carneiro]

certainly it was

[Johan Commelin]

Parts of it look so regular that you would think one might want to generate it

[Mario Carneiro]

the answer to that question is no 90% of the time

[Patrick Massot]

Remember this is part of the project that proved Feit-Thompson. It's the same game that we play, except that it scales. So, yes, they are pretty rigorous and regular

[Patrick Massot]

I need to go, but I hope you'll think seriously about all that

[Chris Hughes]

I'm with Patrick here. list.prod doesn't have anywhere near the number of lemmas of finset.prod.

[Mario Carneiro]

Are there a lot of analogous theorems? I guess the noncommutative story is much simpler since most of the lemmas don't hold

[Mario Carneiro]

• finset.prod_empty -> list.prod_nil
• finset.prod_insert -> list.prod_cons
• finset.prod_singleton -> TODO, but provable by simp
• finset.prod_const_one -> TODO: list.prod_repeat_one : list.prod (list.repeat 1 n) = 1
• finset.prod_image -> unnecessary
• finset.prod_congr -> unnecessary
• finset.prod_union_inter -> inapplicable
• finset.prod_union -> list.prod_append
• finset.prod_sdiff -> inapplicable
• finset.prod_bind -> list.prod_join, TODO?
• finset.prod_product -> TODO
• finset.prod_sigma -> TODO
• finset.prod_image' -> ?
• finset.prod_mul_distrib -> inapplicable
• finset.prod_comm -> inapplicable
• finset.prod_hom -> TODO
• finset.prod_hom_rel -> TODO
• finset.prod_subset -> not sure how to state
• finset.prod_eq_single -> not sure how to state
• finset.prod_attach -> unnecessary
• finset.prod_bij -> inapplicable

The inapplicable ones only apply in a commutative setting, where I assume the finset notion works better. For some of the others, it may be better to have a version of fold that takes a binary operation and a function, similar to Patrick's apply_bigop but without the predicate

[Scott Morrison]

Of course we want to be able to sum on various stuff, including using a predicate. Are you denying this happens in maths?

Of course not...

I just don't understand why a big operations interface needs to know separately about some domain, and some predicate on it, when you could just use .filter (on whatever sort of object is representing the domain).

[Mario Carneiro]

I would say something similar about the similarities between sum_(i \in l) a_i and sum_(i=m..n) a_i. One is literally a special case of the other, so compositionality suggests to factor the definition

[Patrick Massot]

Again, Scott and Mario: of course the implementation uses filter and factor the definition of sum_(i \in l) a_i and sum_(i=m..n) a_i. But the user interface needs to do its job and hide all that.

[Kevin Buzzard]

I think that what might be happening here is similar to this whole "R is Noetherian and S is isomorphic to R so S is Noetherian" thing.

Patrick -- we have to remember that Mario is not actually a mathematician. We might see sums broken up into sums over even and odd indices quite a lot (or maybe much more complex things, like breaking sums over modules into sums over isomorphism classes or whatever), but maybe he just never really does. He knows that everything can be done with filter and fold and doesn't really see the problem. I run into issues when doing things like undergraduate analysis and think "isn't it annoying that this isn't there and I have to use filter and fold", but nobody actually writes the code which should be there because the mathematicians haven't got around to it and the computer scientists don't really seem to know what we want. It's all well and good saying "we want what's in Coq" but somehow in practice what we actually want is the tools necessary to do what we're trying to do right now this instant. I have become convinced that Mario isn't just being obstructive/lazy when he doesn't write me my tactic which will rewrite sensible mathematical statements along isomorphisms of rings, he just can't really see why it's necessary because I've not yet come up with the killer example. I think it's the same here. We occasionally say "we want to do this" and it is pointed out to us that this is actually possible and would in fact be easy if we had some CS training, but we want something else. Maybe we haven't formalised exactly what we want.

[Mario Carneiro]

In metamath I had to do several sums over unusual sets; for example a sum over group elements breaks into a sum over conjugacy classes or cosets, or into sets of size two. Then there are mobius sums, over the divisors of a number, that commute with regular sums in interesting ways. I handled all of these by essentially the same method, which like finset sum. (It was a sum over a general abelian group, so in some ways it's more general than the lean version because it's not as much of a pain to switch between multiplicative and additive.)

To prove stuff about partitioning a group sum, the proof obligation says that you have an indexed family of finsets which is disjoint (this is a definition on families of sets/finsets that says \all (i j : I) (z : A), z \in f i -> z \in f j -> i = j), then the sum breaks into a two dimensional sum indexed over I and then summing the finsets in f.

[Chris Hughes]

There's a danger in hiding the fact that it's based on finset.sum in the sense that you lose the interface and theorems you had for finset, or at least make it less obvious that they apply. Take $\sum_{j=0}^{n} \sum_{k=0}^j a_k b_{j-k} = \sum_{k=0}^{n} a_k \sum_{j=k}^n b_{j-k}$. This is hard to prove without using without using lemmas about finsets (and is stated without proof in any textbook). There are probably a few lemmas missing about intervals, but you still very much need the finset ones.

[Kevin Buzzard]

I always justify this in lectures by saying that it's the sum over 0 <= k <= j <= n

[Chris Hughes]

Exactly. That's the lean proof. But you have to use lemmas about sums over finsets for that. You don't want the finset to be hidden.