bundled finite sets (and avoiding decidable instances)

Stream: general

[Kyle Miller]

Something that has been talked about many times before is having a variant on finset that's "for mathematics" (i.e., ignores issues of computability/decidability). There's a design with seemingly good definitional properties that's been rattling around my mind for a while that I spent some time today developing out to see how it might work.

Here's an overview of the design:

• We keep finset as a data type for use in computation (and perhaps it is renamed to reflect its intended use and properties).
• We replace set.finite with a predicate that says that there exists a finset with the same elements:

structure set.is_finite {α : Type*} (s : set α) : Prop :=
(exists_finset : ∃ (t : finset α), s = t)

• We define a bundled finite_set type implementing docs#set_like, and because all the finset business is in a Prop we can hide away computational issues using classical while making the carrier set have nice definitional properties.

/-- Bundled finite sets -/
structure finite_set (α : Type*) :=
(carrier : set α)
(finite : carrier.is_finite)

• We replace fintype with a Prop-valued predicate, allowing us to avoid diamond problems:

class finite_type (α : Type*) : Prop :=
(univ_finite : (set.univ : set α).is_finite)

• To work with unbundled finite sets, we use [finite_type s] just like how we are already using [fintype s], but now s.to_finite_set has the nice property that it definitionally coerces to s.

def set.to_finite_set {α : Type*} (s : set α) [finite_type s] : finite_set α :=
finite_set.mk s
(by { use (finite_set.univ : finite_set s).finite.to_finset.map (function.embedding.subtype _),
      ext, simp })

@[simp] lemma set.coe_to_finite_set {α : Type*} (s : set α) [finite_type s] :
  (s.to_finite_set : set α) = s := rfl

• We can still talk about computation by introducing instances for computing specific sets as finsets. We can compute specific finite_sets too by giving has_finset instances for them (since they coerce to set).

/-- Class for computing a `finset` for a `set`. -/
class has_finset {α : Type*} (s : set α) :=
(to_finset : finset α)
(eq_to_finset [] : s = to_finset)

[Kyle Miller]

(code below)

[Kyle Miller]

For defining operations on finite_set, the pattern is to

1. Define a set.is_finite constructor for the given set, for instance

protected lemma is_finite.inter {s t : set α} (hs : s.is_finite) (ht : t.is_finite) :
  (s ∩ t).is_finite :=
by { classical, exact ⟨⟨hs.to_finset ∩ ht.to_finset, by { ext, simp }⟩⟩ }

This involves giving a corresponding finset construction.

2. Define the finite_set operation, for instance

instance : has_inter (finite_set α) := ⟨λ s t, ⟨s ∩ t, set.is_finite.inter s.finite t.finite⟩⟩

This is simply a matter of bundling the is_finite operation.

3. Provide extensionality lemmas, for instance

@[simp] lemma mem_inter {s t : finite_set α} {x : α} : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t := iff.rfl

[Kyle Miller]

For lifting operations on sets to computations on finsets, then one can also define some instances for set operations.

instance {s t : set α} [has_finset s] [has_finset t] [decidable_eq α] :
  has_finset (s ∩ t) := ⟨s.get_finset ∩ t.get_finset, by simp⟩

The has_finset class is the set/finset analogue to decidable_eq, which is for Prop/Bool. I don't really know how well this class works in practice, but using instances seems like a reasonably good place to record this sort of thing.

[Kyle Miller]

I guess these has_finset instances can actually be useful for defining is_finite constructors.

protected lemma is_finite.inter {s t : set α} (hs : s.is_finite) (ht : t.is_finite) :
  (s ∩ t).is_finite :=
by { classical, haveI := hs.has_finset, haveI := ht.has_finset, apply is_finite_of_has_finset }
-- ^ code that's not specific to the situation.

[Kyle Miller]

newest code

import data.set
import data.finset
import data.fintype.basic

/-! ## finiteness predicate for sets -/

