Summing over a `Prop`

Stream: new members

[Snir Broshi]

import Mathlib

theorem foo1 : ∑ n ≤ 5, n = 15 := rfl
theorem foo2 : ∑ (n : Fin 10), ∑ (_ : n ≤ 5), n = 15 := rfl
theorem foo3 : ∑' (n : ℕ) (_ : n ≤ 5), n = 15 := rfl
theorem foo4 : ∑' (n : ℕ), ∑' (_ : n ≤ 5), n = 15 := rfl

The first one works because it constructs a Finset first so it doesn't sum over proofs of n ≤ 5, but how can I make the rest work? Basically, why do docs#Finset.sum / docs#Finset.univ / docs#Multiset.sum / docs#tsum take in a Type* rather than a Sort*? The docstring of docs#PSigma warns of "universe level constraints", but it doesn't explain further.

[Ruben Van de Velde]

Let's take a step back. Summing over all n <= 5 makes sense, but why would you implement that as summing over a Prop?

[Eric Wieser]

I think this is a pretty reasonable request, given we do what Snir is asking already for lattice operations

[Eric Wieser]

Ultimately the things you list take in Type* not Sort* because they build upon docs#List, which does the same

[Robin Arnez]

You can use PLift thanks to docs#PLift.fintypeProp:

import Mathlib

theorem foo1 : ∑ n ≤ 5, n = 15 := rfl
theorem foo2 : ∑ (n : Fin 10), ∑ (_ : PLift (n ≤ 5)), n = 15 := rfl
theorem foo3 : ∑' (n : ℕ) (_ : PLift (n ≤ 5)), n = 15 := by sorry -- not rfl though
theorem foo4 : ∑' (n : ℕ), ∑' (_ : PLift (n ≤ 5)), n = 15 := by sorry -- not rfl though