Partitions, finite types

Stream: new members

[Antoine Chambert-Loir]

It is not clear to me how one should work with finsets.
I was willing to formulate a variant of docs#finpartition.sum_card_parts where the partition is not finite a priori,
but just finite because the ambient set is finite.
In the course of it, I was needed to prove that for a fintype X, any c : set(set X)is itself finite.
That worked out (see the mwe below), at the price of noncomputability — which I don't understand.
On the other hand, it is not clear to me neither why Lean couldn't find the instance itself.
Any explanation will be welcome !

import data.fintype.basic
import data.set.basic
import data.setoid.partition
import data.set.finite
import algebra.big_operators.basic

open_locale big_operators

variable (X : Type*)

noncomputable
lemma fintype_of_set [hfX : fintype X] (c : set (set X)) : fintype ↥c :=
begin
  have fin_ssX : fintype (set(set(X))) := set.fintype,
  apply set.finite.fintype,
  exact set.finite.of_fintype c,
end

lemma card_of_partition_eq [hfX : fintype X] {c : set (set X)} (hc : setoid.is_partition c)
  [fintype ↥c] [Π (b : set X), fintype b] :
  ∑ b in c.to_finset, fintype.card b = fintype.card X :=
begin
  sorry,
end

[Yaël Dillies]

Your first instance is docs#subtype.fintype combined with docs#set.fintype and a decidability instance that you didn't have.

[Yaël Dillies]

Long story short for decidability, a finset can be enumerated, so when constructing one you must ensure you do not add twice the same element.

[Yaël Dillies]

In another world I believe we could get rid of those decidability conditions by defining finset directly as the quotient of list under the extensionality relation, rather than as the subtype of nodup multisets. This seems to be the gist of the difference between docs#finsupp and docs#dfinsupp.

[Yaël Dillies]

Maybe @Mario Carneiro has a better explanation?

[Kevin Buzzard]

Maybe we should make some instances for set.finite in the presence of nonempty (fintype X)?

[Yaël Dillies]

We should mostly have a finite typeclass, as Yury wanted.

[Yaël Dillies]

I'm afraid however that this will only bring confusion around the finiteness conundrum.

[Yaël Dillies]

There's already a profusion of options.

[Kevin Buzzard]

But we do have a finite typeclass -- it's nonempty (fintype X)

[Kevin Buzzard]

Basically finsets are hard to use if you're a beginner or are coming to things with a mathematical viewpoint and have no interest in decidability, and I wonder whether it's worth exploring more the nonconstructive versions of these things. With polynomials we liked it so much that we switched

[Mario Carneiro]

@Yaël Dillies To get rid of the decidability assumption in subtype.fintype requires more than just quotienting lists by extensionality; this eliminates the need for the elements of the list to be distinct, but not for them to be elements of the base type A in the first place. If you have a list X covering all the elements of X and want a list of elements of {x : X // p x} covering {x : X // p x}, you have to decide for each original element whether to keep it (if p x is true) or discard it (if p x is false). If you discard an element you needed to keep then it might not cover all the elements of {x : X // p x}, and if you keep an element you need to discard then you can't fit it in the type {x : X // p x}. So you need to decide p x to determine the list.

[Antoine Chambert-Loir]

I am ready to try to understand the decidability issues, they quite interest me. But what I need above all is some directions for how we use those (fin)sets and (fin)types.
An explanation.
I formalized some results from Wielandt's Finite permutation groups. A lot of it is about group actions an arbitrary sets, but part of it requires that the sets be finite.
Should the general stuff be duplicated (eliminating decidability issues in the finset case) ?
Otherwise, should the relevant hypothesis be a fintype instance? or add a set.finite assumption?
This is here that I need directions/advices.

[Adam Topaz]

@Antoine Chambert-Loir If you can figure out how to effectively work with finiteness in lean, please do let us all know! (It's been a huge pain for a lot of us for quite some time.)

More seriously, I think it's a matter of getting to know the API, which is perhaps not so intuitive. Here are a few examples to get started. If you want to know how to do something else, let me know!

import data.set.finite

variables {α : Type*} [fintype α]

example : fintype (set α) := infer_instance
example : fintype (set (set α)) := infer_instance

example (S : set α) : S.finite := set.finite.of_fintype S -- found using library search

noncomputable
example (S : set α) : finset α := (set.finite.of_fintype S).to_finset

example (S : set (set α)) : S.finite := set.finite.of_fintype S

example (S : set (set α)) [decidable_pred (λ t, t ∈ S)] : fintype S := infer_instance

open_locale classical
noncomputable theory

example (S : set (set α)) : fintype S := infer_instance

[Adam Topaz]

(Note that lean does indeed find that last instance, but as Yaël mentioned, one has to deal with decidability, hence the open_locale classical line, or the decidable_pred parameter)