-- to replace `set.finite`
structure set.is_finite {α : Type*} (s : set α) : Prop :=
(exists_finset : ∃ (t : finset α), s = t)

namespace set
variables {α β : Type*}

/-- Noncomputably get the data of a `finset` that represents this set. -/
noncomputable def is_finite.to_finset {s : set α} (hs : s.is_finite) : finset α :=
hs.exists_finset.some

@[simp] lemma is_finite.mem_to_finset {s : set α} (hs : s.is_finite) (x : α) :
  x ∈ hs.to_finset ↔ x ∈ s :=
begin
  have := hs.exists_finset.some_spec.symm,
  apply_fun (λ t, x ∈ t) at this,
  simpa only [eq_iff_iff] using this,
end

/-- Class for computing a `finset` for a `set`. -/
class has_finset {α : Type*} (s : set α) :=
(to_finset : finset α)
(eq_to_finset [] : s = to_finset)

/-- Computably get a `finset` that represents this `finite_set`.
(Writing `get_finset` since mathlib already has `to_finset`.) -/
@[reducible] def get_finset (s : set α) [has_finset s] : finset α :=
has_finset.to_finset s

@[simp] lemma mem_get_finset (s : set α) [has_finset s] (x : α) :
  x ∈ s.get_finset ↔ x ∈ s :=
begin
  have := (has_finset.eq_to_finset s).symm,
  apply_fun (λ t, x ∈ t) at this,
  simpa only [eq_iff_iff] using this,
end

@[simp] def coe_get_finset (s : set α) [has_finset s] :
  (s.get_finset : set α) = s := (has_finset.eq_to_finset _).symm

@[inline] instance has_to_finset.of_finset (s : finset α) : has_finset (s : set α) :=
⟨s, rfl⟩

instance {s t : set α} [has_finset s] [has_finset t] [decidable_eq α] :
  has_finset (s ∪ t) := ⟨s.get_finset ∪ t.get_finset, by simp⟩

instance {s t : set α} [has_finset s] [has_finset t] [decidable_eq α] :
  has_finset (s ∩ t) := ⟨s.get_finset ∩ t.get_finset, by simp⟩

instance {s t : set α} [has_finset s] [has_finset t] [decidable_eq α] :
  has_finset (s \ t) := ⟨s.get_finset \ t.get_finset, by simp⟩

instance {s : set α} [has_finset s] {t : α → set β} [∀ x, has_finset (t x)]
  [decidable_eq β] : has_finset (⋃(x ∈ s), t x) :=
⟨s.get_finset.bUnion (λ x, (t x).get_finset), by simp⟩

instance : has_finset (∅ : set α) := ⟨∅, by simp⟩

instance {x : α} : has_finset ({x} : set α) := ⟨{x}, by simp⟩

instance (s : set α) [has_finset s] (x : α) [decidable_eq α] : has_finset (insert x s) :=
⟨insert x s.get_finset, by simp⟩

instance (f : α → β) (s : set α) [has_finset s] [decidable_eq β] : has_finset (f '' s) :=
⟨s.get_finset.image f, by simp⟩

def is_finite_of_has_finset (s : set α) [has_finset s] : s.is_finite :=
⟨⟨_, has_finset.eq_to_finset _⟩⟩

noncomputable def is_finite.has_finset {s : set α} (hs : s.is_finite) : has_finset s :=
⟨hs.to_finset, hs.exists_finset.some_spec⟩

protected lemma is_finite.union {s t : set α} (hs : s.is_finite) (ht : t.is_finite) :
  (s ∪ t).is_finite :=
by { classical, haveI := hs.has_finset, haveI := ht.has_finset, apply is_finite_of_has_finset }

protected lemma is_finite.inter {s t : set α} (hs : s.is_finite) (ht : t.is_finite) :
  (s ∩ t).is_finite :=
by { classical, haveI := hs.has_finset, haveI := ht.has_finset, apply is_finite_of_has_finset }

