Question on documentation of Finite

Stream: general

[Axel Boldt]

In the documentation of Finite it says

"Finite (x ∈ s → β x) follows from the general instance for pi types, assuming [∀ x, Finite (β x)]".

What are they saying here? Is (x ∈ s → β x) a dependent function type? I assume s is finite?

[Eric Wieser]

That doesn't quantity over x, only over all proofs about memberships of a particular x in s

[Aaron Liu]

since Finite (x ∈ s) and ∀ (_ : x ∈ s), Finite (β x) therefore by docs#Pi.finite we have Finite (x ∈ s → β x)

[Axel Boldt]

Sorry if I'm a bit dense. Are we thinking of (x ∈ s → β x) as a proposition that depends on x, s and β, and we are claiming that, under suitable assumptions, this proposition is a finite type? In other words, it has only finitely many proofs? But I thought we don't distinguish between proofs, which would lead me to believe that any proposition is a finite type: it either contains one proof or zero proofs.

Why then would we every care to state that a certain proposition is finite? Why, for instance, is x ∈ s finite?

[Aaron Liu]

it's not a proposition

[Aaron Liu]

Axel Boldt said:

But I thought we don't distinguish between proofs, which would lead me to believe that any proposition is a finite type: it either contains one proof or zero proofs.

This is completely correct

[Aaron Liu]

but β x isn't a proposition so x ∈ s → β x also isn't a proposition

[Kyle Miller]

It's talking about x ∈ s → β x because it's the motivating case that happens relatively frequently, but the general principle is that p → β is finite if p is a proposition and β is finite, without any special casing for propositions (like you'd need for Fintype). That's because p is Finite, seeing as it has only zero or one elements (no proof, or a proof).

[Aaron Liu]

the claim is that if we assume Finite (β x) (in particular, if we assume ∀ x, Finite (β x)) then we get Finite (x ∈ s → β x)

[Kyle Miller]

The documentation may be too specific in its audience, of people who are familiar with practical details of Fintype.

[Axel Boldt]

I'm still struggling. Is (x ∈ s → β x) a dependent function type, whose elements are functions that assign to every element x of s an element of β x?

[Aaron Liu]

no

[Kyle Miller]

It's a plain old function type.

[Kyle Miller]

That's why I changed it to p → β in my comment.

[Aaron Liu]

Axel Boldt said:

a dependent function type, whose elements are functions that assign to every element x of s an element of β x?

that would be (x : α) → x ∈ s → β x or ∀ x ∈ s, β x or (x : s) → β x

[Kyle Miller]

(I wrote this docstring a year and a half ago in #9667. I wouldn't mind if someone who understands Finite and Fintype could improve the docstring(s) to be less confusing, especially for people trying to make sense of finiteness in Mathlib... It would be good to include a motivating example of the somewhat obscure fact in the docstring that this thread is about.)

[Axel Boldt]

I think I'm getting it now, thanks.

And these function types p → β, where p is a proposition and β is not, do occur in practice?

[Aaron Liu]

well they sometimes occur as a subexpression of stuff like (x : α) → x ∈ s → β x

[Kyle Miller]

An example that's close to what's in the docstring is the fact that docs#Finite.Set.finite_iUnion can handle Finite (⋃ x ∈ s, t x) if the type ι is finite on its own. (The instance docs#Finite.Set.finite_biUnion' is only needed for the case where s is finite but ι isn't.)

When Finite.Set.finite_iUnion handles Finite (⋃ x ∈ s, t x), the function type i ∈ s → Set α appears inside the term.

The general reason for this is that ⋃ x ∈ s, t x is notation for ⋃ (x : ι), ⋃ (h : x ∈ s), t x, and we can make sense of finiteness of ⋃ (h : x ∈ s), t x on its own (it's t x if x ∈ s is true, and otherwise the empty set — but in any case it doesn't matter that x ∈ s is a proposition).

[Kyle Miller]

Axel Boldt said:

And these function types p → β, where p is a proposition and β is not, do occur in practice?

docs#Option.get is an example, a function that requires a proposition to be true for the output to be valid.