Finsum with fintype

Stream: general

[Peter Nelson]

It's great to see finsum in mathlib. I asked this briefly before in the thread that led to the PR, but thought I would ask again now the dust has settled. It seems from discussion in https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.236355.20finsum that many would like finset.sum + finset to eventually take a back seat in mathlib to finsum + set. I'm certainly on board with this!

If this is the case, then what is the intended pattern for working with a finsum and set in a fintype? It is not fun to have to explicitly pull finiteness parameters out of the fintype instance whenever an API lemma is invoked, like in the following example:

import algebra.big_operators.finprod
open_locale big_operators

theorem finsum_mem_bUnion_of_fintype {α ι M : Type*} [fintype α] [fintype ι] [add_comm_monoid M]
{f : α → M} {I : set ι} {t : ι → set α} (h : I.pairwise_on (disjoint on t)) :
  ∑ᶠ (a : α) (H : a ∈ ⋃ (x : ι) (H : x ∈ I), t x), f a
= ∑ᶠ (i : ι) (H : i ∈ I) (j : α) (H : j ∈ t i), f j :=
  finsum_mem_bUnion (set.finite.of_fintype _) (λ _ _, set.finite.of_fintype _) h

An alternative is to use rw finsum_mem_eq_to_finset_sum to change the summations to finset.sum, and then use existing finset.sum and to_finset api lemmas to do the manipulations. In the case of the above theorem, this is even uglier, to the extent that I have left the following as a sorry.

open_locale classical

theorem finsum_mem_bUnion_of_fintype' {α ι M : Type*} [fintype α] [fintype ι] [add_comm_monoid M]
{f : α → M} {I : set ι} {t : ι → set α} (h : I.pairwise_on (disjoint on t)) :
  ∑ᶠ (a : α) (H : a ∈ ⋃ (x : ι) (H : x ∈ I), t x), f a
= ∑ᶠ (i : ι) (H : i ∈ I) (j : α) (H : j ∈ t i), f j :=
begin
  repeat {rw finsum_mem_eq_to_finset_sum},
  /-
⊢  ∑ (i : α) in (⋃ (x : ι) (H : x ∈ I), t x).to_finset, f i
=   ∑ (i : ι) in I.to_finset, ∑ᶠ (j : α) (H : j ∈ t i), f j
-/
  sorry,
  -- to_finset, finset.sum API stuff.
end

One could argue that the first solution is not so bad, but it gets pretty tiring when calculations get more complicated.

The only other option I can think of is to have fintype.finsum_eq_blahblahblah versions of all the finsum api lemmas, probably all going in a data.fintype.finsum file. Would this be a good idea, despite the duplication? If not, is there another way of doing things that I'm missing? (Let's take it for granted that finset isn't the answer I want...)

[Johan Commelin]

If we want finsum to become the main API, then we'll need to do a massive refactor. But it can probably be done gradually.
If it's done gradually, I think it is very important that there is a very good API to move back and forth between finset.sum and finsum. If that is almost effortless, then we can have the two coexist for a while.

[Eric Wieser]

docs#finsum_mem_bUnion as a link for the lazy to the lemma in the example

[Eric Wieser]

It's not immediately clear to me that those assumptions are necessary - if those arguments were not finite, wouldn't both sides still be equal?

[Mario Carneiro]

@Eric Wieser Suppose I = bool and t i = if i then nat else unit and f j = 1. Then

• ∑ᶠ (i : I) (j : t i), f j = ∑ᶠ (j : nat), 1 + ∑ᶠ (j : unit), 1 = 0 + 1 = 1, but
• ∑ᶠ (a : ⋃ (x : I), t x), f a = ∑ᶠ (a : nat + unit), 1 = 0

[Eric Wieser]

Thanks, I see the general principle now - infinite sums can be decomposed into a finite and infinite part, and when that happens the lemmas don't hold

[Bhavik Mehta]

Johan Commelin said:

If we want finsum to become the main API, then we'll need to do a massive refactor. But it can probably be done gradually.
If it's done gradually, I think it is very important that there is a very good API to move back and forth between finset.sum and finsum. If that is almost effortless, then we can have the two coexist for a while.

I agree it's important there's a good API to move between the two - but as Yury says in the linked thread, I don't believe we should eliminate finset.sum in favour of finsum: both approaches have their use cases.

[Peter Nelson]

I agree that an API is important - however, I don't think it is the right way to manipulate finsum expressions in a fintype. Doing a calculation about finsum would involve first translating to finset.sum, then (in many cases) unpacking/repacking the resulting to_finset expression. From what I've experienced, using set.to_finset back and forth too liberally is what introduces instance mismatch issues. Maybe I'm not so great at this, but I think trying to fill in the sorry in the second example in my previous post will give some indication of how fiddly this is.

So I'll re-ask my question - would it be justified to have specialized fintype versions of all the finsum/finprod API lemmas? As far as I can tell, using finsum when working with sets in a fintype is going to be quite annoying without such lemmas.

[Eric Wieser]

Perhaps the compromise is to just put all the finite assumptions last in the argument lists?

[Eric Wieser]

That way, you can rewrite by finsum_mem_bUnion h, and clean up at the end with simp [set.finite.of_fintype]

[Yury G. Kudryashov]

We can also have a tactic that tries set.finite.of_fintype and some other heuristics (may be, as simp [set.finite.of_fintype]) and use h : finite (mul_support f) . finite_tac.