protected lemma is_finite.sdiff {s t : set α} (hs : s.is_finite) (ht : t.is_finite) :
  (s \ t).is_finite :=
by { classical, haveI := hs.has_finset, haveI := ht.has_finset, apply is_finite_of_has_finset }

protected lemma is_finite.bUnion
  {s : set α} (hs : s.is_finite) {t : α → set β} (ht : ∀ x, (t x).is_finite) :
  (⋃(x ∈ s), t x).is_finite :=
begin
  classical,
  haveI := hs.has_finset,
  haveI := λ x, (ht x).has_finset,
  apply is_finite_of_has_finset
end

protected lemma is_finite.image (f : α → β) {s : set α} (hs : s.is_finite) :
  (f '' s).is_finite :=
by { classical, haveI := hs.has_finset, apply is_finite_of_has_finset }

protected lemma is_finite.emptyc : (∅ : set α).is_finite :=
is_finite_of_has_finset _

protected lemma is_finite.singleton (x : α) : ({x} : set α).is_finite :=
is_finite_of_has_finset _

protected lemma is_finite.insert (x : α) {s : set α} (hs : s.is_finite) :
  (insert x s).is_finite :=
by { classical, haveI := hs.has_finset, apply is_finite_of_has_finset }

end set


/-! ## Bundled finite sets -/

/-- Bundled finite sets -/
structure finite_set (α : Type*) :=
(carrier : set α)
(finite : carrier.is_finite)

/-- Create a `finite_set` from a proof of finiteness.  -/
def set.is_finite.to_finite_set {α : Type*} {s : set α} (hs : s.is_finite) : finite_set α := ⟨s, hs⟩

namespace finite_set

variables {α β : Type*} {x : α}

instance : set_like (finite_set α) α :=
⟨finite_set.carrier, λ p q h, by cases p; cases q; congr'⟩

@[simp] lemma mem_carrier {s : finite_set α} : x ∈ s.carrier ↔ x ∈ s := iff.rfl

@[simp] lemma mem_mk {s : set α} {h} : x ∈ finite_set.mk s h ↔ x ∈ s := iff.rfl

@[simp] lemma mem_to_finite_set {s : set α} {hs : s.is_finite} : x ∈ hs.to_finite_set ↔ x ∈ s := iff.rfl

@[ext] theorem ext {s s' : finite_set α} (h : ∀ x, x ∈ s ↔ x ∈ s') : s = s' := set_like.ext h

/-- Copy of a `my_subobject` with a new `carrier` equal to the old one. Useful to fix definitional
equalities. See Note [range copy pattern]. -/
protected def copy (s : finite_set α) (s' : set α) (hs : s' = ↑s) : finite_set α :=
{ carrier := s',
  finite := hs.symm ▸ s.finite }

