membership in finset.sum

Stream: maths

[Filippo A. E. Nuccio]

I do not know how to say that a dummy variable in the finset I am summing over belongs to the finset. A MWE is the following:

import data.finset

open_locale big_operators

lemma foo (x : ℤ) (A : finset ℤ) (P : ℤ → Prop) : x ∈ A → P x := sorry
def bar (x : ℤ) (P : ℤ → Prop) (h : P x) : ℕ := sorry


def bleah (A : finset ℤ) (P : ℤ → Prop) : ℕ :=
begin
  refine ∑ a in A, bar a P (foo a A P _),
  sorry,---lean asks for ⊢ a ∈ A
end

What I am doing is definining a natural number in bar under the assumption that P a holds; and foo provides a proof of P a assuming that a ∈ A. When I perform the sum in bleah, I cannot extract the information that a ∈ A from the fact that a in A.

[Floris van Doorn]

You cannot do this when using ∑ a in A, ....
One thing you can do is to sum over A.subtype P (or even A.subtype (∈ A)?). See docs#finset.subtype.
Another thing you can try (which is probably more convenient) is to redefine bar to produce some garbage value if P does not hold, e.g.

def bar (x : ℤ) (P : ℤ → Prop) : ℕ := if h : P x then sorry else 0

[Filippo A. E. Nuccio]

Ok, thanks! I will try to understand how to use A.subtype P(I am not sure the "garbage" strategy would really work in the case I am working on).

[Johan Commelin]

Yet another option is to use finsum where you can write ∑ᶠ a ∈ A, f a

[Johan Commelin]

But you will then need to work a bit to relate it to finset.sum

[Filippo A. E. Nuccio]

I'll try the first option suggested by Floris and if I can't make it work, I will come back here. Thanks :pray:

[Floris van Doorn]

Very similar to what I suggested: you can also use ∑ a : (A : set ℤ), ... (see e.g. src#finset.prod_finset_coe)

[Filippo A. E. Nuccio]

Yes!

def bleah (A : finset ℤ) (P : ℤ → Prop) [decidable_pred P] : ℕ :=
begin
  refine ∑ a : (A : set ℤ), bar a P (foo a A P (finset.coe_mem _)),
end

[Filippo A. E. Nuccio]

Thanks (with the first option it was somewhat more cumbersome).

[Filippo A. E. Nuccio]

And it also works perfectly in my "true" case.

[Yaël Dillies]

The correct thing to do here might be using docs#finset.attach

[Eric Wieser]

But that's just finset.univ!