Zulip Chat Archive

Stream: new members

Topic: Partitions, finite types

Antoine Chambert-Loir (Mar 02 2022 at 23:23):

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*)

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

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 :=

Yaël Dillies (Mar 02 2022 at 23:33):

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

Yaël Dillies (Mar 02 2022 at 23:35):

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 (Mar 02 2022 at 23:37):

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 (Mar 02 2022 at 23:37):

Maybe @Mario Carneiro has a better explanation?

Kevin Buzzard (Mar 03 2022 at 00:00):

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

Yaël Dillies (Mar 03 2022 at 00:01):

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

Yaël Dillies (Mar 03 2022 at 00:02):

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

Yaël Dillies (Mar 03 2022 at 00:02):

There's already a profusion of options.

Kevin Buzzard (Mar 03 2022 at 00:03):

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

Kevin Buzzard (Mar 03 2022 at 00:04):

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 (Mar 03 2022 at 11:28):

@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 (Mar 03 2022 at 13:27):

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 (Mar 03 2022 at 15:53):

@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

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 (Mar 03 2022 at 15:59):

(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)

Last updated: Dec 20 2023 at 11:08 UTC