@[simp] lemma coe_copy (s : finite_set α) (s' : set α) (hs : s' = ↑s) :
  (s.copy s' hs : set α) = s' := rfl

lemma copy_eq (s : finite_set α) (s' : set α) (hs : s' = ↑s) : s.copy s' hs = s :=
set_like.coe_injective hs

instance has_coe.of_finset : has_coe (finset α) (finite_set α) := ⟨λ s, finite_set.mk ↑s ⟨⟨_, rfl⟩⟩⟩

@[simp] lemma finset.mem_coe (s : finset α) (x : α) : x ∈ (s : finite_set α) ↔ x ∈ s := iff.rfl

@[simp] lemma coe_to_finset_eq (s : finite_set α) : (s.finite.to_finset : set α) = s :=
by { ext, simp }

@[simp] lemma coe_to_finset (s : finite_set α) : (s.finite.to_finset : finite_set α) = s :=
by { ext, simp }

instance : has_union (finite_set α) := ⟨λ s t, ⟨s ∪ t, set.is_finite.union s.finite t.finite⟩⟩
instance : has_inter (finite_set α) := ⟨λ s t, ⟨s ∩ t, set.is_finite.inter s.finite t.finite⟩⟩
instance : has_sdiff (finite_set α) := ⟨λ s t, ⟨s \ t, set.is_finite.sdiff s.finite t.finite⟩⟩
instance : has_emptyc (finite_set α) := ⟨⟨∅, set.is_finite.emptyc⟩⟩
instance : has_singleton α (finite_set α) := ⟨λ x, ⟨{x}, set.is_finite.singleton x⟩⟩
instance : has_insert α (finite_set α) := ⟨λ x s, ⟨insert x s, set.is_finite.insert x s.finite⟩⟩

@[simp] lemma mem_union {s t : finite_set α} {x : α} : x ∈ s ∪ t ↔ x ∈ s ∨ x ∈ t := iff.rfl
@[simp] lemma mem_inter {s t : finite_set α} {x : α} : x ∈ s ∩ t ↔ x ∈ s ∧ x ∈ t := iff.rfl
@[simp] lemma mem_sdiff {s t : finite_set α} {x : α} : x ∈ s \ t ↔ x ∈ s ∧ ¬ x ∈ t := iff.rfl
@[simp] lemma mem_emptyc {x : α} : x ∈ (∅ : finite_set α) ↔ false := iff.rfl
@[simp] lemma mem_insert {x y : α} {s : finite_set α} : x ∈ insert y s ↔ x = y ∨ x ∈ s := iff.rfl

def bUnion (s : finite_set α) (t : α → finite_set β) : finite_set β :=
⟨⋃ (x ∈ s), t x, set.is_finite.bUnion s.finite (λ x, (t x).finite)⟩

@[simp] lemma mem_bUnion {s : finite_set α} {t : α → finite_set β} {y : β} :
  y ∈ s.bUnion t ↔ ∃ x, x ∈ s ∧ y ∈ t x := by simp [bUnion]

def image (f : α → β) (s : finite_set α) : finite_set β :=
⟨f '' s, set.is_finite.image f s.finite⟩

@[simp] lemma mem_image {f : α → β} {s : finite_set α} {y : β} :
  y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y := iff.rfl

instance : monad finite_set :=
{ map := λ _ _ f, image f,
  pure := λ _ x, {x},
  seq := λ _ _ t s, t.bUnion (λ f, s.image f),
  bind := λ _ _ s f, s.bUnion f }

end finite_set


/-! ## Finite types -/

class finite_type (α : Type*) : Prop :=
(univ_finite : (set.univ : set α).is_finite)

namespace finite_set
variables {α : Type*}

/-- `set.univ` as a `finite_set`. -/
def univ [finite_type α] : finite_set α := finite_type.univ_finite.to_finite_set

@[simp] lemma coe_univ [finite_type α] : ((univ : finite_set α) : set α) = set.univ := rfl

@[simp] lemma mem_univ [finite_type α] (x : α) : x ∈ (univ : finite_set α) := trivial

/-- Every type that is computably finite is also a `finite_type`.
(Should `fintype` even exist if there is `finite_type`?) -/
instance of_fintype [fintype α] : finite_type α := ⟨⟨⟨finset.univ, by rw finset.coe_univ⟩⟩⟩

end finite_set


/-! ## Mechanism for bundling a `set` as a `finite_set' -/

/-- Get the bundled `finite_set` for a set that has a `finite_type` instance. -/
def set.to_finite_set {α : Type*} (s : set α) [finite_type s] : finite_set α :=
finite_set.mk s
(by { use (finite_set.univ : finite_set s).finite.to_finset.map (function.embedding.subtype _),
      ext, simp })

@[simp] lemma set.coe_to_finite_set {α : Type*} (s : set α) [finite_type s] :
  (s.to_finite_set : set α) = s := rfl

[Yaël Dillies]

Why not go the other way around and hold a set in finset?

structure finset (α : Type*) :=
(val : multiset α)
(nodup : nodup val)
(to_set : set α)
(coe_eq : ∀ x, x ∈ val ↔ to_set)

Then you can define the coercion from finset α to set α as finset.to_set. No need for a new structure, and not much changes.

[Kyle Miller]

That still needs decidable instances to be useful as data. The design goals are (1) to keep a computational finite set definition around, (2) to have a computationally irrelevant finite set definition (no more decidable instances in proofs about mathematical finite sets!), (3) to have this definition have good definitional properties with respect to set, (4) to have fintype be a Prop so that instances may enjoy proof irrelevance, and (5) to have a way to associate computational sets to computationally irrelevant ones (so we at least have a place to put fintype algorithms).

That suggested change to finset partly handles 3 and does not simultaneously handle 1 and 2. The issue with 3 is that even if the sets are definitionally equal, the multisets might not be.

[Yaël Dillies]

Of course, this is a trade-off. But experience suggests that we care much more about the finset α → set α coercion than the finset α → multiset α one.

[Yaël Dillies]

I'm afraid this will just end up being "Yet another way to talk about finite things" while the symptom of the problem hasn't been solved. Namely, decidability shouldn't stop defeq. A few uneducated solutions I have to this are:

• Do not handle decidability with instances. An option is your compuitable typeclass. Another one would to have a fully separate decidability handler, which automatically marks declaration with the right decidability instances.
• Make subsingleton elimination defeq, at least for decidable and fintype

[Eric Rodriguez]

Make subsingleton elimination defeq, at least for decidable and fintype

I've always suggested this, or at least a type-class inference system that can handle defeq. I feel like the deeper we get into maths, the more we can't rejig to make things defeq. I often struggle accepting that x^1 is not definitionally equal to x (or hell, even 1*x or x*1), and these issues are just going to keep intensifying, c.f. representation theory

[Eric Wieser]

I'm curious if the change in #14122 will make decidable arguments in proofs less annoying

[Eric Rodriguez]

I guess this will mostly solve decidable, but no good solution to fintype still :(

[Eric Rodriguez]

And the only real reason it solves is it because no-one ever writes decidable instances ;b

[Reid Barton]

Make subsingleton elimination defeq, at least for decidable and fintype

I think it's strictly better to just make decidable and fintype propositions, mainly because it's a thing we can actually do

[Eric Wieser]

Making decidable p : Prop would be pointless (and would make if noncomputable!), so I assume you meant something else

[Reid Barton]

Well, effectively it means getting rid of (i.e., not using) decidable

[Reid Barton]

(Also, it's not constructively pointless!)

[Eric Wieser]

decidable is still needed for meta code though

[Reid Barton]

(Also, it's not constructively pointless!)

[Reid Barton]

Well, effectively it means getting rid of (i.e., not using) decidable

[Reid Barton]

Right, if should be noncomputable

[Eric Wieser]

Reid Barton said:

Right, if should be noncomputable

Then we need a different if for meta code

[Reid Barton]

If you're going down the extensional type theory road then you are going to have way bigger problems than that

[Reid Barton]

The general case is that if you want a definitionally irrelevant subsingleton then we already have it, it's called Prop. I agree including the case of decidable is a bit silly.

[Eric Wieser]

Does the type theory become more complex if we allow trunc to be definitionally irrelevant too?

[Eric Wieser]

Because we could wrap everything where this problem arises in trunc if necessary

[Reid Barton]

I'm pretty sure all of these amount to equality reflection, i.e., if you have h : a = b then a and b are defeq

[Reid Barton]

except the ones involving decidable, which I'm not sure about

[Eric Rodriguez]

what was the issue with equality reflection again?

[Reid Barton]

It's way outside the scope of Lean. I've seen a theorem prover based on extensional type theory but I don't remember what it was called, or how serious it was

[Anne Baanen]

NuPRL has extensional types I believe.

[Reid Barton]

The main issue is that to check a defeq the kernel might have to synthesize some arbitrary proof of equality--obviously there's no algorithm that can do so in all cases, so how do you make something usable and reliable and trustable.

[Reid Barton]

In Lean's current type theory the definitional equality is more or less decidable by an algorithm and that algorithm works in practice most of the time.

[Eric Rodriguez]

why can't we just use the current kernel typechecker. if a rfl that should work fails that shouldn't be able to affect consistency

[Eric Rodriguez]

and then we can just add the extra rfls that need kernel support

[Reid Barton]

Those extra rfls are where the problem is

[Reid Barton]

Those extra rfls are where the problem is

[Eric Rodriguez]

how so? say for example we have Lean + "if there's a proof that a type t is a subsingleton in the instance cache somehow, then a = b : @eq t is rfl"

[Reid Barton]

Well the kernel doesn't have an instance cache

[Reid Barton]

Proof irrelevance for Prop is already a bit funny and I think it's why definitions using well-founded recursion don't compute in the kernel (right?)

[Eric Rodriguez]

Hmm, I guess not, but the higher-level automation could add the instances that are used using have statements to the proofs. I guess this is really slow and complicated, though

[Eric Rodriguez]

For specific types, however, specific support could be added and that solves 99% of the issues (fintype, decidable, Q-algebras maybe)

[Johan Commelin]

Eric Wieser said:

Then we need a different if for meta code

I suggest mif

[Reid Barton]

OK so let's suppose you write down a rule "if a : fintype X and b : fintype X then a and b are defeq"

[Reid Barton]

How do you know when to apply the rule?

[Kyle Miller]

@Johan Commelin That makes sense, but we should probably think ahead to Lean 4 -- we probably don't want to override its programming language features. We could have if' on the math side, or cif for "classical if".

[Reid Barton]

Maybe I'm trying to type check rfl : 0 = sum (x : X), x

[Reid Barton]

That sum involves a fintype X argument which might be stuck for some reason (e.g., uses an axiom). But wait! what if I can somehow cook up a second b : fintype X which isn't stuck, and then keep reducing

[Reid Barton]

Now I am back to the same problem, namely, I should be able to synthesize terms out of thin air

[Reid Barton]

Maybe you say: well too bad, I don't know how to do that. Then you are in the nontransitivite defeq situation. The sum with the bad fintype instance is convertible to the one with the good fintype instance (by fintype irrelevance), which can be reduced to 0. But we aren't capable of reducing the original sum to 0.

[Reid Barton]

If that is going to happen anyways, then maybe sum should just be noncomputable in the first place, and we can use tactics/propositional reasoning when we want to "compute" it. At least this is something that we could Just Do today, and doesn't require modifying the kernel with possibly other consequences.

[Eric Rodriguez]

Thanks, that's a really good explanation. I feel like a non-transitive defeq isn't that evil, though - hell, I thought we had it already for some language features. Plus, it also fits my idea of "true by definition" in informal mathematics.

[Eric Rodriguez]

But I guess this second approach is the current tsum/etc approach, and that leaves us with a lot of arguments we have to carry around. Maybe we can improve that by making an instanced version of nonempty (x)for relevant x, and then we get TC search and not a bunch of annoying arguments everywhere

[Kyle Miller]

Yaël Dillies said:

Of course, this is a trade-off. But experience suggests that we care much more about the finset α → set α coercion than the finset α → multiset α one.

I suspect I'm not being understood here. The issues is not about coercions per se. The proposed finite_set type has the property that the finite sets are definitionally equal if and only if the underlying sets are definitionally equal. When you have the multiset in the mix as actual data, you essentially have diamond problems, which I at least would like to avoid.

Regarding a trade-off, the five design goals I mentioned are all met by the finite_set proposal. It does not meet the unmentioned number 6 (not be a whole lot of work) but I think this is unavoidable.

So long as we keep using data structures for finite sets as if they were sets that are finite, I think we're going to keep having a struggle. Regarding your concern about "yet another way to talk about finite things", it seems similar to how we have both lists and functions fin n -> A, but we don't try to force one to be the other.

[Reid Barton]

Or maybe you really specifically need the definitional equality (because these expressions are appearing in the index of some type family) and then yes, I agree it would be much nicer if you could convince the kernel to do these conversions; I just don't know what the framework for making it work reliably should look like, and I'm not sure whether anyone does

[Kyle Miller]

@Reid Barton Do you have any thoughts about the finite_set proposal? It seems like you're in favor at least in principle. I'm wondering partly because I know you spent time a while back working on this sort of thing.

[Kyle Miller]

To reduce work, I think leaving fintype as-is makes sense for now (rather than replacing it) and introducing finite_type for the Prop version, then having finite_type instances from fintype instances.

[Eric Wieser]

Yaël Dillies said:

Why not go the other way around and hold a set in finset?
<snip>

Just to note, the effect of this change is to have nicer definitional control of what finset membership means, but it's orthogonal to decidability discussions.

[Kyle Miller]

@Eric Wieser What's "this"? I assume you're clarifying Yael's suggestion?

[Eric Wieser]

"this" refers to Yael's suggestion in the message I quoted

[Kyle Miller]

After going through all of what we have already in data/set/finite and reorganizing it (#14136), I guess we already have pretty much everything set up for bundled finite sets. Here's an overview for a proposed design:

• finset remains as-is. It's the computational model (i.e. a data structure) for finite sets.
• fintype remains as-is. Paired with docs#set.to_finite, this is the database of ways to turn sets that are finite into computable finite sets. (It's the finite set analogue of decidable.)
• set.finite remains as-is. This is the predicate that represents the mere fact that a set is finite without offering any computational guarantees.
• In data/set/finite there is a long list of fintype instances that give ways of computing different set constructions already.
• Parallel to that, data/set/finite also has a long list of set.finite constructions. These are mostly formulaic, just applying fintype instances.
• Then we can define finite_set, which is a set that is set.finite. This will have all the properties I mentioned in my first posts. Operations on finite_set can be lifted in a mostly formulaic way from corresponding set.finite constructions, and properties should be mostly liftable from set properties due to the fact a finite_set "is" a set. (Note: in the VM, a finite_set will be essentially computationally irrelevant, similar to set. At most they'll be passed around as zero-argument constructors.)
• We can also define finite_type. There are a couple ways this could be defined, but probably the easiest is nonempty (fintype A). This is a type whose set.univ can be given as a finite_set.

[Kevin Buzzard]

+1 for finite_type, I thought @Yury G. Kudryashov mentioned at some point that he was thinking of adding this.

[Yury G. Kudryashov]

I've started working on a typeclass for countable types (and sorts), see branch#YK-countable.

[Yury G. Kudryashov]

It would be nice if someone adopts this branch.

[Yury G. Kudryashov]

About finite_type: please make it work for Sort*.

[Yury G. Kudryashov]

E.g., you can define finite_type (α : Sort*) := (ex_equiv_fin : ∃ n : nat, nonempty (α ≃ fin n))

[Yury G. Kudryashov]

With this typeclass, we can have lemmas about finite unions/intersections without dealing separately with unions over proofs of propositions.

[Kyle Miller]

I was wondering all the ways we have to represent finite (multi)sets in mathlib. Here's what I could think of (and if there are others anyone can think of, I'll add them to the list).

Finite sets:

• docs#finset (a multiset without duplicates)
• docs#set satisfying docs#set.finite
• docs#set whose coercion has a docs#fintype instance
• docs#finsupp with fin 2 codomain

Finite multisets:

• docs#multiset (a list modulo permutation)
• docs#finsupp with ℕ codomain

[Kyle Miller]

This is a kind of funny and perhaps roundabout way to work with finite sets:

import data.finsupp.basic

instance : has_zero Prop := ⟨false⟩

def finset' (α : Sort*) := finsupp α Prop

def finset'.to_set {α : Type*} : finset' α → set α := finsupp.to_fun

If you expand out the definitions it's essentially something Yael suggested earlier, which is a finite set definition that contains both a finset and a set so you can get definitional control over both.